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	$⊢ Y = S ⨉_{𝑠} (x \in I ⟼ R)$
	prdsgsum.b	$⊢ B = {Base}_{R}$
	prdsgsum.z	$⊢ \underset{˙}{0} = 0_{Y}$
	prdsgsum.i	$⊢ φ \to I \in V$
	prdsgsum.j	$⊢ φ \to J \in W$
	prdsgsum.s	$⊢ φ \to S \in X$
	prdsgsum.r	$⊢ (φ \land x \in I) \to R \in CMnd$
	prdsgsum.f	$⊢ (φ \land (x \in I \land y \in J)) \to U \in B$
	prdsgsum.w	$⊢ φ \to {finSupp}_{\underset{˙}{0}} ((y \in J ⟼ (x \in I ⟼ U)))$
Assertion	prdsgsum	$⊢ φ \to \underset{y \in J}{\sum_{Y}} (x \in I ⟼ U) = (x \in I ⟼ \underset{y \in J}{\sum_{R}} U)$

Proof

Step	Hyp	Ref	Expression
1		prdsgsum.y	$⊢ Y = S ⨉_{𝑠} (x \in I ⟼ R)$
2		prdsgsum.b	$⊢ B = {Base}_{R}$
3		prdsgsum.z	$⊢ \underset{˙}{0} = 0_{Y}$
4		prdsgsum.i	$⊢ φ \to I \in V$
5		prdsgsum.j	$⊢ φ \to J \in W$
6		prdsgsum.s	$⊢ φ \to S \in X$
7		prdsgsum.r	$⊢ (φ \land x \in I) \to R \in CMnd$
8		prdsgsum.f	$⊢ (φ \land (x \in I \land y \in J)) \to U \in B$
9		prdsgsum.w	$⊢ φ \to {finSupp}_{\underset{˙}{0}} ((y \in J ⟼ (x \in I ⟼ U)))$
10		eqid	$⊢ {Base}_{Y} = {Base}_{Y}$
11	7	fmpttd	$⊢ φ \to (x \in I ⟼ R) : I ⟶ CMnd$
12	11	ffnd	$⊢ φ \to (x \in I ⟼ R) Fn I$
13	1 4 6 11	prdscmnd	$⊢ φ \to Y \in CMnd$
14	8	anassrs	$⊢ ((φ \land x \in I) \land y \in J) \to U \in B$
15	14	an32s	$⊢ ((φ \land y \in J) \land x \in I) \to U \in B$
16	15	ralrimiva	$⊢ (φ \land y \in J) \to \forall x \in I U \in B$
17	7	ralrimiva	$⊢ φ \to \forall x \in I R \in CMnd$
18	1 10 6 4 17 2	prdsbasmpt2	$⊢ φ \to ((x \in I ⟼ U) \in {Base}_{Y} \leftrightarrow \forall x \in I U \in B)$
19	18	adantr	$⊢ (φ \land y \in J) \to ((x \in I ⟼ U) \in {Base}_{Y} \leftrightarrow \forall x \in I U \in B)$
20	16 19	mpbird	$⊢ (φ \land y \in J) \to (x \in I ⟼ U) \in {Base}_{Y}$
21	20	fmpttd	$⊢ φ \to (y \in J ⟼ (x \in I ⟼ U)) : J ⟶ {Base}_{Y}$
22	10 3 13 5 21 9	gsumcl	$⊢ φ \to \underset{y \in J}{\sum_{Y}} (x \in I ⟼ U) \in {Base}_{Y}$
23	1 10 6 4 12 22	prdsbasfn	$⊢ φ \to (\underset{y \in J}{\sum_{Y}}, (x \in I ⟼ U)) Fn I$
24		nfcv	$⊢ \underline{Ⅎ} x Y$
25		nfcv	$⊢ \underline{Ⅎ} x Σ_{𝑔}$
26		nfcv	$⊢ \underline{Ⅎ} x J$
27		nfmpt1	$⊢ \underline{Ⅎ} x (x \in I ⟼ U)$
28	26 27	nfmpt	$⊢ \underline{Ⅎ} x (y \in J ⟼ (x \in I ⟼ U))$
29	24 25 28	nfov	$⊢ \underline{Ⅎ} x (\underset{y \in J}{\sum_{Y}}, (x \in I ⟼ U))$
30	29	dffn5f	$⊢ (\underset{y \in J}{\sum_{Y}}, (x \in I ⟼ U)) Fn I \leftrightarrow \underset{y \in J}{\sum_{Y}} (x \in I ⟼ U) = (x \in I ⟼ (\underset{y \in J}{\sum_{Y}}, (x \in I ⟼ U)) (x))$
31	23 30	sylib	$⊢ φ \to \underset{y \in J}{\sum_{Y}} (x \in I ⟼ U) = (x \in I ⟼ (\underset{y \in J}{\sum_{Y}}, (x \in I ⟼ U)) (x))$
32		simpr	$⊢ (φ \land x \in I) \to x \in I$
33		eqid	$⊢ (x \in I ⟼ U) = (x \in I ⟼ U)$
34	33	fvmpt2	$⊢ (x \in I \land U \in B) \to (x \in I ⟼ U) (x) = U$
35	32 14 34	syl2an2r	$⊢ ((φ \land x \in I) \land y \in J) \to (x \in I ⟼ U) (x) = U$
36	35	mpteq2dva	$⊢ (φ \land x \in I) \to (y \in J ⟼ (x \in I ⟼ U) (x)) = (y \in J ⟼ U)$
37	36	oveq2d	$⊢ (φ \land x \in I) \to \underset{y \in J}{\sum_{R}} (x \in I ⟼ U) (x) = \underset{y \in J}{\sum_{R}} U$
38	13	adantr	$⊢ (φ \land x \in I) \to Y \in CMnd$
39		cmnmnd	$⊢ R \in CMnd \to R \in Mnd$
40	7 39	syl	$⊢ (φ \land x \in I) \to R \in Mnd$
41	5	adantr	$⊢ (φ \land x \in I) \to J \in W$
42	4	adantr	$⊢ (φ \land x \in I) \to I \in V$
43	6	adantr	$⊢ (φ \land x \in I) \to S \in X$
44	40	fmpttd	$⊢ φ \to (x \in I ⟼ R) : I ⟶ Mnd$
45	44	adantr	$⊢ (φ \land x \in I) \to (x \in I ⟼ R) : I ⟶ Mnd$
46	1 10 42 43 45 32	prdspjmhm	$⊢ (φ \land x \in I) \to (a \in {Base}_{Y} ⟼ a (x)) \in (Y MndHom (x \in I ⟼ R) (x))$
47		eqid	$⊢ (x \in I ⟼ R) = (x \in I ⟼ R)$
48	47	fvmpt2	$⊢ (x \in I \land R \in CMnd) \to (x \in I ⟼ R) (x) = R$
49	32 7 48	syl2anc	$⊢ (φ \land x \in I) \to (x \in I ⟼ R) (x) = R$
50	49	oveq2d	$⊢ (φ \land x \in I) \to Y MndHom (x \in I ⟼ R) (x) = Y MndHom R$
51	46 50	eleqtrd	$⊢ (φ \land x \in I) \to (a \in {Base}_{Y} ⟼ a (x)) \in (Y MndHom R)$
52	20	adantlr	$⊢ ((φ \land x \in I) \land y \in J) \to (x \in I ⟼ U) \in {Base}_{Y}$
53	9	adantr	$⊢ (φ \land x \in I) \to {finSupp}_{\underset{˙}{0}} ((y \in J ⟼ (x \in I ⟼ U)))$
54		fveq1	$⊢ a = (x \in I ⟼ U) \to a (x) = (x \in I ⟼ U) (x)$
55		fveq1	$⊢ a = \underset{y \in J}{\sum_{Y}} (x \in I ⟼ U) \to a (x) = (\underset{y \in J}{\sum_{Y}}, (x \in I ⟼ U)) (x)$
56	10 3 38 40 41 51 52 53 54 55	gsummhm2	$⊢ (φ \land x \in I) \to \underset{y \in J}{\sum_{R}} (x \in I ⟼ U) (x) = (\underset{y \in J}{\sum_{Y}}, (x \in I ⟼ U)) (x)$
57	37 56	eqtr3d	$⊢ (φ \land x \in I) \to \underset{y \in J}{\sum_{R}} U = (\underset{y \in J}{\sum_{Y}}, (x \in I ⟼ U)) (x)$
58	57	mpteq2dva	$⊢ φ \to (x \in I ⟼ \underset{y \in J}{\sum_{R}} U) = (x \in I ⟼ (\underset{y \in J}{\sum_{Y}}, (x \in I ⟼ U)) (x))$
59	31 58	eqtr4d	$⊢ φ \to \underset{y \in J}{\sum_{Y}} (x \in I ⟼ U) = (x \in I ⟼ \underset{y \in J}{\sum_{R}} U)$

Metamath Proof Explorer

Theorem prdsgsum

Proof