Euclidean spaces as free left modules?

[Alexander van der Vekens]

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 )?

[Thierry Arnoux]

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

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/1a52a8cf-3c51-488f-8911-b5412e8e938fn%40googlegroups.com.