Metamath Proof Explorer

Theorem rrxplusgvscavalb

Description: The result of the addition combined with scalar multiplication in a generalized Euclidean space is defined by its coordinate-wise operations. (Contributed by AV, 21-Jan-2023)

Ref Expression
Hypotheses rrxval.r 
|- H = ( RR^ ` I )
rrxbase.b 
|- B = ( Base ` H )
rrxplusgvscavalb.r 
|- .xb = ( .s ` H )
rrxplusgvscavalb.i 
|- ( ph -> I e. V )
rrxplusgvscavalb.a 
|- ( ph -> A e. RR )
rrxplusgvscavalb.x 
|- ( ph -> X e. B )
rrxplusgvscavalb.y 
|- ( ph -> Y e. B )
rrxplusgvscavalb.z 
|- ( ph -> Z e. B )
rrxplusgvscavalb.p 
|- .+b = ( +g ` H )
rrxplusgvscavalb.c 
|- ( ph -> C e. RR )
Assertion rrxplusgvscavalb 
|- ( ph -> ( Z = ( ( A .xb X ) .+b ( C .xb Y ) ) <-> A. i e. I ( Z ` i ) = ( ( A x. ( X ` i ) ) + ( C x. ( Y ` i ) ) ) ) )

Proof

Step Hyp Ref Expression
1 rrxval.r 
 |-  H = ( RR^ ` I )
2 rrxbase.b 
 |-  B = ( Base ` H )
3 rrxplusgvscavalb.r 
 |-  .xb = ( .s ` H )
4 rrxplusgvscavalb.i 
 |-  ( ph -> I e. V )
5 rrxplusgvscavalb.a 
 |-  ( ph -> A e. RR )
6 rrxplusgvscavalb.x 
 |-  ( ph -> X e. B )
7 rrxplusgvscavalb.y 
 |-  ( ph -> Y e. B )
8 rrxplusgvscavalb.z 
 |-  ( ph -> Z e. B )
9 rrxplusgvscavalb.p 
 |-  .+b = ( +g ` H )
10 rrxplusgvscavalb.c 
 |-  ( ph -> C e. RR )
11 1 rrxval 
 |-  ( I e. V -> H = ( toCPreHil ` ( RRfld freeLMod I ) ) )
12 4 11 syl 
 |-  ( ph -> H = ( toCPreHil ` ( RRfld freeLMod I ) ) )
13 12 fveq2d 
 |-  ( ph -> ( +g ` H ) = ( +g ` ( toCPreHil ` ( RRfld freeLMod I ) ) ) )
14 9 13 syl5eq 
 |-  ( ph -> .+b = ( +g ` ( toCPreHil ` ( RRfld freeLMod I ) ) ) )
15 12 fveq2d 
 |-  ( ph -> ( .s ` H ) = ( .s ` ( toCPreHil ` ( RRfld freeLMod I ) ) ) )
16 3 15 syl5eq 
 |-  ( ph -> .xb = ( .s ` ( toCPreHil ` ( RRfld freeLMod I ) ) ) )
17 16 oveqd 
 |-  ( ph -> ( A .xb X ) = ( A ( .s ` ( toCPreHil ` ( RRfld freeLMod I ) ) ) X ) )
18 16 oveqd 
 |-  ( ph -> ( C .xb Y ) = ( C ( .s ` ( toCPreHil ` ( RRfld freeLMod I ) ) ) Y ) )
19 14 17 18 oveq123d 
 |-  ( ph -> ( ( A .xb X ) .+b ( C .xb Y ) ) = ( ( A ( .s ` ( toCPreHil ` ( RRfld freeLMod I ) ) ) X ) ( +g ` ( toCPreHil ` ( RRfld freeLMod I ) ) ) ( C ( .s ` ( toCPreHil ` ( RRfld freeLMod I ) ) ) Y ) ) )
20 19 eqeq2d 
 |-  ( ph -> ( Z = ( ( A .xb X ) .+b ( C .xb Y ) ) <-> Z = ( ( A ( .s ` ( toCPreHil ` ( RRfld freeLMod I ) ) ) X ) ( +g ` ( toCPreHil ` ( RRfld freeLMod I ) ) ) ( C ( .s ` ( toCPreHil ` ( RRfld freeLMod I ) ) ) Y ) ) ) )
21 eqid 
 |-  ( RRfld freeLMod I ) = ( RRfld freeLMod I )
22 eqid 
 |-  ( Base ` ( RRfld freeLMod I ) ) = ( Base ` ( RRfld freeLMod I ) )
23 12 fveq2d 
 |-  ( ph -> ( Base ` H ) = ( Base ` ( toCPreHil ` ( RRfld freeLMod I ) ) ) )
24 eqid 
 |-  ( toCPreHil ` ( RRfld freeLMod I ) ) = ( toCPreHil ` ( RRfld freeLMod I ) )
25 24 22 tcphbas 
 |-  ( Base ` ( RRfld freeLMod I ) ) = ( Base ` ( toCPreHil ` ( RRfld freeLMod I ) ) )
26 23 2 25 3eqtr4g 
 |-  ( ph -> B = ( Base ` ( RRfld freeLMod I ) ) )
27 6 26 eleqtrd 
 |-  ( ph -> X e. ( Base ` ( RRfld freeLMod I ) ) )
28 8 26 eleqtrd 
 |-  ( ph -> Z e. ( Base ` ( RRfld freeLMod I ) ) )
29 recrng 
 |-  RRfld e. *Ring
30 srngring 
 |-  ( RRfld e. *Ring -> RRfld e. Ring )
31 29 30 mp1i 
 |-  ( ph -> RRfld e. Ring )
32 rebase 
 |-  RR = ( Base ` RRfld )
33 eqid 
 |-  ( .s ` ( RRfld freeLMod I ) ) = ( .s ` ( RRfld freeLMod I ) )
34 24 33 tcphvsca 
 |-  ( .s ` ( RRfld freeLMod I ) ) = ( .s ` ( toCPreHil ` ( RRfld freeLMod I ) ) )
35 34 eqcomi 
 |-  ( .s ` ( toCPreHil ` ( RRfld freeLMod I ) ) ) = ( .s ` ( RRfld freeLMod I ) )
36 remulr 
 |-  x. = ( .r ` RRfld )
37 7 26 eleqtrd 
 |-  ( ph -> Y e. ( Base ` ( RRfld freeLMod I ) ) )
38 replusg 
 |-  + = ( +g ` RRfld )
39 eqid 
 |-  ( +g ` ( RRfld freeLMod I ) ) = ( +g ` ( RRfld freeLMod I ) )
40 24 39 tchplusg 
 |-  ( +g ` ( RRfld freeLMod I ) ) = ( +g ` ( toCPreHil ` ( RRfld freeLMod I ) ) )
41 40 eqcomi 
 |-  ( +g ` ( toCPreHil ` ( RRfld freeLMod I ) ) ) = ( +g ` ( RRfld freeLMod I ) )
42 21 22 4 27 28 31 32 5 35 36 37 38 41 10 frlmvplusgscavalb 
 |-  ( ph -> ( Z = ( ( A ( .s ` ( toCPreHil ` ( RRfld freeLMod I ) ) ) X ) ( +g ` ( toCPreHil ` ( RRfld freeLMod I ) ) ) ( C ( .s ` ( toCPreHil ` ( RRfld freeLMod I ) ) ) Y ) ) <-> A. i e. I ( Z ` i ) = ( ( A x. ( X ` i ) ) + ( C x. ( Y ` i ) ) ) ) )
43 20 42 bitrd 
 |-  ( ph -> ( Z = ( ( A .xb X ) .+b ( C .xb Y ) ) <-> A. i e. I ( Z ` i ) = ( ( A x. ( X ` i ) ) + ( C x. ( Y ` i ) ) ) ) )