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	⊢ 𝐵 = ( Base ‘ 𝑅 )
	gsumdixp.t	⊢ · = ( .r ‘ 𝑅 )
	gsumdixp.z	⊢ 0 = ( 0g ‘ 𝑅 )
	gsumdixp.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	gsumdixp.j	⊢ ( 𝜑 → 𝐽 ∈ 𝑊 )
	gsumdixp.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	gsumdixp.x	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑋 ∈ 𝐵 )
	gsumdixp.y	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) → 𝑌 ∈ 𝐵 )
	gsumdixp.xf	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) finSupp 0 )
	gsumdixp.yf	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) finSupp 0 )
Assertion	gsumdixp	⊢ ( 𝜑 → ( ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) ) · ( 𝑅 Σg ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) ) ) = ( 𝑅 Σg ( 𝑥 ∈ 𝐼 , 𝑦 ∈ 𝐽 ↦ ( 𝑋 · 𝑌 ) ) ) )

Proof

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