Metamath Proof Explorer

Theorem frlmplusgval

Description: Addition in a free module. (Contributed by Stefan O'Rear, 1-Feb-2015) (Revised by Stefan O'Rear, 6-May-2015)

Ref Expression
Hypotheses frlmplusgval.y 
|- Y = ( R freeLMod I )
frlmplusgval.b 
|- B = ( Base ` Y )
frlmplusgval.r 
|- ( ph -> R e. V )
frlmplusgval.i 
|- ( ph -> I e. W )
frlmplusgval.f 
|- ( ph -> F e. B )
frlmplusgval.g 
|- ( ph -> G e. B )
frlmplusgval.a 
|- .+ = ( +g ` R )
frlmplusgval.p 
|- .+b = ( +g ` Y )
Assertion frlmplusgval 
|- ( ph -> ( F .+b G ) = ( F oF .+ G ) )

Proof

Step Hyp Ref Expression
1 frlmplusgval.y 
 |-  Y = ( R freeLMod I )
2 frlmplusgval.b 
 |-  B = ( Base ` Y )
3 frlmplusgval.r 
 |-  ( ph -> R e. V )
4 frlmplusgval.i 
 |-  ( ph -> I e. W )
5 frlmplusgval.f 
 |-  ( ph -> F e. B )
6 frlmplusgval.g 
 |-  ( ph -> G e. B )
7 frlmplusgval.a 
 |-  .+ = ( +g ` R )
8 frlmplusgval.p 
 |-  .+b = ( +g ` Y )
9 eqid 
 |-  ( Base ` Y ) = ( Base ` Y )
10 1 9 frlmpws 
 |-  ( ( R e. V /\ I e. W ) -> Y = ( ( ( ringLMod ` R ) ^s I ) |`s ( Base ` Y ) ) )
11 3 4 10 syl2anc 
 |-  ( ph -> Y = ( ( ( ringLMod ` R ) ^s I ) |`s ( Base ` Y ) ) )
12 11 fveq2d 
 |-  ( ph -> ( +g ` Y ) = ( +g ` ( ( ( ringLMod ` R ) ^s I ) |`s ( Base ` Y ) ) ) )
13 fvex 
 |-  ( Base ` Y ) e. _V
14 eqid 
 |-  ( ( ( ringLMod ` R ) ^s I ) |`s ( Base ` Y ) ) = ( ( ( ringLMod ` R ) ^s I ) |`s ( Base ` Y ) )
15 eqid 
 |-  ( +g ` ( ( ringLMod ` R ) ^s I ) ) = ( +g ` ( ( ringLMod ` R ) ^s I ) )
16 14 15 ressplusg 
 |-  ( ( Base ` Y ) e. _V -> ( +g ` ( ( ringLMod ` R ) ^s I ) ) = ( +g ` ( ( ( ringLMod ` R ) ^s I ) |`s ( Base ` Y ) ) ) )
17 13 16 ax-mp 
 |-  ( +g ` ( ( ringLMod ` R ) ^s I ) ) = ( +g ` ( ( ( ringLMod ` R ) ^s I ) |`s ( Base ` Y ) ) )
18 12 8 17 3eqtr4g 
 |-  ( ph -> .+b = ( +g ` ( ( ringLMod ` R ) ^s I ) ) )
19 18 oveqd 
 |-  ( ph -> ( F .+b G ) = ( F ( +g ` ( ( ringLMod ` R ) ^s I ) ) G ) )
20 eqid 
 |-  ( ( ringLMod ` R ) ^s I ) = ( ( ringLMod ` R ) ^s I )
21 eqid 
 |-  ( Base ` ( ( ringLMod ` R ) ^s I ) ) = ( Base ` ( ( ringLMod ` R ) ^s I ) )
22 fvexd 
 |-  ( ph -> ( ringLMod ` R ) e. _V )
23 1 2 frlmpws 
 |-  ( ( R e. V /\ I e. W ) -> Y = ( ( ( ringLMod ` R ) ^s I ) |`s B ) )
24 3 4 23 syl2anc 
 |-  ( ph -> Y = ( ( ( ringLMod ` R ) ^s I ) |`s B ) )
25 24 fveq2d 
 |-  ( ph -> ( Base ` Y ) = ( Base ` ( ( ( ringLMod ` R ) ^s I ) |`s B ) ) )
26 2 25 eqtrid 
 |-  ( ph -> B = ( Base ` ( ( ( ringLMod ` R ) ^s I ) |`s B ) ) )
27 eqid 
 |-  ( ( ( ringLMod ` R ) ^s I ) |`s B ) = ( ( ( ringLMod ` R ) ^s I ) |`s B )
28 27 21 ressbasss 
 |-  ( Base ` ( ( ( ringLMod ` R ) ^s I ) |`s B ) ) C_ ( Base ` ( ( ringLMod ` R ) ^s I ) )
29 26 28 eqsstrdi 
 |-  ( ph -> B C_ ( Base ` ( ( ringLMod ` R ) ^s I ) ) )
30 29 5 sseldd 
 |-  ( ph -> F e. ( Base ` ( ( ringLMod ` R ) ^s I ) ) )
31 29 6 sseldd 
 |-  ( ph -> G e. ( Base ` ( ( ringLMod ` R ) ^s I ) ) )
32 rlmplusg 
 |-  ( +g ` R ) = ( +g ` ( ringLMod ` R ) )
33 7 32 eqtri 
 |-  .+ = ( +g ` ( ringLMod ` R ) )
34 20 21 22 4 30 31 33 15 pwsplusgval 
 |-  ( ph -> ( F ( +g ` ( ( ringLMod ` R ) ^s I ) ) G ) = ( F oF .+ G ) )
35 19 34 eqtrd 
 |-  ( ph -> ( F .+b G ) = ( F oF .+ G ) )