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 ) ) ) )

Metamath Proof Explorer

Theorem gsumdixp

Proof