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