Metamath Proof Explorer

Theorem rrxvsca

Description: The scalar product over generalized Euclidean spaces is the componentwise real number multiplication. (Contributed by Thierry Arnoux, 18-Jan-2023)

Ref Expression
Hypotheses rrxval.r 
|- H = ( RR^ ` I )
rrxbase.b 
|- B = ( Base ` H )
rrxvsca.r 
|- .xb = ( .s ` H )
rrxvsca.i 
|- ( ph -> I e. V )
rrxvsca.j 
|- ( ph -> J e. I )
rrxvsca.a 
|- ( ph -> A e. RR )
rrxvsca.x 
|- ( ph -> X e. ( Base ` H ) )
Assertion rrxvsca 
|- ( ph -> ( ( A .xb X ) ` J ) = ( A x. ( X ` J ) ) )

Proof

Step Hyp Ref Expression
1 rrxval.r 
 |-  H = ( RR^ ` I )
2 rrxbase.b 
 |-  B = ( Base ` H )
3 rrxvsca.r 
 |-  .xb = ( .s ` H )
4 rrxvsca.i 
 |-  ( ph -> I e. V )
5 rrxvsca.j 
 |-  ( ph -> J e. I )
6 rrxvsca.a 
 |-  ( ph -> A e. RR )
7 rrxvsca.x 
 |-  ( ph -> X e. ( Base ` H ) )
8 1 rrxval 
 |-  ( I e. V -> H = ( toCPreHil ` ( RRfld freeLMod I ) ) )
9 4 8 syl 
 |-  ( ph -> H = ( toCPreHil ` ( RRfld freeLMod I ) ) )
10 9 fveq2d 
 |-  ( ph -> ( .s ` H ) = ( .s ` ( toCPreHil ` ( RRfld freeLMod I ) ) ) )
11 3 10 syl5eq 
 |-  ( ph -> .xb = ( .s ` ( toCPreHil ` ( RRfld freeLMod I ) ) ) )
12 11 oveqd 
 |-  ( ph -> ( A .xb X ) = ( A ( .s ` ( toCPreHil ` ( RRfld freeLMod I ) ) ) X ) )
13 12 fveq1d 
 |-  ( ph -> ( ( A .xb X ) ` J ) = ( ( A ( .s ` ( toCPreHil ` ( RRfld freeLMod I ) ) ) X ) ` J ) )
14 eqid 
 |-  ( RRfld freeLMod I ) = ( RRfld freeLMod I )
15 eqid 
 |-  ( Base ` ( RRfld freeLMod I ) ) = ( Base ` ( RRfld freeLMod I ) )
16 rebase 
 |-  RR = ( Base ` RRfld )
17 9 fveq2d 
 |-  ( ph -> ( Base ` H ) = ( Base ` ( toCPreHil ` ( RRfld freeLMod I ) ) ) )
18 eqid 
 |-  ( toCPreHil ` ( RRfld freeLMod I ) ) = ( toCPreHil ` ( RRfld freeLMod I ) )
19 18 15 tcphbas 
 |-  ( Base ` ( RRfld freeLMod I ) ) = ( Base ` ( toCPreHil ` ( RRfld freeLMod I ) ) )
20 17 19 eqtr4di 
 |-  ( ph -> ( Base ` H ) = ( Base ` ( RRfld freeLMod I ) ) )
21 7 20 eleqtrd 
 |-  ( ph -> X e. ( Base ` ( RRfld freeLMod I ) ) )
22 eqid 
 |-  ( .s ` ( RRfld freeLMod I ) ) = ( .s ` ( RRfld freeLMod I ) )
23 18 22 tcphvsca 
 |-  ( .s ` ( RRfld freeLMod I ) ) = ( .s ` ( toCPreHil ` ( RRfld freeLMod I ) ) )
24 23 eqcomi 
 |-  ( .s ` ( toCPreHil ` ( RRfld freeLMod I ) ) ) = ( .s ` ( RRfld freeLMod I ) )
25 remulr 
 |-  x. = ( .r ` RRfld )
26 14 15 16 4 6 21 5 24 25 frlmvscaval 
 |-  ( ph -> ( ( A ( .s ` ( toCPreHil ` ( RRfld freeLMod I ) ) ) X ) ` J ) = ( A x. ( X ` J ) ) )
27 13 26 eqtrd 
 |-  ( ph -> ( ( A .xb X ) ` J ) = ( A x. ( X ` J ) ) )