Theorem prdsgsum

Description: Finite commutative sums in a product structure are taken componentwise. (Contributed by Stefan O'Rear, 1-Feb-2015) (Revised by Mario Carneiro, 3-Jul-2015) (Revised by AV, 9-Jun-2019)

	Ref	Expression
Hypotheses	prdsgsum.y	⊢ 𝑌 = ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) )
	prdsgsum.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	prdsgsum.z	⊢ 0 = ( 0g ‘ 𝑌 )
	prdsgsum.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	prdsgsum.j	⊢ ( 𝜑 → 𝐽 ∈ 𝑊 )
	prdsgsum.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑋 )
	prdsgsum.r	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑅 ∈ CMnd )
	prdsgsum.f	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽 ) ) → 𝑈 ∈ 𝐵 )
	prdsgsum.w	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) finSupp 0 )
Assertion	prdsgsum	⊢ ( 𝜑 → ( 𝑌 Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 Σg ( 𝑦 ∈ 𝐽 ↦ 𝑈 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		prdsgsum.y	⊢ 𝑌 = ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) )
2		prdsgsum.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
3		prdsgsum.z	⊢ 0 = ( 0g ‘ 𝑌 )
4		prdsgsum.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
5		prdsgsum.j	⊢ ( 𝜑 → 𝐽 ∈ 𝑊 )
6		prdsgsum.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑋 )
7		prdsgsum.r	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑅 ∈ CMnd )
8		prdsgsum.f	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽 ) ) → 𝑈 ∈ 𝐵 )
9		prdsgsum.w	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) finSupp 0 )
10		eqid	⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
11	7	fmpttd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) : 𝐼 ⟶ CMnd )
12	11	ffnd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) Fn 𝐼 )
13	1 4 6 11	prdscmnd	⊢ ( 𝜑 → 𝑌 ∈ CMnd )
14	8	anassrs	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑦 ∈ 𝐽 ) → 𝑈 ∈ 𝐵 )
15	14	an32s	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → 𝑈 ∈ 𝐵 )
16	15	ralrimiva	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) → ∀ 𝑥 ∈ 𝐼 𝑈 ∈ 𝐵 )
17	7	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 𝑅 ∈ CMnd )
18	1 10 6 4 17 2	prdsbasmpt2	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ∈ ( Base ‘ 𝑌 ) ↔ ∀ 𝑥 ∈ 𝐼 𝑈 ∈ 𝐵 ) )
19	18	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) → ( ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ∈ ( Base ‘ 𝑌 ) ↔ ∀ 𝑥 ∈ 𝐼 𝑈 ∈ 𝐵 ) )
20	16 19	mpbird	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) → ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ∈ ( Base ‘ 𝑌 ) )
21	20	fmpttd	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) : 𝐽 ⟶ ( Base ‘ 𝑌 ) )
22	10 3 13 5 21 9	gsumcl	⊢ ( 𝜑 → ( 𝑌 Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) ) ∈ ( Base ‘ 𝑌 ) )
23	1 10 6 4 12 22	prdsbasfn	⊢ ( 𝜑 → ( 𝑌 Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) ) Fn 𝐼 )
24		nfcv	⊢ Ⅎ 𝑥 𝑌
25		nfcv	⊢ Ⅎ 𝑥 Σg
26		nfcv	⊢ Ⅎ 𝑥 𝐽
27		nfmpt1	⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐼 ↦ 𝑈 )
28	26 27	nfmpt	⊢ Ⅎ 𝑥 ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) )
29	24 25 28	nfov	⊢ Ⅎ 𝑥 ( 𝑌 Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) )
30	29	dffn5f	⊢ ( ( 𝑌 Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) ) Fn 𝐼 ↔ ( 𝑌 Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑌 Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) ) ‘ 𝑥 ) ) )
31	23 30	sylib	⊢ ( 𝜑 → ( 𝑌 Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑌 Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) ) ‘ 𝑥 ) ) )
32		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑥 ∈ 𝐼 )
33		eqid	⊢ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) = ( 𝑥 ∈ 𝐼 ↦ 𝑈 )
34	33	fvmpt2	⊢ ( ( 𝑥 ∈ 𝐼 ∧ 𝑈 ∈ 𝐵 ) → ( ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ‘ 𝑥 ) = 𝑈 )
35	32 14 34	syl2an2r	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑦 ∈ 𝐽 ) → ( ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ‘ 𝑥 ) = 𝑈 )
36	35	mpteq2dva	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑦 ∈ 𝐽 ↦ ( ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ‘ 𝑥 ) ) = ( 𝑦 ∈ 𝐽 ↦ 𝑈 ) )
37	36	oveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑅 Σg ( 𝑦 ∈ 𝐽 ↦ ( ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ‘ 𝑥 ) ) ) = ( 𝑅 Σg ( 𝑦 ∈ 𝐽 ↦ 𝑈 ) ) )
38	13	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑌 ∈ CMnd )
39		cmnmnd	⊢ ( 𝑅 ∈ CMnd → 𝑅 ∈ Mnd )
40	7 39	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑅 ∈ Mnd )
41	5	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐽 ∈ 𝑊 )
42	4	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐼 ∈ 𝑉 )
43	6	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑆 ∈ 𝑋 )
44	40	fmpttd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) : 𝐼 ⟶ Mnd )
45	44	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) : 𝐼 ⟶ Mnd )
46	1 10 42 43 45 32	prdspjmhm	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑎 ∈ ( Base ‘ 𝑌 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ∈ ( 𝑌 MndHom ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑥 ) ) )
47		eqid	⊢ ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) = ( 𝑥 ∈ 𝐼 ↦ 𝑅 )
48	47	fvmpt2	⊢ ( ( 𝑥 ∈ 𝐼 ∧ 𝑅 ∈ CMnd ) → ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑥 ) = 𝑅 )
49	32 7 48	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑥 ) = 𝑅 )
50	49	oveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑌 MndHom ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑥 ) ) = ( 𝑌 MndHom 𝑅 ) )
51	46 50	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑎 ∈ ( Base ‘ 𝑌 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ∈ ( 𝑌 MndHom 𝑅 ) )
52	20	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑦 ∈ 𝐽 ) → ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ∈ ( Base ‘ 𝑌 ) )
53	9	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) finSupp 0 )
54		fveq1	⊢ ( 𝑎 = ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) → ( 𝑎 ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ‘ 𝑥 ) )
55		fveq1	⊢ ( 𝑎 = ( 𝑌 Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) ) → ( 𝑎 ‘ 𝑥 ) = ( ( 𝑌 Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) ) ‘ 𝑥 ) )
56	10 3 38 40 41 51 52 53 54 55	gsummhm2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑅 Σg ( 𝑦 ∈ 𝐽 ↦ ( ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ‘ 𝑥 ) ) ) = ( ( 𝑌 Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) ) ‘ 𝑥 ) )
57	37 56	eqtr3d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑅 Σg ( 𝑦 ∈ 𝐽 ↦ 𝑈 ) ) = ( ( 𝑌 Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) ) ‘ 𝑥 ) )
58	57	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 Σg ( 𝑦 ∈ 𝐽 ↦ 𝑈 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑌 Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) ) ‘ 𝑥 ) ) )
59	31 58	eqtr4d	⊢ ( 𝜑 → ( 𝑌 Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 Σg ( 𝑦 ∈ 𝐽 ↦ 𝑈 ) ) ) )