Theorem gsummpt2co

Description: Split a finite sum into a sum of a collection of sums over disjoint subsets. (Contributed by Thierry Arnoux, 27-Mar-2018)

	Ref	Expression
Hypotheses	gsummpt2co.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
	gsummpt2co.z	⊢ 0 = ( 0g ‘ 𝑊 )
	gsummpt2co.w	⊢ ( 𝜑 → 𝑊 ∈ CMnd )
	gsummpt2co.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	gsummpt2co.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑉 )
	gsummpt2co.1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝐵 )
	gsummpt2co.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐷 ∈ 𝐸 )
	gsummpt2co.3	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐷 )
Assertion	gsummpt2co	⊢ ( 𝜑 → ( 𝑊 Σg ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ) = ( 𝑊 Σg ( 𝑦 ∈ 𝐸 ↦ ( 𝑊 Σg ( 𝑥 ∈ ( ◡ 𝐹 “ { 𝑦 } ) ↦ 𝐶 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		gsummpt2co.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
2		gsummpt2co.z	⊢ 0 = ( 0g ‘ 𝑊 )
3		gsummpt2co.w	⊢ ( 𝜑 → 𝑊 ∈ CMnd )
4		gsummpt2co.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
5		gsummpt2co.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑉 )
6		gsummpt2co.1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝐵 )
7		gsummpt2co.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐷 ∈ 𝐸 )
8		gsummpt2co.3	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐷 )
9		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ ( 2nd ‘ 𝑝 ) / 𝑥 ⦌ 𝐶
10		csbeq1a	⊢ ( 𝑥 = ( 2nd ‘ 𝑝 ) → 𝐶 = ⦋ ( 2nd ‘ 𝑝 ) / 𝑥 ⦌ 𝐶 )
11		ssidd	⊢ ( 𝜑 → 𝐵 ⊆ 𝐵 )
12		elcnv	⊢ ( 𝑝 ∈ ◡ 𝐹 ↔ ∃ 𝑧 ∃ 𝑥 ( 𝑝 = ⟨ 𝑧 , 𝑥 ⟩ ∧ 𝑥 𝐹 𝑧 ) )
13		vex	⊢ 𝑧 ∈ V
14		vex	⊢ 𝑥 ∈ V
15	13 14	op2ndd	⊢ ( 𝑝 = ⟨ 𝑧 , 𝑥 ⟩ → ( 2nd ‘ 𝑝 ) = 𝑥 )
16	15	adantr	⊢ ( ( 𝑝 = ⟨ 𝑧 , 𝑥 ⟩ ∧ 𝑥 𝐹 𝑧 ) → ( 2nd ‘ 𝑝 ) = 𝑥 )
17	8	dmmptss	⊢ dom 𝐹 ⊆ 𝐴
18	14 13	breldm	⊢ ( 𝑥 𝐹 𝑧 → 𝑥 ∈ dom 𝐹 )
19	17 18	sselid	⊢ ( 𝑥 𝐹 𝑧 → 𝑥 ∈ 𝐴 )
20	19	adantl	⊢ ( ( 𝑝 = ⟨ 𝑧 , 𝑥 ⟩ ∧ 𝑥 𝐹 𝑧 ) → 𝑥 ∈ 𝐴 )
21	16 20	eqeltrd	⊢ ( ( 𝑝 = ⟨ 𝑧 , 𝑥 ⟩ ∧ 𝑥 𝐹 𝑧 ) → ( 2nd ‘ 𝑝 ) ∈ 𝐴 )
22	21	exlimivv	⊢ ( ∃ 𝑧 ∃ 𝑥 ( 𝑝 = ⟨ 𝑧 , 𝑥 ⟩ ∧ 𝑥 𝐹 𝑧 ) → ( 2nd ‘ 𝑝 ) ∈ 𝐴 )
23	12 22	sylbi	⊢ ( 𝑝 ∈ ◡ 𝐹 → ( 2nd ‘ 𝑝 ) ∈ 𝐴 )
24	23	adantl	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ◡ 𝐹 ) → ( 2nd ‘ 𝑝 ) ∈ 𝐴 )
25	8	funmpt2	⊢ Fun 𝐹
26		funcnvcnv	⊢ ( Fun 𝐹 → Fun ◡ ◡ 𝐹 )
27	25 26	ax-mp	⊢ Fun ◡ ◡ 𝐹
28	27	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → Fun ◡ ◡ 𝐹 )
29		dfdm4	⊢ dom 𝐹 = ran ◡ 𝐹
30	8	dmeqi	⊢ dom 𝐹 = dom ( 𝑥 ∈ 𝐴 ↦ 𝐷 )
31	7	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐷 ∈ 𝐸 )
32		dmmptg	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐷 ∈ 𝐸 → dom ( 𝑥 ∈ 𝐴 ↦ 𝐷 ) = 𝐴 )
33	31 32	syl	⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝐴 ↦ 𝐷 ) = 𝐴 )
34	30 33	syl5eq	⊢ ( 𝜑 → dom 𝐹 = 𝐴 )
35	29 34	eqtr3id	⊢ ( 𝜑 → ran ◡ 𝐹 = 𝐴 )
36	35	eleq2d	⊢ ( 𝜑 → ( 𝑥 ∈ ran ◡ 𝐹 ↔ 𝑥 ∈ 𝐴 ) )
37	36	biimpar	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ran ◡ 𝐹 )
38		relcnv	⊢ Rel ◡ 𝐹
39		fcnvgreu	⊢ ( ( ( Rel ◡ 𝐹 ∧ Fun ◡ ◡ 𝐹 ) ∧ 𝑥 ∈ ran ◡ 𝐹 ) → ∃! 𝑝 ∈ ◡ 𝐹 𝑥 = ( 2nd ‘ 𝑝 ) )
40	38 39	mpanl1	⊢ ( ( Fun ◡ ◡ 𝐹 ∧ 𝑥 ∈ ran ◡ 𝐹 ) → ∃! 𝑝 ∈ ◡ 𝐹 𝑥 = ( 2nd ‘ 𝑝 ) )
41	28 37 40	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∃! 𝑝 ∈ ◡ 𝐹 𝑥 = ( 2nd ‘ 𝑝 ) )
42	9 1 2 10 3 4 11 6 24 41	gsummptf1o	⊢ ( 𝜑 → ( 𝑊 Σg ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ) = ( 𝑊 Σg ( 𝑝 ∈ ◡ 𝐹 ↦ ⦋ ( 2nd ‘ 𝑝 ) / 𝑥 ⦌ 𝐶 ) ) )
43	8	rnmptss	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐷 ∈ 𝐸 → ran 𝐹 ⊆ 𝐸 )
44	31 43	syl	⊢ ( 𝜑 → ran 𝐹 ⊆ 𝐸 )
45		dfcnv2	⊢ ( ran 𝐹 ⊆ 𝐸 → ◡ 𝐹 = ∪ 𝑧 ∈ 𝐸 ( { 𝑧 } × ( ◡ 𝐹 “ { 𝑧 } ) ) )
46	44 45	syl	⊢ ( 𝜑 → ◡ 𝐹 = ∪ 𝑧 ∈ 𝐸 ( { 𝑧 } × ( ◡ 𝐹 “ { 𝑧 } ) ) )
47	46	mpteq1d	⊢ ( 𝜑 → ( 𝑝 ∈ ◡ 𝐹 ↦ ⦋ ( 2nd ‘ 𝑝 ) / 𝑥 ⦌ 𝐶 ) = ( 𝑝 ∈ ∪ 𝑧 ∈ 𝐸 ( { 𝑧 } × ( ◡ 𝐹 “ { 𝑧 } ) ) ↦ ⦋ ( 2nd ‘ 𝑝 ) / 𝑥 ⦌ 𝐶 ) )
48		nfcv	⊢ Ⅎ 𝑧 ⦋ ( 2nd ‘ 𝑝 ) / 𝑥 ⦌ 𝐶
49		csbeq1	⊢ ( ( 2nd ‘ 𝑝 ) = 𝑥 → ⦋ ( 2nd ‘ 𝑝 ) / 𝑥 ⦌ 𝐶 = ⦋ 𝑥 / 𝑥 ⦌ 𝐶 )
50	15 49	syl	⊢ ( 𝑝 = ⟨ 𝑧 , 𝑥 ⟩ → ⦋ ( 2nd ‘ 𝑝 ) / 𝑥 ⦌ 𝐶 = ⦋ 𝑥 / 𝑥 ⦌ 𝐶 )
51		csbid	⊢ ⦋ 𝑥 / 𝑥 ⦌ 𝐶 = 𝐶
52	50 51	eqtrdi	⊢ ( 𝑝 = ⟨ 𝑧 , 𝑥 ⟩ → ⦋ ( 2nd ‘ 𝑝 ) / 𝑥 ⦌ 𝐶 = 𝐶 )
53	48 9 52	mpomptxf	⊢ ( 𝑝 ∈ ∪ 𝑧 ∈ 𝐸 ( { 𝑧 } × ( ◡ 𝐹 “ { 𝑧 } ) ) ↦ ⦋ ( 2nd ‘ 𝑝 ) / 𝑥 ⦌ 𝐶 ) = ( 𝑧 ∈ 𝐸 , 𝑥 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ↦ 𝐶 )
54	47 53	eqtrdi	⊢ ( 𝜑 → ( 𝑝 ∈ ◡ 𝐹 ↦ ⦋ ( 2nd ‘ 𝑝 ) / 𝑥 ⦌ 𝐶 ) = ( 𝑧 ∈ 𝐸 , 𝑥 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ↦ 𝐶 ) )
55	54	oveq2d	⊢ ( 𝜑 → ( 𝑊 Σg ( 𝑝 ∈ ◡ 𝐹 ↦ ⦋ ( 2nd ‘ 𝑝 ) / 𝑥 ⦌ 𝐶 ) ) = ( 𝑊 Σg ( 𝑧 ∈ 𝐸 , 𝑥 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ↦ 𝐶 ) ) )
56		mptfi	⊢ ( 𝐴 ∈ Fin → ( 𝑥 ∈ 𝐴 ↦ 𝐷 ) ∈ Fin )
57	8 56	eqeltrid	⊢ ( 𝐴 ∈ Fin → 𝐹 ∈ Fin )
58		cnvfi	⊢ ( 𝐹 ∈ Fin → ◡ 𝐹 ∈ Fin )
59	4 57 58	3syl	⊢ ( 𝜑 → ◡ 𝐹 ∈ Fin )
60		imaexg	⊢ ( ◡ 𝐹 ∈ Fin → ( ◡ 𝐹 “ { 𝑧 } ) ∈ V )
61	59 60	syl	⊢ ( 𝜑 → ( ◡ 𝐹 “ { 𝑧 } ) ∈ V )
62	61	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐸 ) → ( ◡ 𝐹 “ { 𝑧 } ) ∈ V )
63		simpll	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐸 ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ) → 𝜑 )
64		imassrn	⊢ ( ◡ 𝐹 “ { 𝑧 } ) ⊆ ran ◡ 𝐹
65	64 29	sseqtrri	⊢ ( ◡ 𝐹 “ { 𝑧 } ) ⊆ dom 𝐹
66	65 17	sstri	⊢ ( ◡ 𝐹 “ { 𝑧 } ) ⊆ 𝐴
67	13 14	elimasn	⊢ ( 𝑥 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ↔ ⟨ 𝑧 , 𝑥 ⟩ ∈ ◡ 𝐹 )
68	67	biimpi	⊢ ( 𝑥 ∈ ( ◡ 𝐹 “ { 𝑧 } ) → ⟨ 𝑧 , 𝑥 ⟩ ∈ ◡ 𝐹 )
69	68	adantl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐸 ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ) → ⟨ 𝑧 , 𝑥 ⟩ ∈ ◡ 𝐹 )
70	69 67	sylibr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐸 ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ) → 𝑥 ∈ ( ◡ 𝐹 “ { 𝑧 } ) )
71	66 70	sselid	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐸 ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ) → 𝑥 ∈ 𝐴 )
72	63 71 6	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐸 ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ) → 𝐶 ∈ 𝐵 )
73	72	anasss	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐸 ∧ 𝑥 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ) ) → 𝐶 ∈ 𝐵 )
74		df-br	⊢ ( 𝑧 ◡ 𝐹 𝑥 ↔ ⟨ 𝑧 , 𝑥 ⟩ ∈ ◡ 𝐹 )
75	69 74	sylibr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐸 ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ) → 𝑧 ◡ 𝐹 𝑥 )
76	75	anasss	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐸 ∧ 𝑥 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ) ) → 𝑧 ◡ 𝐹 𝑥 )
77	76	pm2.24d	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐸 ∧ 𝑥 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ) ) → ( ¬ 𝑧 ◡ 𝐹 𝑥 → 𝐶 = 0 ) )
78	77	imp	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐸 ∧ 𝑥 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ) ) ∧ ¬ 𝑧 ◡ 𝐹 𝑥 ) → 𝐶 = 0 )
79	78	anasss	⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ 𝐸 ∧ 𝑥 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ) ∧ ¬ 𝑧 ◡ 𝐹 𝑥 ) ) → 𝐶 = 0 )
80	1 2 3 5 62 73 59 79	gsum2d2	⊢ ( 𝜑 → ( 𝑊 Σg ( 𝑧 ∈ 𝐸 , 𝑥 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ↦ 𝐶 ) ) = ( 𝑊 Σg ( 𝑧 ∈ 𝐸 ↦ ( 𝑊 Σg ( 𝑥 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ↦ 𝐶 ) ) ) ) )
81	42 55 80	3eqtrd	⊢ ( 𝜑 → ( 𝑊 Σg ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ) = ( 𝑊 Σg ( 𝑧 ∈ 𝐸 ↦ ( 𝑊 Σg ( 𝑥 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ↦ 𝐶 ) ) ) ) )
82		nfcv	⊢ Ⅎ 𝑧 ( 𝑊 Σg ( 𝑥 ∈ ( ◡ 𝐹 “ { 𝑦 } ) ↦ 𝐶 ) )
83		nfcv	⊢ Ⅎ 𝑦 ( 𝑊 Σg ( 𝑥 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ↦ 𝐶 ) )
84		sneq	⊢ ( 𝑦 = 𝑧 → { 𝑦 } = { 𝑧 } )
85	84	imaeq2d	⊢ ( 𝑦 = 𝑧 → ( ◡ 𝐹 “ { 𝑦 } ) = ( ◡ 𝐹 “ { 𝑧 } ) )
86	85	mpteq1d	⊢ ( 𝑦 = 𝑧 → ( 𝑥 ∈ ( ◡ 𝐹 “ { 𝑦 } ) ↦ 𝐶 ) = ( 𝑥 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ↦ 𝐶 ) )
87	86	oveq2d	⊢ ( 𝑦 = 𝑧 → ( 𝑊 Σg ( 𝑥 ∈ ( ◡ 𝐹 “ { 𝑦 } ) ↦ 𝐶 ) ) = ( 𝑊 Σg ( 𝑥 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ↦ 𝐶 ) ) )
88	82 83 87	cbvmpt	⊢ ( 𝑦 ∈ 𝐸 ↦ ( 𝑊 Σg ( 𝑥 ∈ ( ◡ 𝐹 “ { 𝑦 } ) ↦ 𝐶 ) ) ) = ( 𝑧 ∈ 𝐸 ↦ ( 𝑊 Σg ( 𝑥 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ↦ 𝐶 ) ) )
89	88	oveq2i	⊢ ( 𝑊 Σg ( 𝑦 ∈ 𝐸 ↦ ( 𝑊 Σg ( 𝑥 ∈ ( ◡ 𝐹 “ { 𝑦 } ) ↦ 𝐶 ) ) ) ) = ( 𝑊 Σg ( 𝑧 ∈ 𝐸 ↦ ( 𝑊 Σg ( 𝑥 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ↦ 𝐶 ) ) ) )
90	81 89	eqtr4di	⊢ ( 𝜑 → ( 𝑊 Σg ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ) = ( 𝑊 Σg ( 𝑦 ∈ 𝐸 ↦ ( 𝑊 Σg ( 𝑥 ∈ ( ◡ 𝐹 “ { 𝑦 } ) ↦ 𝐶 ) ) ) ) )