This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem frlmvplusgscavalb

Description: Addition combined with scalar multiplication in a free module at the coordinates. (Contributed by AV, 16-Jan-2023)

Ref Expression
Hypotheses frlmplusgvalb.f 
|- F = ( R freeLMod I )
frlmplusgvalb.b 
|- B = ( Base ` F )
frlmplusgvalb.i 
|- ( ph -> I e. W )
frlmplusgvalb.x 
|- ( ph -> X e. B )
frlmplusgvalb.z 
|- ( ph -> Z e. B )
frlmplusgvalb.r 
|- ( ph -> R e. Ring )
frlmvscavalb.k 
|- K = ( Base ` R )
frlmvscavalb.a 
|- ( ph -> A e. K )
frlmvscavalb.v 
|- .xb = ( .s ` F )
frlmvscavalb.t 
|- .x. = ( .r ` R )
frlmvplusgscavalb.y 
|- ( ph -> Y e. B )
frlmvplusgscavalb.a 
|- .+ = ( +g ` R )
frlmvplusgscavalb.p 
|- .+b = ( +g ` F )
frlmvplusgscavalb.c 
|- ( ph -> C e. K )
Assertion frlmvplusgscavalb 
|- ( 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 frlmplusgvalb.f 
 |-  F = ( R freeLMod I )
2 frlmplusgvalb.b 
 |-  B = ( Base ` F )
3 frlmplusgvalb.i 
 |-  ( ph -> I e. W )
4 frlmplusgvalb.x 
 |-  ( ph -> X e. B )
5 frlmplusgvalb.z 
 |-  ( ph -> Z e. B )
6 frlmplusgvalb.r 
 |-  ( ph -> R e. Ring )
7 frlmvscavalb.k 
 |-  K = ( Base ` R )
8 frlmvscavalb.a 
 |-  ( ph -> A e. K )
9 frlmvscavalb.v 
 |-  .xb = ( .s ` F )
10 frlmvscavalb.t 
 |-  .x. = ( .r ` R )
11 frlmvplusgscavalb.y 
 |-  ( ph -> Y e. B )
12 frlmvplusgscavalb.a 
 |-  .+ = ( +g ` R )
13 frlmvplusgscavalb.p 
 |-  .+b = ( +g ` F )
14 frlmvplusgscavalb.c 
 |-  ( ph -> C e. K )
15 1 frlmlmod 
 |-  ( ( R e. Ring /\ I e. W ) -> F e. LMod )
16 6 3 15 syl2anc 
 |-  ( ph -> F e. LMod )
17 8 7 eleqtrdi 
 |-  ( ph -> A e. ( Base ` R ) )
18 1 frlmsca 
 |-  ( ( R e. Ring /\ I e. W ) -> R = ( Scalar ` F ) )
19 6 3 18 syl2anc 
 |-  ( ph -> R = ( Scalar ` F ) )
20 19 fveq2d 
 |-  ( ph -> ( Base ` R ) = ( Base ` ( Scalar ` F ) ) )
21 17 20 eleqtrd 
 |-  ( ph -> A e. ( Base ` ( Scalar ` F ) ) )
22 eqid 
 |-  ( Scalar ` F ) = ( Scalar ` F )
23 eqid 
 |-  ( Base ` ( Scalar ` F ) ) = ( Base ` ( Scalar ` F ) )
24 2 22 9 23 lmodvscl 
 |-  ( ( F e. LMod /\ A e. ( Base ` ( Scalar ` F ) ) /\ X e. B ) -> ( A .xb X ) e. B )
25 16 21 4 24 syl3anc 
 |-  ( ph -> ( A .xb X ) e. B )
26 14 7 eleqtrdi 
 |-  ( ph -> C e. ( Base ` R ) )
27 26 20 eleqtrd 
 |-  ( ph -> C e. ( Base ` ( Scalar ` F ) ) )
28 2 22 9 23 lmodvscl 
 |-  ( ( F e. LMod /\ C e. ( Base ` ( Scalar ` F ) ) /\ Y e. B ) -> ( C .xb Y ) e. B )
29 16 27 11 28 syl3anc 
 |-  ( ph -> ( C .xb Y ) e. B )
30 1 2 3 25 5 6 29 12 13 frlmplusgvalb 
 |-  ( ph -> ( Z = ( ( A .xb X ) .+b ( C .xb Y ) ) <-> A. i e. I ( Z ` i ) = ( ( ( A .xb X ) ` i ) .+ ( ( C .xb Y ) ` i ) ) ) )
31 3 adantr 
 |-  ( ( ph /\ i e. I ) -> I e. W )
32 8 adantr 
 |-  ( ( ph /\ i e. I ) -> A e. K )
33 4 adantr 
 |-  ( ( ph /\ i e. I ) -> X e. B )
34 simpr 
 |-  ( ( ph /\ i e. I ) -> i e. I )
35 1 2 7 31 32 33 34 9 10 frlmvscaval 
 |-  ( ( ph /\ i e. I ) -> ( ( A .xb X ) ` i ) = ( A .x. ( X ` i ) ) )
36 14 adantr 
 |-  ( ( ph /\ i e. I ) -> C e. K )
37 11 adantr 
 |-  ( ( ph /\ i e. I ) -> Y e. B )
38 1 2 7 31 36 37 34 9 10 frlmvscaval 
 |-  ( ( ph /\ i e. I ) -> ( ( C .xb Y ) ` i ) = ( C .x. ( Y ` i ) ) )
39 35 38 oveq12d 
 |-  ( ( ph /\ i e. I ) -> ( ( ( A .xb X ) ` i ) .+ ( ( C .xb Y ) ` i ) ) = ( ( A .x. ( X ` i ) ) .+ ( C .x. ( Y ` i ) ) ) )
40 39 eqeq2d 
 |-  ( ( ph /\ i e. I ) -> ( ( Z ` i ) = ( ( ( A .xb X ) ` i ) .+ ( ( C .xb Y ) ` i ) ) <-> ( Z ` i ) = ( ( A .x. ( X ` i ) ) .+ ( C .x. ( Y ` i ) ) ) ) )
41 40 ralbidva 
 |-  ( ph -> ( A. i e. I ( Z ` i ) = ( ( ( A .xb X ) ` i ) .+ ( ( C .xb Y ) ` i ) ) <-> A. i e. I ( Z ` i ) = ( ( A .x. ( X ` i ) ) .+ ( C .x. ( Y ` i ) ) ) ) )
42 30 41 bitrd 
 |-  ( ph -> ( Z = ( ( A .xb X ) .+b ( C .xb Y ) ) <-> A. i e. I ( Z ` i ) = ( ( A .x. ( X ` i ) ) .+ ( C .x. ( Y ` i ) ) ) ) )