Hi Alexander, Here I believe ~tcphsca is your friend. Assuming an hypothesis:
|- .xb = ( Scalar ` ( RR^ ` I ) ) You should be able to use `tcphsca` to obtain something like: |- .xb = ( Scalar ` ( RRfld freeLMod I ) ) And then apply ~frlmvscaval to get your result. _ Thierry On 18/01/2023 08:40, 'Alexander van der Vekens' via Metamath wrote:
Although (generalized) Euclidean spaces RR^ (and implicitly EEhil) are defined as extended free left modules (see df-rrx $a |- RR^ = ( i e. _V |-> ( toCPreHil ` ( RRfld freeLMod i ) ) ), it seems that they aren't free left modules. At least I see no way to apply the theorems available for free left modules to the Euclidean spaces as defined above. For example, I want to show ( ph -> ( ( A .xb X ) ` i ) = ( A .x. ( X ` i ) ) ) (the ith coodinate of the scalar product of a vector X with a real number A is the usual real multiplication of the ith coordinate of X with A) where X e. ( Base ` ( RR^ ` I ) ), A e. RR and i e. I. For free left modules, we have the corresponding theorem ~frlmvscaval, but I wonder how this theorem can be used to prove my theorem. Is there a simple way to make ( RR^ ` I ) a free left module, so that the theorems for free left modules are also available for ( RR^ ` I )? -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/1a52a8cf-3c51-488f-8911-b5412e8e938fn%40googlegroups.com <https://groups.google.com/d/msgid/metamath/1a52a8cf-3c51-488f-8911-b5412e8e938fn%40googlegroups.com?utm_medium=email&utm_source=footer>.
-- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/3f581b21-f627-b714-5649-2eddd103fc72%40gmx.net.
