Metamath Proof Explorer

Theorem gsumdixp

Description: Distribute a binary product of sums to a sum of binary products in a ring. (Contributed by Mario Carneiro, 8-Mar-2015) (Revised by AV, 10-Jul-2019)

Ref Expression
Hypotheses gsumdixp.b 
|- B = ( Base ` R )
gsumdixp.t 
|- .x. = ( .r ` R )
gsumdixp.z 
|- .0. = ( 0g ` R )
gsumdixp.i 
|- ( ph -> I e. V )
gsumdixp.j 
|- ( ph -> J e. W )
gsumdixp.r 
|- ( ph -> R e. Ring )
gsumdixp.x 
|- ( ( ph /\ x e. I ) -> X e. B )
gsumdixp.y 
|- ( ( ph /\ y e. J ) -> Y e. B )
gsumdixp.xf 
|- ( ph -> ( x e. I |-> X ) finSupp .0. )
gsumdixp.yf 
|- ( ph -> ( y e. J |-> Y ) finSupp .0. )
Assertion gsumdixp 
|- ( ph -> ( ( R gsum ( x e. I |-> X ) ) .x. ( R gsum ( y e. J |-> Y ) ) ) = ( R gsum ( x e. I , y e. J |-> ( X .x. Y ) ) ) )

Proof

Step Hyp Ref Expression
1 gsumdixp.b 
 |-  B = ( Base ` R )
2 gsumdixp.t 
 |-  .x. = ( .r ` R )
3 gsumdixp.z 
 |-  .0. = ( 0g ` R )
4 gsumdixp.i 
 |-  ( ph -> I e. V )
5 gsumdixp.j 
 |-  ( ph -> J e. W )
6 gsumdixp.r 
 |-  ( ph -> R e. Ring )
7 gsumdixp.x 
 |-  ( ( ph /\ x e. I ) -> X e. B )
8 gsumdixp.y 
 |-  ( ( ph /\ y e. J ) -> Y e. B )
9 gsumdixp.xf 
 |-  ( ph -> ( x e. I |-> X ) finSupp .0. )
10 gsumdixp.yf 
 |-  ( ph -> ( y e. J |-> Y ) finSupp .0. )
11 6 ringcmnd 
 |-  ( ph -> R e. CMnd )
12 5 adantr 
 |-  ( ( ph /\ i e. I ) -> J e. W )
13 6 adantr 
 |-  ( ( ph /\ ( i e. I /\ j e. J ) ) -> R e. Ring )
14 7 fmpttd 
 |-  ( ph -> ( x e. I |-> X ) : I --> B )
15 simpl 
 |-  ( ( i e. I /\ j e. J ) -> i e. I )
16 ffvelcdm 
 |-  ( ( ( x e. I |-> X ) : I --> B /\ i e. I ) -> ( ( x e. I |-> X ) ` i ) e. B )
17 14 15 16 syl2an 
 |-  ( ( ph /\ ( i e. I /\ j e. J ) ) -> ( ( x e. I |-> X ) ` i ) e. B )
18 8 fmpttd 
 |-  ( ph -> ( y e. J |-> Y ) : J --> B )
19 simpr 
 |-  ( ( i e. I /\ j e. J ) -> j e. J )
20 ffvelcdm 
 |-  ( ( ( y e. J |-> Y ) : J --> B /\ j e. J ) -> ( ( y e. J |-> Y ) ` j ) e. B )
21 18 19 20 syl2an 
 |-  ( ( ph /\ ( i e. I /\ j e. J ) ) -> ( ( y e. J |-> Y ) ` j ) e. B )
22 1 2 13 17 21 ringcld 
 |-  ( ( ph /\ ( i e. I /\ j e. J ) ) -> ( ( ( x e. I |-> X ) ` i ) .x. ( ( y e. J |-> Y ) ` j ) ) e. B )
23 9 fsuppimpd 
 |-  ( ph -> ( ( x e. I |-> X ) supp .0. ) e. Fin )
24 10 fsuppimpd 
 |-  ( ph -> ( ( y e. J |-> Y ) supp .0. ) e. Fin )
25 xpfi 
 |-  ( ( ( ( x e. I |-> X ) supp .0. ) e. Fin /\ ( ( y e. J |-> Y ) supp .0. ) e. Fin ) -> ( ( ( x e. I |-> X ) supp .0. ) X. ( ( y e. J |-> Y ) supp .0. ) ) e. Fin )
26 23 24 25 syl2anc 
 |-  ( ph -> ( ( ( x e. I |-> X ) supp .0. ) X. ( ( y e. J |-> Y ) supp .0. ) ) e. Fin )
27 ianor 
 |-  ( -. ( i e. ( ( x e. I |-> X ) supp .0. ) /\ j e. ( ( y e. J |-> Y ) supp .0. ) ) <-> ( -. i e. ( ( x e. I |-> X ) supp .0. ) \/ -. j e. ( ( y e. J |-> Y ) supp .0. ) ) )
28 brxp 
 |-  ( i ( ( ( x e. I |-> X ) supp .0. ) X. ( ( y e. J |-> Y ) supp .0. ) ) j <-> ( i e. ( ( x e. I |-> X ) supp .0. ) /\ j e. ( ( y e. J |-> Y ) supp .0. ) ) )
29 27 28 xchnxbir 
 |-  ( -. i ( ( ( x e. I |-> X ) supp .0. ) X. ( ( y e. J |-> Y ) supp .0. ) ) j <-> ( -. i e. ( ( x e. I |-> X ) supp .0. ) \/ -. j e. ( ( y e. J |-> Y ) supp .0. ) ) )
30 simprl 
 |-  ( ( ph /\ ( i e. I /\ j e. J ) ) -> i e. I )
31 eldif 
 |-  ( i e. ( I \ ( ( x e. I |-> X ) supp .0. ) ) <-> ( i e. I /\ -. i e. ( ( x e. I |-> X ) supp .0. ) ) )
32 31 biimpri 
 |-  ( ( i e. I /\ -. i e. ( ( x e. I |-> X ) supp .0. ) ) -> i e. ( I \ ( ( x e. I |-> X ) supp .0. ) ) )
33 30 32 sylan 
 |-  ( ( ( ph /\ ( i e. I /\ j e. J ) ) /\ -. i e. ( ( x e. I |-> X ) supp .0. ) ) -> i e. ( I \ ( ( x e. I |-> X ) supp .0. ) ) )
34 14 adantr 
 |-  ( ( ph /\ ( i e. I /\ j e. J ) ) -> ( x e. I |-> X ) : I --> B )
35 ssidd 
 |-  ( ( ph /\ ( i e. I /\ j e. J ) ) -> ( ( x e. I |-> X ) supp .0. ) C_ ( ( x e. I |-> X ) supp .0. ) )
36 4 adantr 
 |-  ( ( ph /\ ( i e. I /\ j e. J ) ) -> I e. V )
37 3 fvexi 
 |-  .0. e. _V
38 37 a1i 
 |-  ( ( ph /\ ( i e. I /\ j e. J ) ) -> .0. e. _V )
39 34 35 36 38 suppssr 
 |-  ( ( ( ph /\ ( i e. I /\ j e. J ) ) /\ i e. ( I \ ( ( x e. I |-> X ) supp .0. ) ) ) -> ( ( x e. I |-> X ) ` i ) = .0. )
40 33 39 syldan 
 |-  ( ( ( ph /\ ( i e. I /\ j e. J ) ) /\ -. i e. ( ( x e. I |-> X ) supp .0. ) ) -> ( ( x e. I |-> X ) ` i ) = .0. )
41 40 oveq1d 
 |-  ( ( ( ph /\ ( i e. I /\ j e. J ) ) /\ -. i e. ( ( x e. I |-> X ) supp .0. ) ) -> ( ( ( x e. I |-> X ) ` i ) .x. ( ( y e. J |-> Y ) ` j ) ) = ( .0. .x. ( ( y e. J |-> Y ) ` j ) ) )
42 1 2 3 ringlz 
 |-  ( ( R e. Ring /\ ( ( y e. J |-> Y ) ` j ) e. B ) -> ( .0. .x. ( ( y e. J |-> Y ) ` j ) ) = .0. )
43 13 21 42 syl2anc 
 |-  ( ( ph /\ ( i e. I /\ j e. J ) ) -> ( .0. .x. ( ( y e. J |-> Y ) ` j ) ) = .0. )
44 43 adantr 
 |-  ( ( ( ph /\ ( i e. I /\ j e. J ) ) /\ -. i e. ( ( x e. I |-> X ) supp .0. ) ) -> ( .0. .x. ( ( y e. J |-> Y ) ` j ) ) = .0. )
45 41 44 eqtrd 
 |-  ( ( ( ph /\ ( i e. I /\ j e. J ) ) /\ -. i e. ( ( x e. I |-> X ) supp .0. ) ) -> ( ( ( x e. I |-> X ) ` i ) .x. ( ( y e. J |-> Y ) ` j ) ) = .0. )
46 simprr 
 |-  ( ( ph /\ ( i e. I /\ j e. J ) ) -> j e. J )
47 eldif 
 |-  ( j e. ( J \ ( ( y e. J |-> Y ) supp .0. ) ) <-> ( j e. J /\ -. j e. ( ( y e. J |-> Y ) supp .0. ) ) )
48 47 biimpri 
 |-  ( ( j e. J /\ -. j e. ( ( y e. J |-> Y ) supp .0. ) ) -> j e. ( J \ ( ( y e. J |-> Y ) supp .0. ) ) )
49 46 48 sylan 
 |-  ( ( ( ph /\ ( i e. I /\ j e. J ) ) /\ -. j e. ( ( y e. J |-> Y ) supp .0. ) ) -> j e. ( J \ ( ( y e. J |-> Y ) supp .0. ) ) )
50 18 adantr 
 |-  ( ( ph /\ ( i e. I /\ j e. J ) ) -> ( y e. J |-> Y ) : J --> B )
51 ssidd 
 |-  ( ( ph /\ ( i e. I /\ j e. J ) ) -> ( ( y e. J |-> Y ) supp .0. ) C_ ( ( y e. J |-> Y ) supp .0. ) )
52 5 adantr 
 |-  ( ( ph /\ ( i e. I /\ j e. J ) ) -> J e. W )
53 50 51 52 38 suppssr 
 |-  ( ( ( ph /\ ( i e. I /\ j e. J ) ) /\ j e. ( J \ ( ( y e. J |-> Y ) supp .0. ) ) ) -> ( ( y e. J |-> Y ) ` j ) = .0. )
54 49 53 syldan 
 |-  ( ( ( ph /\ ( i e. I /\ j e. J ) ) /\ -. j e. ( ( y e. J |-> Y ) supp .0. ) ) -> ( ( y e. J |-> Y ) ` j ) = .0. )
55 54 oveq2d 
 |-  ( ( ( ph /\ ( i e. I /\ j e. J ) ) /\ -. j e. ( ( y e. J |-> Y ) supp .0. ) ) -> ( ( ( x e. I |-> X ) ` i ) .x. ( ( y e. J |-> Y ) ` j ) ) = ( ( ( x e. I |-> X ) ` i ) .x. .0. ) )
56 1 2 3 ringrz 
 |-  ( ( R e. Ring /\ ( ( x e. I |-> X ) ` i ) e. B ) -> ( ( ( x e. I |-> X ) ` i ) .x. .0. ) = .0. )
57 13 17 56 syl2anc 
 |-  ( ( ph /\ ( i e. I /\ j e. J ) ) -> ( ( ( x e. I |-> X ) ` i ) .x. .0. ) = .0. )
58 57 adantr 
 |-  ( ( ( ph /\ ( i e. I /\ j e. J ) ) /\ -. j e. ( ( y e. J |-> Y ) supp .0. ) ) -> ( ( ( x e. I |-> X ) ` i ) .x. .0. ) = .0. )
59 55 58 eqtrd 
 |-  ( ( ( ph /\ ( i e. I /\ j e. J ) ) /\ -. j e. ( ( y e. J |-> Y ) supp .0. ) ) -> ( ( ( x e. I |-> X ) ` i ) .x. ( ( y e. J |-> Y ) ` j ) ) = .0. )
60 45 59 jaodan 
 |-  ( ( ( ph /\ ( i e. I /\ j e. J ) ) /\ ( -. i e. ( ( x e. I |-> X ) supp .0. ) \/ -. j e. ( ( y e. J |-> Y ) supp .0. ) ) ) -> ( ( ( x e. I |-> X ) ` i ) .x. ( ( y e. J |-> Y ) ` j ) ) = .0. )
61 29 60 sylan2b 
 |-  ( ( ( ph /\ ( i e. I /\ j e. J ) ) /\ -. i ( ( ( x e. I |-> X ) supp .0. ) X. ( ( y e. J |-> Y ) supp .0. ) ) j ) -> ( ( ( x e. I |-> X ) ` i ) .x. ( ( y e. J |-> Y ) ` j ) ) = .0. )
62 61 anasss 
 |-  ( ( ph /\ ( ( i e. I /\ j e. J ) /\ -. i ( ( ( x e. I |-> X ) supp .0. ) X. ( ( y e. J |-> Y ) supp .0. ) ) j ) ) -> ( ( ( x e. I |-> X ) ` i ) .x. ( ( y e. J |-> Y ) ` j ) ) = .0. )
63 1 3 11 4 12 22 26 62 gsum2d2 
 |-  ( ph -> ( R gsum ( i e. I , j e. J |-> ( ( ( x e. I |-> X ) ` i ) .x. ( ( y e. J |-> Y ) ` j ) ) ) ) = ( R gsum ( i e. I |-> ( R gsum ( j e. J |-> ( ( ( x e. I |-> X ) ` i ) .x. ( ( y e. J |-> Y ) ` j ) ) ) ) ) ) )
64 nffvmpt1 
 |-  F/_ x ( ( x e. I |-> X ) ` i )
65 nfcv 
 |-  F/_ x .x.
66 nfcv 
 |-  F/_ x ( ( y e. J |-> Y ) ` j )
67 64 65 66 nfov 
 |-  F/_ x ( ( ( x e. I |-> X ) ` i ) .x. ( ( y e. J |-> Y ) ` j ) )
68 nfcv 
 |-  F/_ y ( ( x e. I |-> X ) ` i )
69 nfcv 
 |-  F/_ y .x.
70 nffvmpt1 
 |-  F/_ y ( ( y e. J |-> Y ) ` j )
71 68 69 70 nfov 
 |-  F/_ y ( ( ( x e. I |-> X ) ` i ) .x. ( ( y e. J |-> Y ) ` j ) )
72 nfcv 
 |-  F/_ i ( ( ( x e. I |-> X ) ` x ) .x. ( ( y e. J |-> Y ) ` y ) )
73 nfcv 
 |-  F/_ j ( ( ( x e. I |-> X ) ` x ) .x. ( ( y e. J |-> Y ) ` y ) )
74 fveq2 
 |-  ( i = x -> ( ( x e. I |-> X ) ` i ) = ( ( x e. I |-> X ) ` x ) )
75 fveq2 
 |-  ( j = y -> ( ( y e. J |-> Y ) ` j ) = ( ( y e. J |-> Y ) ` y ) )
76 74 75 oveqan12d 
 |-  ( ( i = x /\ j = y ) -> ( ( ( x e. I |-> X ) ` i ) .x. ( ( y e. J |-> Y ) ` j ) ) = ( ( ( x e. I |-> X ) ` x ) .x. ( ( y e. J |-> Y ) ` y ) ) )
77 67 71 72 73 76 cbvmpo 
 |-  ( i e. I , j e. J |-> ( ( ( x e. I |-> X ) ` i ) .x. ( ( y e. J |-> Y ) ` j ) ) ) = ( x e. I , y e. J |-> ( ( ( x e. I |-> X ) ` x ) .x. ( ( y e. J |-> Y ) ` y ) ) )
78 simp2 
 |-  ( ( ph /\ x e. I /\ y e. J ) -> x e. I )
79 7 3adant3 
 |-  ( ( ph /\ x e. I /\ y e. J ) -> X e. B )
80 eqid 
 |-  ( x e. I |-> X ) = ( x e. I |-> X )
81 80 fvmpt2 
 |-  ( ( x e. I /\ X e. B ) -> ( ( x e. I |-> X ) ` x ) = X )
82 78 79 81 syl2anc 
 |-  ( ( ph /\ x e. I /\ y e. J ) -> ( ( x e. I |-> X ) ` x ) = X )
83 simp3 
 |-  ( ( ph /\ x e. I /\ y e. J ) -> y e. J )
84 eqid 
 |-  ( y e. J |-> Y ) = ( y e. J |-> Y )
85 84 fvmpt2 
 |-  ( ( y e. J /\ Y e. B ) -> ( ( y e. J |-> Y ) ` y ) = Y )
86 83 8 85 3imp3i2an 
 |-  ( ( ph /\ x e. I /\ y e. J ) -> ( ( y e. J |-> Y ) ` y ) = Y )
87 82 86 oveq12d 
 |-  ( ( ph /\ x e. I /\ y e. J ) -> ( ( ( x e. I |-> X ) ` x ) .x. ( ( y e. J |-> Y ) ` y ) ) = ( X .x. Y ) )
88 87 mpoeq3dva 
 |-  ( ph -> ( x e. I , y e. J |-> ( ( ( x e. I |-> X ) ` x ) .x. ( ( y e. J |-> Y ) ` y ) ) ) = ( x e. I , y e. J |-> ( X .x. Y ) ) )
89 77 88 eqtrid 
 |-  ( ph -> ( i e. I , j e. J |-> ( ( ( x e. I |-> X ) ` i ) .x. ( ( y e. J |-> Y ) ` j ) ) ) = ( x e. I , y e. J |-> ( X .x. Y ) ) )
90 89 oveq2d 
 |-  ( ph -> ( R gsum ( i e. I , j e. J |-> ( ( ( x e. I |-> X ) ` i ) .x. ( ( y e. J |-> Y ) ` j ) ) ) ) = ( R gsum ( x e. I , y e. J |-> ( X .x. Y ) ) ) )
91 nfcv 
 |-  F/_ x R
92 nfcv 
 |-  F/_ x gsum
93 nfcv 
 |-  F/_ x J
94 93 67 nfmpt 
 |-  F/_ x ( j e. J |-> ( ( ( x e. I |-> X ) ` i ) .x. ( ( y e. J |-> Y ) ` j ) ) )
95 91 92 94 nfov 
 |-  F/_ x ( R gsum ( j e. J |-> ( ( ( x e. I |-> X ) ` i ) .x. ( ( y e. J |-> Y ) ` j ) ) ) )
96 nfcv 
 |-  F/_ i ( R gsum ( y e. J |-> ( ( ( x e. I |-> X ) ` x ) .x. ( ( y e. J |-> Y ) ` y ) ) ) )
97 74 oveq1d 
 |-  ( i = x -> ( ( ( x e. I |-> X ) ` i ) .x. ( ( y e. J |-> Y ) ` j ) ) = ( ( ( x e. I |-> X ) ` x ) .x. ( ( y e. J |-> Y ) ` j ) ) )
98 97 mpteq2dv 
 |-  ( i = x -> ( j e. J |-> ( ( ( x e. I |-> X ) ` i ) .x. ( ( y e. J |-> Y ) ` j ) ) ) = ( j e. J |-> ( ( ( x e. I |-> X ) ` x ) .x. ( ( y e. J |-> Y ) ` j ) ) ) )
99 nfcv 
 |-  F/_ y ( ( x e. I |-> X ) ` x )
100 99 69 70 nfov 
 |-  F/_ y ( ( ( x e. I |-> X ) ` x ) .x. ( ( y e. J |-> Y ) ` j ) )
101 75 oveq2d 
 |-  ( j = y -> ( ( ( x e. I |-> X ) ` x ) .x. ( ( y e. J |-> Y ) ` j ) ) = ( ( ( x e. I |-> X ) ` x ) .x. ( ( y e. J |-> Y ) ` y ) ) )
102 100 73 101 cbvmpt 
 |-  ( j e. J |-> ( ( ( x e. I |-> X ) ` x ) .x. ( ( y e. J |-> Y ) ` j ) ) ) = ( y e. J |-> ( ( ( x e. I |-> X ) ` x ) .x. ( ( y e. J |-> Y ) ` y ) ) )
103 98 102 eqtrdi 
 |-  ( i = x -> ( j e. J |-> ( ( ( x e. I |-> X ) ` i ) .x. ( ( y e. J |-> Y ) ` j ) ) ) = ( y e. J |-> ( ( ( x e. I |-> X ) ` x ) .x. ( ( y e. J |-> Y ) ` y ) ) ) )
104 103 oveq2d 
 |-  ( i = x -> ( R gsum ( j e. J |-> ( ( ( x e. I |-> X ) ` i ) .x. ( ( y e. J |-> Y ) ` j ) ) ) ) = ( R gsum ( y e. J |-> ( ( ( x e. I |-> X ) ` x ) .x. ( ( y e. J |-> Y ) ` y ) ) ) ) )
105 95 96 104 cbvmpt 
 |-  ( i e. I |-> ( R gsum ( j e. J |-> ( ( ( x e. I |-> X ) ` i ) .x. ( ( y e. J |-> Y ) ` j ) ) ) ) ) = ( x e. I |-> ( R gsum ( y e. J |-> ( ( ( x e. I |-> X ) ` x ) .x. ( ( y e. J |-> Y ) ` y ) ) ) ) )
106 87 3expa 
 |-  ( ( ( ph /\ x e. I ) /\ y e. J ) -> ( ( ( x e. I |-> X ) ` x ) .x. ( ( y e. J |-> Y ) ` y ) ) = ( X .x. Y ) )
107 106 mpteq2dva 
 |-  ( ( ph /\ x e. I ) -> ( y e. J |-> ( ( ( x e. I |-> X ) ` x ) .x. ( ( y e. J |-> Y ) ` y ) ) ) = ( y e. J |-> ( X .x. Y ) ) )
108 107 oveq2d 
 |-  ( ( ph /\ x e. I ) -> ( R gsum ( y e. J |-> ( ( ( x e. I |-> X ) ` x ) .x. ( ( y e. J |-> Y ) ` y ) ) ) ) = ( R gsum ( y e. J |-> ( X .x. Y ) ) ) )
109 108 mpteq2dva 
 |-  ( ph -> ( x e. I |-> ( R gsum ( y e. J |-> ( ( ( x e. I |-> X ) ` x ) .x. ( ( y e. J |-> Y ) ` y ) ) ) ) ) = ( x e. I |-> ( R gsum ( y e. J |-> ( X .x. Y ) ) ) ) )
110 105 109 eqtrid 
 |-  ( ph -> ( i e. I |-> ( R gsum ( j e. J |-> ( ( ( x e. I |-> X ) ` i ) .x. ( ( y e. J |-> Y ) ` j ) ) ) ) ) = ( x e. I |-> ( R gsum ( y e. J |-> ( X .x. Y ) ) ) ) )
111 110 oveq2d 
 |-  ( ph -> ( R gsum ( i e. I |-> ( R gsum ( j e. J |-> ( ( ( x e. I |-> X ) ` i ) .x. ( ( y e. J |-> Y ) ` j ) ) ) ) ) ) = ( R gsum ( x e. I |-> ( R gsum ( y e. J |-> ( X .x. Y ) ) ) ) ) )
112 63 90 111 3eqtr3d 
 |-  ( ph -> ( R gsum ( x e. I , y e. J |-> ( X .x. Y ) ) ) = ( R gsum ( x e. I |-> ( R gsum ( y e. J |-> ( X .x. Y ) ) ) ) ) )
113 6 adantr 
 |-  ( ( ph /\ x e. I ) -> R e. Ring )
114 5 adantr 
 |-  ( ( ph /\ x e. I ) -> J e. W )
115 8 adantlr 
 |-  ( ( ( ph /\ x e. I ) /\ y e. J ) -> Y e. B )
116 10 adantr 
 |-  ( ( ph /\ x e. I ) -> ( y e. J |-> Y ) finSupp .0. )
117 1 3 2 113 114 7 115 116 gsummulc2 
 |-  ( ( ph /\ x e. I ) -> ( R gsum ( y e. J |-> ( X .x. Y ) ) ) = ( X .x. ( R gsum ( y e. J |-> Y ) ) ) )
118 117 mpteq2dva 
 |-  ( ph -> ( x e. I |-> ( R gsum ( y e. J |-> ( X .x. Y ) ) ) ) = ( x e. I |-> ( X .x. ( R gsum ( y e. J |-> Y ) ) ) ) )
119 118 oveq2d 
 |-  ( ph -> ( R gsum ( x e. I |-> ( R gsum ( y e. J |-> ( X .x. Y ) ) ) ) ) = ( R gsum ( x e. I |-> ( X .x. ( R gsum ( y e. J |-> Y ) ) ) ) ) )
120 1 3 11 5 18 10 gsumcl 
 |-  ( ph -> ( R gsum ( y e. J |-> Y ) ) e. B )
121 1 3 2 6 4 120 7 9 gsummulc1 
 |-  ( ph -> ( R gsum ( x e. I |-> ( X .x. ( R gsum ( y e. J |-> Y ) ) ) ) ) = ( ( R gsum ( x e. I |-> X ) ) .x. ( R gsum ( y e. J |-> Y ) ) ) )
122 112 119 121 3eqtrrd 
 |-  ( ph -> ( ( R gsum ( x e. I |-> X ) ) .x. ( R gsum ( y e. J |-> Y ) ) ) = ( R gsum ( x e. I , y e. J |-> ( X .x. Y ) ) ) )