Metamath Proof Explorer

Theorem matgsum

Description: Finite commutative sums in a matrix algebra are taken componentwise. (Contributed by AV, 26-Sep-2019)

Ref Expression
Hypotheses matgsum.a 
|- A = ( N Mat R )
matgsum.b 
|- B = ( Base ` A )
matgsum.z 
|- .0. = ( 0g ` A )
matgsum.i 
|- ( ph -> N e. Fin )
matgsum.j 
|- ( ph -> J e. W )
matgsum.r 
|- ( ph -> R e. Ring )
matgsum.f 
|- ( ( ph /\ y e. J ) -> ( i e. N , j e. N |-> U ) e. B )
matgsum.w 
|- ( ph -> ( y e. J |-> ( i e. N , j e. N |-> U ) ) finSupp .0. )
Assertion matgsum 
|- ( ph -> ( A gsum ( y e. J |-> ( i e. N , j e. N |-> U ) ) ) = ( i e. N , j e. N |-> ( R gsum ( y e. J |-> U ) ) ) )

Proof

Step Hyp Ref Expression
1 matgsum.a 
 |-  A = ( N Mat R )
2 matgsum.b 
 |-  B = ( Base ` A )
3 matgsum.z 
 |-  .0. = ( 0g ` A )
4 matgsum.i 
 |-  ( ph -> N e. Fin )
5 matgsum.j 
 |-  ( ph -> J e. W )
6 matgsum.r 
 |-  ( ph -> R e. Ring )
7 matgsum.f 
 |-  ( ( ph /\ y e. J ) -> ( i e. N , j e. N |-> U ) e. B )
8 matgsum.w 
 |-  ( ph -> ( y e. J |-> ( i e. N , j e. N |-> U ) ) finSupp .0. )
9 5 mptexd 
 |-  ( ph -> ( y e. J |-> ( i e. N , j e. N |-> U ) ) e. _V )
10 1 ovexi 
 |-  A e. _V
11 10 a1i 
 |-  ( ph -> A e. _V )
12 ovexd 
 |-  ( ph -> ( R freeLMod ( N X. N ) ) e. _V )
13 eqid 
 |-  ( R freeLMod ( N X. N ) ) = ( R freeLMod ( N X. N ) )
14 1 13 matbas 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( Base ` ( R freeLMod ( N X. N ) ) ) = ( Base ` A ) )
15 4 6 14 syl2anc 
 |-  ( ph -> ( Base ` ( R freeLMod ( N X. N ) ) ) = ( Base ` A ) )
16 15 eqcomd 
 |-  ( ph -> ( Base ` A ) = ( Base ` ( R freeLMod ( N X. N ) ) ) )
17 1 13 matplusg 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( +g ` ( R freeLMod ( N X. N ) ) ) = ( +g ` A ) )
18 4 6 17 syl2anc 
 |-  ( ph -> ( +g ` ( R freeLMod ( N X. N ) ) ) = ( +g ` A ) )
19 18 eqcomd 
 |-  ( ph -> ( +g ` A ) = ( +g ` ( R freeLMod ( N X. N ) ) ) )
20 9 11 12 16 19 gsumpropd 
 |-  ( ph -> ( A gsum ( y e. J |-> ( i e. N , j e. N |-> U ) ) ) = ( ( R freeLMod ( N X. N ) ) gsum ( y e. J |-> ( i e. N , j e. N |-> U ) ) ) )
21 mpompts 
 |-  ( i e. N , j e. N |-> U ) = ( z e. ( N X. N ) |-> [_ ( 1st ` z ) / i ]_ [_ ( 2nd ` z ) / j ]_ U )
22 21 a1i 
 |-  ( ph -> ( i e. N , j e. N |-> U ) = ( z e. ( N X. N ) |-> [_ ( 1st ` z ) / i ]_ [_ ( 2nd ` z ) / j ]_ U ) )
23 22 mpteq2dv 
 |-  ( ph -> ( y e. J |-> ( i e. N , j e. N |-> U ) ) = ( y e. J |-> ( z e. ( N X. N ) |-> [_ ( 1st ` z ) / i ]_ [_ ( 2nd ` z ) / j ]_ U ) ) )
24 23 oveq2d 
 |-  ( ph -> ( ( R freeLMod ( N X. N ) ) gsum ( y e. J |-> ( i e. N , j e. N |-> U ) ) ) = ( ( R freeLMod ( N X. N ) ) gsum ( y e. J |-> ( z e. ( N X. N ) |-> [_ ( 1st ` z ) / i ]_ [_ ( 2nd ` z ) / j ]_ U ) ) ) )
25 eqid 
 |-  ( Base ` ( R freeLMod ( N X. N ) ) ) = ( Base ` ( R freeLMod ( N X. N ) ) )
26 eqid 
 |-  ( 0g ` ( R freeLMod ( N X. N ) ) ) = ( 0g ` ( R freeLMod ( N X. N ) ) )
27 xpfi 
 |-  ( ( N e. Fin /\ N e. Fin ) -> ( N X. N ) e. Fin )
28 4 4 27 syl2anc 
 |-  ( ph -> ( N X. N ) e. Fin )
29 7 2 eleqtrdi 
 |-  ( ( ph /\ y e. J ) -> ( i e. N , j e. N |-> U ) e. ( Base ` A ) )
30 21 eqcomi 
 |-  ( z e. ( N X. N ) |-> [_ ( 1st ` z ) / i ]_ [_ ( 2nd ` z ) / j ]_ U ) = ( i e. N , j e. N |-> U )
31 30 a1i 
 |-  ( ( ph /\ y e. J ) -> ( z e. ( N X. N ) |-> [_ ( 1st ` z ) / i ]_ [_ ( 2nd ` z ) / j ]_ U ) = ( i e. N , j e. N |-> U ) )
32 4 6 jca 
 |-  ( ph -> ( N e. Fin /\ R e. Ring ) )
33 32 adantr 
 |-  ( ( ph /\ y e. J ) -> ( N e. Fin /\ R e. Ring ) )
34 33 14 syl 
 |-  ( ( ph /\ y e. J ) -> ( Base ` ( R freeLMod ( N X. N ) ) ) = ( Base ` A ) )
35 29 31 34 3eltr4d 
 |-  ( ( ph /\ y e. J ) -> ( z e. ( N X. N ) |-> [_ ( 1st ` z ) / i ]_ [_ ( 2nd ` z ) / j ]_ U ) e. ( Base ` ( R freeLMod ( N X. N ) ) ) )
36 30 mpteq2i 
 |-  ( y e. J |-> ( z e. ( N X. N ) |-> [_ ( 1st ` z ) / i ]_ [_ ( 2nd ` z ) / j ]_ U ) ) = ( y e. J |-> ( i e. N , j e. N |-> U ) )
37 3 eqcomi 
 |-  ( 0g ` A ) = .0.
38 8 36 37 3brtr4g 
 |-  ( ph -> ( y e. J |-> ( z e. ( N X. N ) |-> [_ ( 1st ` z ) / i ]_ [_ ( 2nd ` z ) / j ]_ U ) ) finSupp ( 0g ` A ) )
39 1 13 mat0 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( 0g ` ( R freeLMod ( N X. N ) ) ) = ( 0g ` A ) )
40 4 6 39 syl2anc 
 |-  ( ph -> ( 0g ` ( R freeLMod ( N X. N ) ) ) = ( 0g ` A ) )
41 38 40 breqtrrd 
 |-  ( ph -> ( y e. J |-> ( z e. ( N X. N ) |-> [_ ( 1st ` z ) / i ]_ [_ ( 2nd ` z ) / j ]_ U ) ) finSupp ( 0g ` ( R freeLMod ( N X. N ) ) ) )
42 13 25 26 28 5 6 35 41 frlmgsum 
 |-  ( ph -> ( ( R freeLMod ( N X. N ) ) gsum ( y e. J |-> ( z e. ( N X. N ) |-> [_ ( 1st ` z ) / i ]_ [_ ( 2nd ` z ) / j ]_ U ) ) ) = ( z e. ( N X. N ) |-> ( R gsum ( y e. J |-> [_ ( 1st ` z ) / i ]_ [_ ( 2nd ` z ) / j ]_ U ) ) ) )
43 24 42 eqtrd 
 |-  ( ph -> ( ( R freeLMod ( N X. N ) ) gsum ( y e. J |-> ( i e. N , j e. N |-> U ) ) ) = ( z e. ( N X. N ) |-> ( R gsum ( y e. J |-> [_ ( 1st ` z ) / i ]_ [_ ( 2nd ` z ) / j ]_ U ) ) ) )
44 fvex 
 |-  ( 2nd ` z ) e. _V
45 csbov2g 
 |-  ( ( 2nd ` z ) e. _V -> [_ ( 2nd ` z ) / j ]_ ( R gsum ( y e. J |-> U ) ) = ( R gsum [_ ( 2nd ` z ) / j ]_ ( y e. J |-> U ) ) )
46 44 45 ax-mp 
 |-  [_ ( 2nd ` z ) / j ]_ ( R gsum ( y e. J |-> U ) ) = ( R gsum [_ ( 2nd ` z ) / j ]_ ( y e. J |-> U ) )
47 46 csbeq2i 
 |-  [_ ( 1st ` z ) / i ]_ [_ ( 2nd ` z ) / j ]_ ( R gsum ( y e. J |-> U ) ) = [_ ( 1st ` z ) / i ]_ ( R gsum [_ ( 2nd ` z ) / j ]_ ( y e. J |-> U ) )
48 fvex 
 |-  ( 1st ` z ) e. _V
49 csbov2g 
 |-  ( ( 1st ` z ) e. _V -> [_ ( 1st ` z ) / i ]_ ( R gsum [_ ( 2nd ` z ) / j ]_ ( y e. J |-> U ) ) = ( R gsum [_ ( 1st ` z ) / i ]_ [_ ( 2nd ` z ) / j ]_ ( y e. J |-> U ) ) )
50 48 49 ax-mp 
 |-  [_ ( 1st ` z ) / i ]_ ( R gsum [_ ( 2nd ` z ) / j ]_ ( y e. J |-> U ) ) = ( R gsum [_ ( 1st ` z ) / i ]_ [_ ( 2nd ` z ) / j ]_ ( y e. J |-> U ) )
51 csbmpt2 
 |-  ( ( 2nd ` z ) e. _V -> [_ ( 2nd ` z ) / j ]_ ( y e. J |-> U ) = ( y e. J |-> [_ ( 2nd ` z ) / j ]_ U ) )
52 44 51 ax-mp 
 |-  [_ ( 2nd ` z ) / j ]_ ( y e. J |-> U ) = ( y e. J |-> [_ ( 2nd ` z ) / j ]_ U )
53 52 csbeq2i 
 |-  [_ ( 1st ` z ) / i ]_ [_ ( 2nd ` z ) / j ]_ ( y e. J |-> U ) = [_ ( 1st ` z ) / i ]_ ( y e. J |-> [_ ( 2nd ` z ) / j ]_ U )
54 csbmpt2 
 |-  ( ( 1st ` z ) e. _V -> [_ ( 1st ` z ) / i ]_ ( y e. J |-> [_ ( 2nd ` z ) / j ]_ U ) = ( y e. J |-> [_ ( 1st ` z ) / i ]_ [_ ( 2nd ` z ) / j ]_ U ) )
55 48 54 ax-mp 
 |-  [_ ( 1st ` z ) / i ]_ ( y e. J |-> [_ ( 2nd ` z ) / j ]_ U ) = ( y e. J |-> [_ ( 1st ` z ) / i ]_ [_ ( 2nd ` z ) / j ]_ U )
56 53 55 eqtri 
 |-  [_ ( 1st ` z ) / i ]_ [_ ( 2nd ` z ) / j ]_ ( y e. J |-> U ) = ( y e. J |-> [_ ( 1st ` z ) / i ]_ [_ ( 2nd ` z ) / j ]_ U )
57 56 oveq2i 
 |-  ( R gsum [_ ( 1st ` z ) / i ]_ [_ ( 2nd ` z ) / j ]_ ( y e. J |-> U ) ) = ( R gsum ( y e. J |-> [_ ( 1st ` z ) / i ]_ [_ ( 2nd ` z ) / j ]_ U ) )
58 47 50 57 3eqtrri 
 |-  ( R gsum ( y e. J |-> [_ ( 1st ` z ) / i ]_ [_ ( 2nd ` z ) / j ]_ U ) ) = [_ ( 1st ` z ) / i ]_ [_ ( 2nd ` z ) / j ]_ ( R gsum ( y e. J |-> U ) )
59 58 mpteq2i 
 |-  ( z e. ( N X. N ) |-> ( R gsum ( y e. J |-> [_ ( 1st ` z ) / i ]_ [_ ( 2nd ` z ) / j ]_ U ) ) ) = ( z e. ( N X. N ) |-> [_ ( 1st ` z ) / i ]_ [_ ( 2nd ` z ) / j ]_ ( R gsum ( y e. J |-> U ) ) )
60 mpompts 
 |-  ( i e. N , j e. N |-> ( R gsum ( y e. J |-> U ) ) ) = ( z e. ( N X. N ) |-> [_ ( 1st ` z ) / i ]_ [_ ( 2nd ` z ) / j ]_ ( R gsum ( y e. J |-> U ) ) )
61 59 60 eqtr4i 
 |-  ( z e. ( N X. N ) |-> ( R gsum ( y e. J |-> [_ ( 1st ` z ) / i ]_ [_ ( 2nd ` z ) / j ]_ U ) ) ) = ( i e. N , j e. N |-> ( R gsum ( y e. J |-> U ) ) )
62 61 a1i 
 |-  ( ph -> ( z e. ( N X. N ) |-> ( R gsum ( y e. J |-> [_ ( 1st ` z ) / i ]_ [_ ( 2nd ` z ) / j ]_ U ) ) ) = ( i e. N , j e. N |-> ( R gsum ( y e. J |-> U ) ) ) )
63 20 43 62 3eqtrd 
 |-  ( ph -> ( A gsum ( y e. J |-> ( i e. N , j e. N |-> U ) ) ) = ( i e. N , j e. N |-> ( R gsum ( y e. J |-> U ) ) ) )