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	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	gsumdixp.z	$⊢ \underset{˙}{0} = 0_{R}$
	gsumdixp.i	$⊢ φ \to I \in V$
	gsumdixp.j	$⊢ φ \to J \in W$
	gsumdixp.r	$⊢ φ \to R \in Ring$
	gsumdixp.x	$⊢ (φ \land x \in I) \to X \in B$
	gsumdixp.y	$⊢ (φ \land y \in J) \to Y \in B$
	gsumdixp.xf	$⊢ φ \to {finSupp}_{\underset{˙}{0}} ((x \in I ⟼ X))$
	gsumdixp.yf	$⊢ φ \to {finSupp}_{\underset{˙}{0}} ((y \in J ⟼ Y))$
Assertion	gsumdixp	$⊢ φ \to (\underset{x \in I}{\sum_{R}}, X) \underset{˙}{\cdot} (\underset{y \in J}{\sum_{R}}, Y) = \sum_{R} (x \in I, y \in J ⟼ X \underset{˙}{\cdot} Y)$

Proof

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

Metamath Proof Explorer

Theorem gsumdixp

Proof