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.
