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 ringcmn 
 |-  ( R e. Ring -> R e. CMnd )
12 6 11 syl 
 |-  ( ph -> R e. CMnd )
13 5 adantr 
 |-  ( ( ph /\ i e. I ) -> J e. W )
14 6 adantr 
 |-  ( ( ph /\ ( i e. I /\ j e. J ) ) -> R e. Ring )
15 7 fmpttd 
 |-  ( ph -> ( x e. I |-> X ) : I --> B )
16 simpl 
 |-  ( ( i e. I /\ j e. J ) -> i e. I )
17 ffvelrn 
 |-  ( ( ( x e. I |-> X ) : I --> B /\ i e. I ) -> ( ( x e. I |-> X ) ` i ) e. B )
18 15 16 17 syl2an 
 |-  ( ( ph /\ ( i e. I /\ j e. J ) ) -> ( ( x e. I |-> X ) ` i ) e. B )
19 8 fmpttd 
 |-  ( ph -> ( y e. J |-> Y ) : J --> B )
20 simpr 
 |-  ( ( i e. I /\ j e. J ) -> j e. J )
21 ffvelrn 
 |-  ( ( ( y e. J |-> Y ) : J --> B /\ j e. J ) -> ( ( y e. J |-> Y ) ` j ) e. B )
22 19 20 21 syl2an 
 |-  ( ( ph /\ ( i e. I /\ j e. J ) ) -> ( ( y e. J |-> Y ) ` j ) e. B )
23 1 2 ringcl 
 |-  ( ( R e. Ring /\ ( ( x e. I |-> X ) ` i ) e. B /\ ( ( y e. J |-> Y ) ` j ) e. B ) -> ( ( ( x e. I |-> X ) ` i ) .x. ( ( y e. J |-> Y ) ` j ) ) e. B )
24 14 18 22 23 syl3anc 
 |-  ( ( ph /\ ( i e. I /\ j e. J ) ) -> ( ( ( x e. I |-> X ) ` i ) .x. ( ( y e. J |-> Y ) ` j ) ) e. B )
25 9 fsuppimpd 
 |-  ( ph -> ( ( x e. I |-> X ) supp .0. ) e. Fin )
26 10 fsuppimpd 
 |-  ( ph -> ( ( y e. J |-> Y ) supp .0. ) e. Fin )
27 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 )
28 25 26 27 syl2anc 
 |-  ( ph -> ( ( ( x e. I |-> X ) supp .0. ) X. ( ( y e. J |-> Y ) supp .0. ) ) e. Fin )
29 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. ) ) )
30 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. ) ) )
31 29 30 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. ) ) )
32 simprl 
 |-  ( ( ph /\ ( i e. I /\ j e. J ) ) -> i e. I )
33 eldif 
 |-  ( i e. ( I \ ( ( x e. I |-> X ) supp .0. ) ) <-> ( i e. I /\ -. i e. ( ( x e. I |-> X ) supp .0. ) ) )
34 33 biimpri 
 |-  ( ( i e. I /\ -. i e. ( ( x e. I |-> X ) supp .0. ) ) -> i e. ( I \ ( ( x e. I |-> X ) supp .0. ) ) )
35 32 34 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. ) ) )
36 15 adantr 
 |-  ( ( ph /\ ( i e. I /\ j e. J ) ) -> ( x e. I |-> X ) : I --> B )
37 ssidd 
 |-  ( ( ph /\ ( i e. I /\ j e. J ) ) -> ( ( x e. I |-> X ) supp .0. ) C_ ( ( x e. I |-> X ) supp .0. ) )
38 4 adantr 
 |-  ( ( ph /\ ( i e. I /\ j e. J ) ) -> I e. V )
39 3 fvexi 
 |-  .0. e. _V
40 39 a1i 
 |-  ( ( ph /\ ( i e. I /\ j e. J ) ) -> .0. e. _V )
41 36 37 38 40 suppssr 
 |-  ( ( ( ph /\ ( i e. I /\ j e. J ) ) /\ i e. ( I \ ( ( x e. I |-> X ) supp .0. ) ) ) -> ( ( x e. I |-> X ) ` i ) = .0. )
42 35 41 syldan 
 |-  ( ( ( ph /\ ( i e. I /\ j e. J ) ) /\ -. i e. ( ( x e. I |-> X ) supp .0. ) ) -> ( ( x e. I |-> X ) ` i ) = .0. )
43 42 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 ) ) )
44 1 2 3 ringlz 
 |-  ( ( R e. Ring /\ ( ( y e. J |-> Y ) ` j ) e. B ) -> ( .0. .x. ( ( y e. J |-> Y ) ` j ) ) = .0. )
45 14 22 44 syl2anc 
 |-  ( ( ph /\ ( i e. I /\ j e. J ) ) -> ( .0. .x. ( ( y e. J |-> Y ) ` j ) ) = .0. )
46 45 adantr 
 |-  ( ( ( ph /\ ( i e. I /\ j e. J ) ) /\ -. i e. ( ( x e. I |-> X ) supp .0. ) ) -> ( .0. .x. ( ( y e. J |-> Y ) ` j ) ) = .0. )
47 43 46 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. )
48 simprr 
 |-  ( ( ph /\ ( i e. I /\ j e. J ) ) -> j e. J )
49 eldif 
 |-  ( j e. ( J \ ( ( y e. J |-> Y ) supp .0. ) ) <-> ( j e. J /\ -. j e. ( ( y e. J |-> Y ) supp .0. ) ) )
50 49 biimpri 
 |-  ( ( j e. J /\ -. j e. ( ( y e. J |-> Y ) supp .0. ) ) -> j e. ( J \ ( ( y e. J |-> Y ) supp .0. ) ) )
51 48 50 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. ) ) )
52 19 adantr 
 |-  ( ( ph /\ ( i e. I /\ j e. J ) ) -> ( y e. J |-> Y ) : J --> B )
53 ssidd 
 |-  ( ( ph /\ ( i e. I /\ j e. J ) ) -> ( ( y e. J |-> Y ) supp .0. ) C_ ( ( y e. J |-> Y ) supp .0. ) )
54 5 adantr 
 |-  ( ( ph /\ ( i e. I /\ j e. J ) ) -> J e. W )
55 52 53 54 40 suppssr 
 |-  ( ( ( ph /\ ( i e. I /\ j e. J ) ) /\ j e. ( J \ ( ( y e. J |-> Y ) supp .0. ) ) ) -> ( ( y e. J |-> Y ) ` j ) = .0. )
56 51 55 syldan 
 |-  ( ( ( ph /\ ( i e. I /\ j e. J ) ) /\ -. j e. ( ( y e. J |-> Y ) supp .0. ) ) -> ( ( y e. J |-> Y ) ` j ) = .0. )
57 56 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. ) )
58 1 2 3 ringrz 
 |-  ( ( R e. Ring /\ ( ( x e. I |-> X ) ` i ) e. B ) -> ( ( ( x e. I |-> X ) ` i ) .x. .0. ) = .0. )
59 14 18 58 syl2anc 
 |-  ( ( ph /\ ( i e. I /\ j e. J ) ) -> ( ( ( x e. I |-> X ) ` i ) .x. .0. ) = .0. )
60 59 adantr 
 |-  ( ( ( ph /\ ( i e. I /\ j e. J ) ) /\ -. j e. ( ( y e. J |-> Y ) supp .0. ) ) -> ( ( ( x e. I |-> X ) ` i ) .x. .0. ) = .0. )
61 57 60 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. )
62 47 61 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. )
63 31 62 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. )
64 63 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. )
65 1 3 12 4 13 24 28 64 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 ) ) ) ) ) ) )
66 nffvmpt1 
 |-  F/_ x ( ( x e. I |-> X ) ` i )
67 nfcv 
 |-  F/_ x .x.
68 nfcv 
 |-  F/_ x ( ( y e. J |-> Y ) ` j )
69 66 67 68 nfov 
 |-  F/_ x ( ( ( x e. I |-> X ) ` i ) .x. ( ( y e. J |-> Y ) ` j ) )
70 nfcv 
 |-  F/_ y ( ( x e. I |-> X ) ` i )
71 nfcv 
 |-  F/_ y .x.
72 nffvmpt1 
 |-  F/_ y ( ( y e. J |-> Y ) ` j )
73 70 71 72 nfov 
 |-  F/_ y ( ( ( x e. I |-> X ) ` i ) .x. ( ( y e. J |-> Y ) ` j ) )
74 nfcv 
 |-  F/_ i ( ( ( x e. I |-> X ) ` x ) .x. ( ( y e. J |-> Y ) ` y ) )
75 nfcv 
 |-  F/_ j ( ( ( x e. I |-> X ) ` x ) .x. ( ( y e. J |-> Y ) ` y ) )
76 fveq2 
 |-  ( i = x -> ( ( x e. I |-> X ) ` i ) = ( ( x e. I |-> X ) ` x ) )
77 fveq2 
 |-  ( j = y -> ( ( y e. J |-> Y ) ` j ) = ( ( y e. J |-> Y ) ` y ) )
78 76 77 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 ) ) )
79 69 73 74 75 78 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 ) ) )
80 simp2 
 |-  ( ( ph /\ x e. I /\ y e. J ) -> x e. I )
81 7 3adant3 
 |-  ( ( ph /\ x e. I /\ y e. J ) -> X e. B )
82 eqid 
 |-  ( x e. I |-> X ) = ( x e. I |-> X )
83 82 fvmpt2 
 |-  ( ( x e. I /\ X e. B ) -> ( ( x e. I |-> X ) ` x ) = X )
84 80 81 83 syl2anc 
 |-  ( ( ph /\ x e. I /\ y e. J ) -> ( ( x e. I |-> X ) ` x ) = X )
85 simp3 
 |-  ( ( ph /\ x e. I /\ y e. J ) -> y e. J )
86 eqid 
 |-  ( y e. J |-> Y ) = ( y e. J |-> Y )
87 86 fvmpt2 
 |-  ( ( y e. J /\ Y e. B ) -> ( ( y e. J |-> Y ) ` y ) = Y )
88 85 8 87 3imp3i2an 
 |-  ( ( ph /\ x e. I /\ y e. J ) -> ( ( y e. J |-> Y ) ` y ) = Y )
89 84 88 oveq12d 
 |-  ( ( ph /\ x e. I /\ y e. J ) -> ( ( ( x e. I |-> X ) ` x ) .x. ( ( y e. J |-> Y ) ` y ) ) = ( X .x. Y ) )
90 89 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 ) ) )
91 79 90 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 ) ) )
92 91 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 ) ) ) )
93 nfcv 
 |-  F/_ x R
94 nfcv 
 |-  F/_ x gsum
95 nfcv 
 |-  F/_ x J
96 95 69 nfmpt 
 |-  F/_ x ( j e. J |-> ( ( ( x e. I |-> X ) ` i ) .x. ( ( y e. J |-> Y ) ` j ) ) )
97 93 94 96 nfov 
 |-  F/_ x ( R gsum ( j e. J |-> ( ( ( x e. I |-> X ) ` i ) .x. ( ( y e. J |-> Y ) ` j ) ) ) )
98 nfcv 
 |-  F/_ i ( R gsum ( y e. J |-> ( ( ( x e. I |-> X ) ` x ) .x. ( ( y e. J |-> Y ) ` y ) ) ) )
99 76 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 ) ) )
100 99 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 ) ) ) )
101 nfcv 
 |-  F/_ y ( ( x e. I |-> X ) ` x )
102 101 71 72 nfov 
 |-  F/_ y ( ( ( x e. I |-> X ) ` x ) .x. ( ( y e. J |-> Y ) ` j ) )
103 77 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 ) ) )
104 102 75 103 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 ) ) )
105 100 104 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 ) ) ) )
106 105 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 ) ) ) ) )
107 97 98 106 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 ) ) ) ) )
108 89 3expa 
 |-  ( ( ( ph /\ x e. I ) /\ y e. J ) -> ( ( ( x e. I |-> X ) ` x ) .x. ( ( y e. J |-> Y ) ` y ) ) = ( X .x. Y ) )
109 108 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 ) ) )
110 109 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 ) ) ) )
111 110 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 ) ) ) ) )
112 107 111 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 ) ) ) ) )
113 112 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 ) ) ) ) ) )
114 65 92 113 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 ) ) ) ) ) )
115 eqid 
 |-  ( +g ` R ) = ( +g ` R )
116 6 adantr 
 |-  ( ( ph /\ x e. I ) -> R e. Ring )
117 5 adantr 
 |-  ( ( ph /\ x e. I ) -> J e. W )
118 8 adantlr 
 |-  ( ( ( ph /\ x e. I ) /\ y e. J ) -> Y e. B )
119 10 adantr 
 |-  ( ( ph /\ x e. I ) -> ( y e. J |-> Y ) finSupp .0. )
120 1 3 115 2 116 117 7 118 119 gsummulc2 
 |-  ( ( ph /\ x e. I ) -> ( R gsum ( y e. J |-> ( X .x. Y ) ) ) = ( X .x. ( R gsum ( y e. J |-> Y ) ) ) )
121 120 mpteq2dva 
 |-  ( ph -> ( x e. I |-> ( R gsum ( y e. J |-> ( X .x. Y ) ) ) ) = ( x e. I |-> ( X .x. ( R gsum ( y e. J |-> Y ) ) ) ) )
122 121 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 ) ) ) ) ) )
123 1 3 12 5 19 10 gsumcl 
 |-  ( ph -> ( R gsum ( y e. J |-> Y ) ) e. B )
124 1 3 115 2 6 4 123 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 ) ) ) )
125 114 122 124 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 ) ) ) )