Metamath Proof Explorer

Theorem frlmplusgvalb

Description: Addition 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 )
frlmplusgvalb.y 
|- ( ph -> Y e. B )
frlmplusgvalb.a 
|- .+ = ( +g ` R )
frlmplusgvalb.p 
|- .+b = ( +g ` F )
Assertion frlmplusgvalb 
|- ( ph -> ( Z = ( X .+b Y ) <-> A. i e. I ( Z ` i ) = ( ( X ` i ) .+ ( 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 frlmplusgvalb.y 
 |-  ( ph -> Y e. B )
8 frlmplusgvalb.a 
 |-  .+ = ( +g ` R )
9 frlmplusgvalb.p 
 |-  .+b = ( +g ` F )
10 eqid 
 |-  ( Base ` R ) = ( Base ` R )
11 1 10 2 frlmbasmap 
 |-  ( ( I e. W /\ Z e. B ) -> Z e. ( ( Base ` R ) ^m I ) )
12 3 5 11 syl2anc 
 |-  ( ph -> Z e. ( ( Base ` R ) ^m I ) )
13 fvexd 
 |-  ( ph -> ( Base ` R ) e. _V )
14 13 3 elmapd 
 |-  ( ph -> ( Z e. ( ( Base ` R ) ^m I ) <-> Z : I --> ( Base ` R ) ) )
15 12 14 mpbid 
 |-  ( ph -> Z : I --> ( Base ` R ) )
16 15 ffnd 
 |-  ( ph -> Z Fn I )
17 1 frlmlmod 
 |-  ( ( R e. Ring /\ I e. W ) -> F e. LMod )
18 6 3 17 syl2anc 
 |-  ( ph -> F e. LMod )
19 lmodgrp 
 |-  ( F e. LMod -> F e. Grp )
20 18 19 syl 
 |-  ( ph -> F e. Grp )
21 2 9 grpcl 
 |-  ( ( F e. Grp /\ X e. B /\ Y e. B ) -> ( X .+b Y ) e. B )
22 20 4 7 21 syl3anc 
 |-  ( ph -> ( X .+b Y ) e. B )
23 1 10 2 frlmbasmap 
 |-  ( ( I e. W /\ ( X .+b Y ) e. B ) -> ( X .+b Y ) e. ( ( Base ` R ) ^m I ) )
24 3 22 23 syl2anc 
 |-  ( ph -> ( X .+b Y ) e. ( ( Base ` R ) ^m I ) )
25 13 3 elmapd 
 |-  ( ph -> ( ( X .+b Y ) e. ( ( Base ` R ) ^m I ) <-> ( X .+b Y ) : I --> ( Base ` R ) ) )
26 24 25 mpbid 
 |-  ( ph -> ( X .+b Y ) : I --> ( Base ` R ) )
27 26 ffnd 
 |-  ( ph -> ( X .+b Y ) Fn I )
28 eqfnfv 
 |-  ( ( Z Fn I /\ ( X .+b Y ) Fn I ) -> ( Z = ( X .+b Y ) <-> A. i e. I ( Z ` i ) = ( ( X .+b Y ) ` i ) ) )
29 16 27 28 syl2anc 
 |-  ( ph -> ( Z = ( X .+b Y ) <-> A. i e. I ( Z ` i ) = ( ( X .+b Y ) ` i ) ) )
30 6 adantr 
 |-  ( ( ph /\ i e. I ) -> R e. Ring )
31 3 adantr 
 |-  ( ( ph /\ i e. I ) -> I e. W )
32 4 adantr 
 |-  ( ( ph /\ i e. I ) -> X e. B )
33 7 adantr 
 |-  ( ( ph /\ i e. I ) -> Y e. B )
34 simpr 
 |-  ( ( ph /\ i e. I ) -> i e. I )
35 1 2 30 31 32 33 34 8 9 frlmvplusgvalc 
 |-  ( ( ph /\ i e. I ) -> ( ( X .+b Y ) ` i ) = ( ( X ` i ) .+ ( Y ` i ) ) )
36 35 eqeq2d 
 |-  ( ( ph /\ i e. I ) -> ( ( Z ` i ) = ( ( X .+b Y ) ` i ) <-> ( Z ` i ) = ( ( X ` i ) .+ ( Y ` i ) ) ) )
37 36 ralbidva 
 |-  ( ph -> ( A. i e. I ( Z ` i ) = ( ( X .+b Y ) ` i ) <-> A. i e. I ( Z ` i ) = ( ( X ` i ) .+ ( Y ` i ) ) ) )
38 29 37 bitrd 
 |-  ( ph -> ( Z = ( X .+b Y ) <-> A. i e. I ( Z ` i ) = ( ( X ` i ) .+ ( Y ` i ) ) ) )