Metamath Proof Explorer

Theorem frlmgsum

Description: Finite commutative sums in a free module are taken componentwise. (Contributed by Stefan O'Rear, 1-Feb-2015) (Revised by Mario Carneiro, 5-Jul-2015) (Revised by AV, 23-Jun-2019)

Ref Expression
Hypotheses frlmgsum.y 
|- Y = ( R freeLMod I )
frlmgsum.b 
|- B = ( Base ` Y )
frlmgsum.z 
|- .0. = ( 0g ` Y )
frlmgsum.i 
|- ( ph -> I e. V )
frlmgsum.j 
|- ( ph -> J e. W )
frlmgsum.r 
|- ( ph -> R e. Ring )
frlmgsum.f 
|- ( ( ph /\ y e. J ) -> ( x e. I |-> U ) e. B )
frlmgsum.w 
|- ( ph -> ( y e. J |-> ( x e. I |-> U ) ) finSupp .0. )
Assertion frlmgsum 
|- ( ph -> ( Y gsum ( y e. J |-> ( x e. I |-> U ) ) ) = ( x e. I |-> ( R gsum ( y e. J |-> U ) ) ) )

Proof

Step Hyp Ref Expression
1 frlmgsum.y 
 |-  Y = ( R freeLMod I )
2 frlmgsum.b 
 |-  B = ( Base ` Y )
3 frlmgsum.z 
 |-  .0. = ( 0g ` Y )
4 frlmgsum.i 
 |-  ( ph -> I e. V )
5 frlmgsum.j 
 |-  ( ph -> J e. W )
6 frlmgsum.r 
 |-  ( ph -> R e. Ring )
7 frlmgsum.f 
 |-  ( ( ph /\ y e. J ) -> ( x e. I |-> U ) e. B )
8 frlmgsum.w 
 |-  ( ph -> ( y e. J |-> ( x e. I |-> U ) ) finSupp .0. )
9 1 2 frlmpws 
 |-  ( ( R e. Ring /\ I e. V ) -> Y = ( ( ( ringLMod ` R ) ^s I ) |`s B ) )
10 6 4 9 syl2anc 
 |-  ( ph -> Y = ( ( ( ringLMod ` R ) ^s I ) |`s B ) )
11 10 oveq1d 
 |-  ( ph -> ( Y gsum ( y e. J |-> ( x e. I |-> U ) ) ) = ( ( ( ( ringLMod ` R ) ^s I ) |`s B ) gsum ( y e. J |-> ( x e. I |-> U ) ) ) )
12 eqid 
 |-  ( Base ` ( ( ringLMod ` R ) ^s I ) ) = ( Base ` ( ( ringLMod ` R ) ^s I ) )
13 eqid 
 |-  ( +g ` ( ( ringLMod ` R ) ^s I ) ) = ( +g ` ( ( ringLMod ` R ) ^s I ) )
14 eqid 
 |-  ( ( ( ringLMod ` R ) ^s I ) |`s B ) = ( ( ( ringLMod ` R ) ^s I ) |`s B )
15 ovexd 
 |-  ( ph -> ( ( ringLMod ` R ) ^s I ) e. _V )
16 eqid 
 |-  ( LSubSp ` ( ( ringLMod ` R ) ^s I ) ) = ( LSubSp ` ( ( ringLMod ` R ) ^s I ) )
17 1 2 16 frlmlss 
 |-  ( ( R e. Ring /\ I e. V ) -> B e. ( LSubSp ` ( ( ringLMod ` R ) ^s I ) ) )
18 6 4 17 syl2anc 
 |-  ( ph -> B e. ( LSubSp ` ( ( ringLMod ` R ) ^s I ) ) )
19 12 16 lssss 
 |-  ( B e. ( LSubSp ` ( ( ringLMod ` R ) ^s I ) ) -> B C_ ( Base ` ( ( ringLMod ` R ) ^s I ) ) )
20 18 19 syl 
 |-  ( ph -> B C_ ( Base ` ( ( ringLMod ` R ) ^s I ) ) )
21 7 fmpttd 
 |-  ( ph -> ( y e. J |-> ( x e. I |-> U ) ) : J --> B )
22 rlmlmod 
 |-  ( R e. Ring -> ( ringLMod ` R ) e. LMod )
23 6 22 syl 
 |-  ( ph -> ( ringLMod ` R ) e. LMod )
24 eqid 
 |-  ( ( ringLMod ` R ) ^s I ) = ( ( ringLMod ` R ) ^s I )
25 24 pwslmod 
 |-  ( ( ( ringLMod ` R ) e. LMod /\ I e. V ) -> ( ( ringLMod ` R ) ^s I ) e. LMod )
26 23 4 25 syl2anc 
 |-  ( ph -> ( ( ringLMod ` R ) ^s I ) e. LMod )
27 eqid 
 |-  ( 0g ` ( ( ringLMod ` R ) ^s I ) ) = ( 0g ` ( ( ringLMod ` R ) ^s I ) )
28 27 16 lss0cl 
 |-  ( ( ( ( ringLMod ` R ) ^s I ) e. LMod /\ B e. ( LSubSp ` ( ( ringLMod ` R ) ^s I ) ) ) -> ( 0g ` ( ( ringLMod ` R ) ^s I ) ) e. B )
29 26 18 28 syl2anc 
 |-  ( ph -> ( 0g ` ( ( ringLMod ` R ) ^s I ) ) e. B )
30 lmodcmn 
 |-  ( ( ringLMod ` R ) e. LMod -> ( ringLMod ` R ) e. CMnd )
31 23 30 syl 
 |-  ( ph -> ( ringLMod ` R ) e. CMnd )
32 cmnmnd 
 |-  ( ( ringLMod ` R ) e. CMnd -> ( ringLMod ` R ) e. Mnd )
33 31 32 syl 
 |-  ( ph -> ( ringLMod ` R ) e. Mnd )
34 24 pwsmnd 
 |-  ( ( ( ringLMod ` R ) e. Mnd /\ I e. V ) -> ( ( ringLMod ` R ) ^s I ) e. Mnd )
35 33 4 34 syl2anc 
 |-  ( ph -> ( ( ringLMod ` R ) ^s I ) e. Mnd )
36 12 13 27 mndlrid 
 |-  ( ( ( ( ringLMod ` R ) ^s I ) e. Mnd /\ x e. ( Base ` ( ( ringLMod ` R ) ^s I ) ) ) -> ( ( ( 0g ` ( ( ringLMod ` R ) ^s I ) ) ( +g ` ( ( ringLMod ` R ) ^s I ) ) x ) = x /\ ( x ( +g ` ( ( ringLMod ` R ) ^s I ) ) ( 0g ` ( ( ringLMod ` R ) ^s I ) ) ) = x ) )
37 35 36 sylan 
 |-  ( ( ph /\ x e. ( Base ` ( ( ringLMod ` R ) ^s I ) ) ) -> ( ( ( 0g ` ( ( ringLMod ` R ) ^s I ) ) ( +g ` ( ( ringLMod ` R ) ^s I ) ) x ) = x /\ ( x ( +g ` ( ( ringLMod ` R ) ^s I ) ) ( 0g ` ( ( ringLMod ` R ) ^s I ) ) ) = x ) )
38 12 13 14 15 5 20 21 29 37 gsumress 
 |-  ( ph -> ( ( ( ringLMod ` R ) ^s I ) gsum ( y e. J |-> ( x e. I |-> U ) ) ) = ( ( ( ( ringLMod ` R ) ^s I ) |`s B ) gsum ( y e. J |-> ( x e. I |-> U ) ) ) )
39 rlmbas 
 |-  ( Base ` R ) = ( Base ` ( ringLMod ` R ) )
40 eqid 
 |-  ( Base ` R ) = ( Base ` R )
41 1 40 2 frlmbasf 
 |-  ( ( I e. V /\ ( x e. I |-> U ) e. B ) -> ( x e. I |-> U ) : I --> ( Base ` R ) )
42 4 7 41 syl2an2r 
 |-  ( ( ph /\ y e. J ) -> ( x e. I |-> U ) : I --> ( Base ` R ) )
43 42 fvmptelrn 
 |-  ( ( ( ph /\ y e. J ) /\ x e. I ) -> U e. ( Base ` R ) )
44 43 an32s 
 |-  ( ( ( ph /\ x e. I ) /\ y e. J ) -> U e. ( Base ` R ) )
45 44 anasss 
 |-  ( ( ph /\ ( x e. I /\ y e. J ) ) -> U e. ( Base ` R ) )
46 10 fveq2d 
 |-  ( ph -> ( 0g ` Y ) = ( 0g ` ( ( ( ringLMod ` R ) ^s I ) |`s B ) ) )
47 16 lsssubg 
 |-  ( ( ( ( ringLMod ` R ) ^s I ) e. LMod /\ B e. ( LSubSp ` ( ( ringLMod ` R ) ^s I ) ) ) -> B e. ( SubGrp ` ( ( ringLMod ` R ) ^s I ) ) )
48 26 18 47 syl2anc 
 |-  ( ph -> B e. ( SubGrp ` ( ( ringLMod ` R ) ^s I ) ) )
49 14 27 subg0 
 |-  ( B e. ( SubGrp ` ( ( ringLMod ` R ) ^s I ) ) -> ( 0g ` ( ( ringLMod ` R ) ^s I ) ) = ( 0g ` ( ( ( ringLMod ` R ) ^s I ) |`s B ) ) )
50 48 49 syl 
 |-  ( ph -> ( 0g ` ( ( ringLMod ` R ) ^s I ) ) = ( 0g ` ( ( ( ringLMod ` R ) ^s I ) |`s B ) ) )
51 46 50 eqtr4d 
 |-  ( ph -> ( 0g ` Y ) = ( 0g ` ( ( ringLMod ` R ) ^s I ) ) )
52 3 51 syl5eq 
 |-  ( ph -> .0. = ( 0g ` ( ( ringLMod ` R ) ^s I ) ) )
53 8 52 breqtrd 
 |-  ( ph -> ( y e. J |-> ( x e. I |-> U ) ) finSupp ( 0g ` ( ( ringLMod ` R ) ^s I ) ) )
54 24 39 27 4 5 31 45 53 pwsgsum 
 |-  ( ph -> ( ( ( ringLMod ` R ) ^s I ) gsum ( y e. J |-> ( x e. I |-> U ) ) ) = ( x e. I |-> ( ( ringLMod ` R ) gsum ( y e. J |-> U ) ) ) )
55 5 mptexd 
 |-  ( ph -> ( y e. J |-> U ) e. _V )
56 fvexd 
 |-  ( ph -> ( ringLMod ` R ) e. _V )
57 39 a1i 
 |-  ( ph -> ( Base ` R ) = ( Base ` ( ringLMod ` R ) ) )
58 rlmplusg 
 |-  ( +g ` R ) = ( +g ` ( ringLMod ` R ) )
59 58 a1i 
 |-  ( ph -> ( +g ` R ) = ( +g ` ( ringLMod ` R ) ) )
60 55 6 56 57 59 gsumpropd 
 |-  ( ph -> ( R gsum ( y e. J |-> U ) ) = ( ( ringLMod ` R ) gsum ( y e. J |-> U ) ) )
61 60 mpteq2dv 
 |-  ( ph -> ( x e. I |-> ( R gsum ( y e. J |-> U ) ) ) = ( x e. I |-> ( ( ringLMod ` R ) gsum ( y e. J |-> U ) ) ) )
62 54 61 eqtr4d 
 |-  ( ph -> ( ( ( ringLMod ` R ) ^s I ) gsum ( y e. J |-> ( x e. I |-> U ) ) ) = ( x e. I |-> ( R gsum ( y e. J |-> U ) ) ) )
63 11 38 62 3eqtr2d 
 |-  ( ph -> ( Y gsum ( y e. J |-> ( x e. I |-> U ) ) ) = ( x e. I |-> ( R gsum ( y e. J |-> U ) ) ) )