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