gsummptfidmsplit - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > gsummptfidmsplit		GIF version

Theorem gsummptfidmsplit 14254

Description: Split a group sum expressed as mapping with a finite domain into two parts. (Contributed by AV, 23-Jul-2019.)

**Hypotheses**
Ref	Expression
gsummptfidmsplit.b	⊢ 𝐵 = (Base‘𝐺)
gsummptfidmsplit.p	⊢ + = (+_g‘𝐺)
gsummptfidmsplit.g	⊢ (𝜑 → 𝐺 ∈ CMnd)
gsummptfidmsplit.a	⊢ (𝜑 → 𝐴 ∈ Fin)
gsummptfidmsplit.y	⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑌 ∈ 𝐵)
gsummptfidmsplit.i	⊢ (𝜑 → (𝐶 ∩ 𝐷) = ∅)
gsummptfidmsplit.u	⊢ (𝜑 → 𝐴 = (𝐶 ∪ 𝐷))

**Assertion**
Ref	Expression
gsummptfidmsplit	⊢ (𝜑 → (𝐺 Σ_g (𝑘 ∈ 𝐴 ↦ 𝑌)) = ((𝐺 Σ_g (𝑘 ∈ 𝐶 ↦ 𝑌)) + (𝐺 Σ_g (𝑘 ∈ 𝐷 ↦ 𝑌))))

Distinct variable groups: 𝐴,𝑘 𝐵,𝑘 𝐶,𝑘 𝐷,𝑘 𝜑,𝑘 Allowed substitution hints: + (𝑘) 𝐺(𝑘) 𝑌(𝑘)

Proof of Theorem gsummptfidmsplit Dummy variables 𝑤 𝑦 𝑧 𝑞 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mpteq1 4216	. . . . 5 ⊢ (𝑤 = ∅ → (𝑘 ∈ 𝑤 ↦ 𝑌) = (𝑘 ∈ ∅ ↦ 𝑌))
2	1	oveq2d 6104	. . . 4 ⊢ (𝑤 = ∅ → (𝐺 Σ_g (𝑘 ∈ 𝑤 ↦ 𝑌)) = (𝐺 Σ_g (𝑘 ∈ ∅ ↦ 𝑌)))
3		ineq2 3426	. . . . . . 7 ⊢ (𝑤 = ∅ → (𝐶 ∩ 𝑤) = (𝐶 ∩ ∅))
4	3	mpteq1d 4217	. . . . . 6 ⊢ (𝑤 = ∅ → (𝑘 ∈ (𝐶 ∩ 𝑤) ↦ 𝑌) = (𝑘 ∈ (𝐶 ∩ ∅) ↦ 𝑌))
5	4	oveq2d 6104	. . . . 5 ⊢ (𝑤 = ∅ → (𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑤) ↦ 𝑌)) = (𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ ∅) ↦ 𝑌)))
6		ineq2 3426	. . . . . . 7 ⊢ (𝑤 = ∅ → (𝐷 ∩ 𝑤) = (𝐷 ∩ ∅))
7	6	mpteq1d 4217	. . . . . 6 ⊢ (𝑤 = ∅ → (𝑘 ∈ (𝐷 ∩ 𝑤) ↦ 𝑌) = (𝑘 ∈ (𝐷 ∩ ∅) ↦ 𝑌))
8	7	oveq2d 6104	. . . . 5 ⊢ (𝑤 = ∅ → (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑤) ↦ 𝑌)) = (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ ∅) ↦ 𝑌)))
9	5, 8	oveq12d 6106	. . . 4 ⊢ (𝑤 = ∅ → ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑤) ↦ 𝑌)) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑤) ↦ 𝑌))) = ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ ∅) ↦ 𝑌)) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ ∅) ↦ 𝑌))))
10	2, 9	eqeq12d 2253	. . 3 ⊢ (𝑤 = ∅ → ((𝐺 Σ_g (𝑘 ∈ 𝑤 ↦ 𝑌)) = ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑤) ↦ 𝑌)) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑤) ↦ 𝑌))) ↔ (𝐺 Σ_g (𝑘 ∈ ∅ ↦ 𝑌)) = ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ ∅) ↦ 𝑌)) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ ∅) ↦ 𝑌)))))
11		mpteq1 4216	. . . . 5 ⊢ (𝑤 = 𝑦 → (𝑘 ∈ 𝑤 ↦ 𝑌) = (𝑘 ∈ 𝑦 ↦ 𝑌))
12	11	oveq2d 6104	. . . 4 ⊢ (𝑤 = 𝑦 → (𝐺 Σ_g (𝑘 ∈ 𝑤 ↦ 𝑌)) = (𝐺 Σ_g (𝑘 ∈ 𝑦 ↦ 𝑌)))
13		ineq2 3426	. . . . . . 7 ⊢ (𝑤 = 𝑦 → (𝐶 ∩ 𝑤) = (𝐶 ∩ 𝑦))
14	13	mpteq1d 4217	. . . . . 6 ⊢ (𝑤 = 𝑦 → (𝑘 ∈ (𝐶 ∩ 𝑤) ↦ 𝑌) = (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌))
15	14	oveq2d 6104	. . . . 5 ⊢ (𝑤 = 𝑦 → (𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑤) ↦ 𝑌)) = (𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌)))
16		ineq2 3426	. . . . . . 7 ⊢ (𝑤 = 𝑦 → (𝐷 ∩ 𝑤) = (𝐷 ∩ 𝑦))
17	16	mpteq1d 4217	. . . . . 6 ⊢ (𝑤 = 𝑦 → (𝑘 ∈ (𝐷 ∩ 𝑤) ↦ 𝑌) = (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌))
18	17	oveq2d 6104	. . . . 5 ⊢ (𝑤 = 𝑦 → (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑤) ↦ 𝑌)) = (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌)))
19	15, 18	oveq12d 6106	. . . 4 ⊢ (𝑤 = 𝑦 → ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑤) ↦ 𝑌)) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑤) ↦ 𝑌))) = ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌)) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌))))
20	12, 19	eqeq12d 2253	. . 3 ⊢ (𝑤 = 𝑦 → ((𝐺 Σ_g (𝑘 ∈ 𝑤 ↦ 𝑌)) = ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑤) ↦ 𝑌)) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑤) ↦ 𝑌))) ↔ (𝐺 Σ_g (𝑘 ∈ 𝑦 ↦ 𝑌)) = ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌)) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌)))))
21		mpteq1 4216	. . . . 5 ⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (𝑘 ∈ 𝑤 ↦ 𝑌) = (𝑘 ∈ (𝑦 ∪ {𝑧}) ↦ 𝑌))
22	21	oveq2d 6104	. . . 4 ⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (𝐺 Σ_g (𝑘 ∈ 𝑤 ↦ 𝑌)) = (𝐺 Σ_g (𝑘 ∈ (𝑦 ∪ {𝑧}) ↦ 𝑌)))
23		ineq2 3426	. . . . . . 7 ⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (𝐶 ∩ 𝑤) = (𝐶 ∩ (𝑦 ∪ {𝑧})))
24	23	mpteq1d 4217	. . . . . 6 ⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (𝑘 ∈ (𝐶 ∩ 𝑤) ↦ 𝑌) = (𝑘 ∈ (𝐶 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌))
25	24	oveq2d 6104	. . . . 5 ⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑤) ↦ 𝑌)) = (𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌)))
26		ineq2 3426	. . . . . . 7 ⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (𝐷 ∩ 𝑤) = (𝐷 ∩ (𝑦 ∪ {𝑧})))
27	26	mpteq1d 4217	. . . . . 6 ⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (𝑘 ∈ (𝐷 ∩ 𝑤) ↦ 𝑌) = (𝑘 ∈ (𝐷 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌))
28	27	oveq2d 6104	. . . . 5 ⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑤) ↦ 𝑌)) = (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌)))
29	25, 28	oveq12d 6106	. . . 4 ⊢ (𝑤 = (𝑦 ∪ {𝑧}) → ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑤) ↦ 𝑌)) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑤) ↦ 𝑌))) = ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌)) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌))))
30	22, 29	eqeq12d 2253	. . 3 ⊢ (𝑤 = (𝑦 ∪ {𝑧}) → ((𝐺 Σ_g (𝑘 ∈ 𝑤 ↦ 𝑌)) = ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑤) ↦ 𝑌)) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑤) ↦ 𝑌))) ↔ (𝐺 Σ_g (𝑘 ∈ (𝑦 ∪ {𝑧}) ↦ 𝑌)) = ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌)) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌)))))
31		mpteq1 4216	. . . . 5 ⊢ (𝑤 = 𝐴 → (𝑘 ∈ 𝑤 ↦ 𝑌) = (𝑘 ∈ 𝐴 ↦ 𝑌))
32	31	oveq2d 6104	. . . 4 ⊢ (𝑤 = 𝐴 → (𝐺 Σ_g (𝑘 ∈ 𝑤 ↦ 𝑌)) = (𝐺 Σ_g (𝑘 ∈ 𝐴 ↦ 𝑌)))
33		ineq2 3426	. . . . . . 7 ⊢ (𝑤 = 𝐴 → (𝐶 ∩ 𝑤) = (𝐶 ∩ 𝐴))
34	33	mpteq1d 4217	. . . . . 6 ⊢ (𝑤 = 𝐴 → (𝑘 ∈ (𝐶 ∩ 𝑤) ↦ 𝑌) = (𝑘 ∈ (𝐶 ∩ 𝐴) ↦ 𝑌))
35	34	oveq2d 6104	. . . . 5 ⊢ (𝑤 = 𝐴 → (𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑤) ↦ 𝑌)) = (𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝐴) ↦ 𝑌)))
36		ineq2 3426	. . . . . . 7 ⊢ (𝑤 = 𝐴 → (𝐷 ∩ 𝑤) = (𝐷 ∩ 𝐴))
37	36	mpteq1d 4217	. . . . . 6 ⊢ (𝑤 = 𝐴 → (𝑘 ∈ (𝐷 ∩ 𝑤) ↦ 𝑌) = (𝑘 ∈ (𝐷 ∩ 𝐴) ↦ 𝑌))
38	37	oveq2d 6104	. . . . 5 ⊢ (𝑤 = 𝐴 → (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑤) ↦ 𝑌)) = (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝐴) ↦ 𝑌)))
39	35, 38	oveq12d 6106	. . . 4 ⊢ (𝑤 = 𝐴 → ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑤) ↦ 𝑌)) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑤) ↦ 𝑌))) = ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝐴) ↦ 𝑌)) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝐴) ↦ 𝑌))))
40	32, 39	eqeq12d 2253	. . 3 ⊢ (𝑤 = 𝐴 → ((𝐺 Σ_g (𝑘 ∈ 𝑤 ↦ 𝑌)) = ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑤) ↦ 𝑌)) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑤) ↦ 𝑌))) ↔ (𝐺 Σ_g (𝑘 ∈ 𝐴 ↦ 𝑌)) = ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝐴) ↦ 𝑌)) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝐴) ↦ 𝑌)))))
41		gsummptfidmsplit.g	. . . . . 6 ⊢ (𝜑 → 𝐺 ∈ CMnd)
42	41	cmnmndd 14201	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ Mnd)
43		gsummptfidmsplit.b	. . . . . 6 ⊢ 𝐵 = (Base‘𝐺)
44		eqid 2238	. . . . . 6 ⊢ (0_g‘𝐺) = (0_g‘𝐺)
45	43, 44	mndidcl 13802	. . . . 5 ⊢ (𝐺 ∈ Mnd → (0_g‘𝐺) ∈ 𝐵)
46		gsummptfidmsplit.p	. . . . . 6 ⊢ + = (+_g‘𝐺)
47	43, 46, 44	mndlid 13807	. . . . 5 ⊢ ((𝐺 ∈ Mnd ∧ (0_g‘𝐺) ∈ 𝐵) → ((0_g‘𝐺) + (0_g‘𝐺)) = (0_g‘𝐺))
48	42, 45, 47	syl2anc2 416	. . . 4 ⊢ (𝜑 → ((0_g‘𝐺) + (0_g‘𝐺)) = (0_g‘𝐺))
49		in0 3557	. . . . . . . 8 ⊢ (𝐶 ∩ ∅) = ∅
50		mpteq1 4216	. . . . . . . 8 ⊢ ((𝐶 ∩ ∅) = ∅ → (𝑘 ∈ (𝐶 ∩ ∅) ↦ 𝑌) = (𝑘 ∈ ∅ ↦ 𝑌))
51	49, 50	ax-mp 5	. . . . . . 7 ⊢ (𝑘 ∈ (𝐶 ∩ ∅) ↦ 𝑌) = (𝑘 ∈ ∅ ↦ 𝑌)
52	51	oveq2i 6099	. . . . . 6 ⊢ (𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ ∅) ↦ 𝑌)) = (𝐺 Σ_g (𝑘 ∈ ∅ ↦ 𝑌))
53		mpt0 5514	. . . . . . . 8 ⊢ (𝑘 ∈ ∅ ↦ 𝑌) = ∅
54	53	oveq2i 6099	. . . . . . 7 ⊢ (𝐺 Σ_g (𝑘 ∈ ∅ ↦ 𝑌)) = (𝐺 Σ_g ∅)
55		gsum0cmn 14244	. . . . . . . 8 ⊢ (𝐺 ∈ CMnd → (𝐺 Σ_g ∅) = (0_g‘𝐺))
56	41, 55	syl 14	. . . . . . 7 ⊢ (𝜑 → (𝐺 Σ_g ∅) = (0_g‘𝐺))
57	54, 56	eqtrid 2283	. . . . . 6 ⊢ (𝜑 → (𝐺 Σ_g (𝑘 ∈ ∅ ↦ 𝑌)) = (0_g‘𝐺))
58	52, 57	eqtrid 2283	. . . . 5 ⊢ (𝜑 → (𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ ∅) ↦ 𝑌)) = (0_g‘𝐺))
59		in0 3557	. . . . . . . 8 ⊢ (𝐷 ∩ ∅) = ∅
60		mpteq1 4216	. . . . . . . 8 ⊢ ((𝐷 ∩ ∅) = ∅ → (𝑘 ∈ (𝐷 ∩ ∅) ↦ 𝑌) = (𝑘 ∈ ∅ ↦ 𝑌))
61	59, 60	ax-mp 5	. . . . . . 7 ⊢ (𝑘 ∈ (𝐷 ∩ ∅) ↦ 𝑌) = (𝑘 ∈ ∅ ↦ 𝑌)
62	61	oveq2i 6099	. . . . . 6 ⊢ (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ ∅) ↦ 𝑌)) = (𝐺 Σ_g (𝑘 ∈ ∅ ↦ 𝑌))
63	62, 57	eqtrid 2283	. . . . 5 ⊢ (𝜑 → (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ ∅) ↦ 𝑌)) = (0_g‘𝐺))
64	58, 63	oveq12d 6106	. . . 4 ⊢ (𝜑 → ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ ∅) ↦ 𝑌)) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ ∅) ↦ 𝑌))) = ((0_g‘𝐺) + (0_g‘𝐺)))
65	48, 64, 57	3eqtr4rd 2282	. . 3 ⊢ (𝜑 → (𝐺 Σ_g (𝑘 ∈ ∅ ↦ 𝑌)) = ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ ∅) ↦ 𝑌)) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ ∅) ↦ 𝑌))))
66	41	ad2antrr 492	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → 𝐺 ∈ CMnd)
67		simplll 539	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ (𝑦 ∪ {𝑧})) → 𝜑)
68		simprl 535	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → 𝑦 ⊆ 𝐴)
69	68	ad2antrr 492	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑘 ∈ 𝑦) → 𝑦 ⊆ 𝐴)
70		simpr 110	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑘 ∈ 𝑦) → 𝑘 ∈ 𝑦)
71	69, 70	sseldd 3249	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑘 ∈ 𝑦) → 𝑘 ∈ 𝐴)
72		simprr 537	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → 𝑧 ∈ (𝐴 ∖ 𝑦))
73	72	eldifad 3231	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → 𝑧 ∈ 𝐴)
74	73	ad2antrr 492	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑘 ∈ {𝑧}) → 𝑧 ∈ 𝐴)
75		elsni 3727	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ {𝑧} → 𝑘 = 𝑧)
76	75	eleq1d 2307	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ {𝑧} → (𝑘 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴))
77	76	adantl 277	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑘 ∈ {𝑧}) → (𝑘 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴))
78	74, 77	mpbird 167	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ (𝑦 ∪ {𝑧})) ∧ 𝑘 ∈ {𝑧}) → 𝑘 ∈ 𝐴)
79		elun 3370	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (𝑦 ∪ {𝑧}) ↔ (𝑘 ∈ 𝑦 ∨ 𝑘 ∈ {𝑧}))
80	79	bilani 387	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ (𝑦 ∪ {𝑧})) → (𝑘 ∈ 𝑦 ∨ 𝑘 ∈ {𝑧}))
81	71, 78, 80	mpjaodan 810	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ (𝑦 ∪ {𝑧})) → 𝑘 ∈ 𝐴)
82		gsummptfidmsplit.y	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑌 ∈ 𝐵)
83	67, 81, 82	syl2anc 415	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ (𝑦 ∪ {𝑧})) → 𝑌 ∈ 𝐵)
84	83	fmpttd 5866	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (𝑘 ∈ (𝑦 ∪ {𝑧}) ↦ 𝑌):(𝑦 ∪ {𝑧})⟶𝐵)
85		simplr 533	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → 𝑦 ∈ Fin)
86	72	eldifbd 3232	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ¬ 𝑧 ∈ 𝑦)
87	43, 46, 66, 84, 85, 73, 86	gsump1 14247	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (𝐺 Σ_g (𝑘 ∈ (𝑦 ∪ {𝑧}) ↦ 𝑌)) = ((𝐺 Σ_g ((𝑘 ∈ (𝑦 ∪ {𝑧}) ↦ 𝑌) ↾ 𝑦)) + ((𝑘 ∈ (𝑦 ∪ {𝑧}) ↦ 𝑌)‘𝑧)))
88		ssun1 3392	. . . . . . . . . . . . . 14 ⊢ 𝑦 ⊆ (𝑦 ∪ {𝑧})
89	88	a1i 9	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → 𝑦 ⊆ (𝑦 ∪ {𝑧}))
90	89	resmptd 5117	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ((𝑘 ∈ (𝑦 ∪ {𝑧}) ↦ 𝑌) ↾ 𝑦) = (𝑘 ∈ 𝑦 ↦ 𝑌))
91	90	oveq2d 6104	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (𝐺 Σ_g ((𝑘 ∈ (𝑦 ∪ {𝑧}) ↦ 𝑌) ↾ 𝑦)) = (𝐺 Σ_g (𝑘 ∈ 𝑦 ↦ 𝑌)))
92		vsnid 3741	. . . . . . . . . . . . 13 ⊢ 𝑧 ∈ {𝑧}
93		elun2 3397	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ {𝑧} → 𝑧 ∈ (𝑦 ∪ {𝑧}))
94	92, 93	ax-mp 5	. . . . . . . . . . . 12 ⊢ 𝑧 ∈ (𝑦 ∪ {𝑧})
95	82	ralrimiva 2623	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝑌 ∈ 𝐵)
96	95	ad2antrr 492	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ∀𝑘 ∈ 𝐴 𝑌 ∈ 𝐵)
97		nfcsb1v 3180	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘⦋𝑧 / 𝑘⦌𝑌
98	97	nfel1 2403	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘⦋𝑧 / 𝑘⦌𝑌 ∈ 𝐵
99		csbeq1a 3156	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑧 → 𝑌 = ⦋𝑧 / 𝑘⦌𝑌)
100	99	eleq1d 2307	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑧 → (𝑌 ∈ 𝐵 ↔ ⦋𝑧 / 𝑘⦌𝑌 ∈ 𝐵))
101	98, 100	rspc 2923	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝑌 ∈ 𝐵 → ⦋𝑧 / 𝑘⦌𝑌 ∈ 𝐵))
102	73, 96, 101	sylc 62	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ⦋𝑧 / 𝑘⦌𝑌 ∈ 𝐵)
103		eqid 2238	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (𝑦 ∪ {𝑧}) ↦ 𝑌) = (𝑘 ∈ (𝑦 ∪ {𝑧}) ↦ 𝑌)
104	103	fvmpts 5786	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ (𝑦 ∪ {𝑧}) ∧ ⦋𝑧 / 𝑘⦌𝑌 ∈ 𝐵) → ((𝑘 ∈ (𝑦 ∪ {𝑧}) ↦ 𝑌)‘𝑧) = ⦋𝑧 / 𝑘⦌𝑌)
105	94, 102, 104	sylancr 418	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ((𝑘 ∈ (𝑦 ∪ {𝑧}) ↦ 𝑌)‘𝑧) = ⦋𝑧 / 𝑘⦌𝑌)
106	91, 105	oveq12d 6106	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ((𝐺 Σ_g ((𝑘 ∈ (𝑦 ∪ {𝑧}) ↦ 𝑌) ↾ 𝑦)) + ((𝑘 ∈ (𝑦 ∪ {𝑧}) ↦ 𝑌)‘𝑧)) = ((𝐺 Σ_g (𝑘 ∈ 𝑦 ↦ 𝑌)) + ⦋𝑧 / 𝑘⦌𝑌))
107	87, 106	eqtrd 2271	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (𝐺 Σ_g (𝑘 ∈ (𝑦 ∪ {𝑧}) ↦ 𝑌)) = ((𝐺 Σ_g (𝑘 ∈ 𝑦 ↦ 𝑌)) + ⦋𝑧 / 𝑘⦌𝑌))
108	107	adantr 276	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ (𝐺 Σ_g (𝑘 ∈ 𝑦 ↦ 𝑌)) = ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌)) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌)))) → (𝐺 Σ_g (𝑘 ∈ (𝑦 ∪ {𝑧}) ↦ 𝑌)) = ((𝐺 Σ_g (𝑘 ∈ 𝑦 ↦ 𝑌)) + ⦋𝑧 / 𝑘⦌𝑌))
109		simpr 110	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ (𝐺 Σ_g (𝑘 ∈ 𝑦 ↦ 𝑌)) = ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌)) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌)))) → (𝐺 Σ_g (𝑘 ∈ 𝑦 ↦ 𝑌)) = ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌)) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌))))
110	109	oveq1d 6103	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ (𝐺 Σ_g (𝑘 ∈ 𝑦 ↦ 𝑌)) = ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌)) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌)))) → ((𝐺 Σ_g (𝑘 ∈ 𝑦 ↦ 𝑌)) + ⦋𝑧 / 𝑘⦌𝑌) = (((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌)) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌))) + ⦋𝑧 / 𝑘⦌𝑌))
111	66	adantr 276	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ (𝐺 Σ_g (𝑘 ∈ 𝑦 ↦ 𝑌)) = ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌)) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌)))) → 𝐺 ∈ CMnd)
112		gsummptfidmsplit.a	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ∈ Fin)
113	112	ad2antrr 492	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → 𝐴 ∈ Fin)
114		inss2 3452	. . . . . . . . . . . . 13 ⊢ (𝐶 ∩ 𝑦) ⊆ 𝑦
115	114, 68	sstrid 3259	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (𝐶 ∩ 𝑦) ⊆ 𝐴)
116		gsummptfidmsplit.i	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐶 ∩ 𝐷) = ∅)
117	116	ad3antrrr 496	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑞 ∈ 𝐴) → (𝐶 ∩ 𝐷) = ∅)
118		ineqcom 3422	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐶 ∩ 𝐷) = ∅ ↔ (𝐷 ∩ 𝐶) = ∅)
119	117, 118	sylib 122	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑞 ∈ 𝐴) → (𝐷 ∩ 𝐶) = ∅)
120		gsummptfidmsplit.u	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐴 = (𝐶 ∪ 𝐷))
121	120	eleq2d 2308	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑞 ∈ 𝐴 ↔ 𝑞 ∈ (𝐶 ∪ 𝐷)))
122	121	ad2antrr 492	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (𝑞 ∈ 𝐴 ↔ 𝑞 ∈ (𝐶 ∪ 𝐷)))
123	122	biimpa 296	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑞 ∈ 𝐴) → 𝑞 ∈ (𝐶 ∪ 𝐷))
124		elun 3370	. . . . . . . . . . . . . . . . 17 ⊢ (𝑞 ∈ (𝐶 ∪ 𝐷) ↔ (𝑞 ∈ 𝐶 ∨ 𝑞 ∈ 𝐷))
125	123, 124	sylib 122	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑞 ∈ 𝐴) → (𝑞 ∈ 𝐶 ∨ 𝑞 ∈ 𝐷))
126		orc 724	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑞 ∈ 𝐶 → (𝑞 ∈ 𝐶 ∨ ¬ 𝑞 ∈ 𝐶))
127		df-dc 847	. . . . . . . . . . . . . . . . . . 19 ⊢ (DECID 𝑞 ∈ 𝐶 ↔ (𝑞 ∈ 𝐶 ∨ ¬ 𝑞 ∈ 𝐶))
128	126, 127	sylibr 134	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑞 ∈ 𝐶 → DECID 𝑞 ∈ 𝐶)
129	128	a1i 9	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ∩ 𝐶) = ∅ → (𝑞 ∈ 𝐶 → DECID 𝑞 ∈ 𝐶))
130		disjel 3579	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐷 ∩ 𝐶) = ∅ ∧ 𝑞 ∈ 𝐷) → ¬ 𝑞 ∈ 𝐶)
131	130	olcd 746	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐷 ∩ 𝐶) = ∅ ∧ 𝑞 ∈ 𝐷) → (𝑞 ∈ 𝐶 ∨ ¬ 𝑞 ∈ 𝐶))
132	131, 127	sylibr 134	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐷 ∩ 𝐶) = ∅ ∧ 𝑞 ∈ 𝐷) → DECID 𝑞 ∈ 𝐶)
133	132	ex 115	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ∩ 𝐶) = ∅ → (𝑞 ∈ 𝐷 → DECID 𝑞 ∈ 𝐶))
134	129, 133	jaod 729	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∩ 𝐶) = ∅ → ((𝑞 ∈ 𝐶 ∨ 𝑞 ∈ 𝐷) → DECID 𝑞 ∈ 𝐶))
135	119, 125, 134	sylc 62	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑞 ∈ 𝐴) → DECID 𝑞 ∈ 𝐶)
136		fissfi 7267	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ⊆ 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝑦 ∈ Fin) → ∀𝑞 ∈ 𝐴 DECID 𝑞 ∈ 𝑦)
137	68, 113, 85, 136	syl3anc 1278	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ∀𝑞 ∈ 𝐴 DECID 𝑞 ∈ 𝑦)
138	137	r19.21bi 2638	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑞 ∈ 𝐴) → DECID 𝑞 ∈ 𝑦)
139	135, 138	dcand 945	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑞 ∈ 𝐴) → DECID (𝑞 ∈ 𝐶 ∧ 𝑞 ∈ 𝑦))
140		elin 3412	. . . . . . . . . . . . . . 15 ⊢ (𝑞 ∈ (𝐶 ∩ 𝑦) ↔ (𝑞 ∈ 𝐶 ∧ 𝑞 ∈ 𝑦))
141	140	dcbii 852	. . . . . . . . . . . . . 14 ⊢ (DECID 𝑞 ∈ (𝐶 ∩ 𝑦) ↔ DECID (𝑞 ∈ 𝐶 ∧ 𝑞 ∈ 𝑦))
142	139, 141	sylibr 134	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑞 ∈ 𝐴) → DECID 𝑞 ∈ (𝐶 ∩ 𝑦))
143	142	ralrimiva 2623	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ∀𝑞 ∈ 𝐴 DECID 𝑞 ∈ (𝐶 ∩ 𝑦))
144		ssfidc 7249	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Fin ∧ (𝐶 ∩ 𝑦) ⊆ 𝐴 ∧ ∀𝑞 ∈ 𝐴 DECID 𝑞 ∈ (𝐶 ∩ 𝑦)) → (𝐶 ∩ 𝑦) ∈ Fin)
145	113, 115, 143, 144	syl3anc 1278	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (𝐶 ∩ 𝑦) ∈ Fin)
146		simplll 539	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ (𝐶 ∩ 𝑦)) → 𝜑)
147	115	sselda 3248	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ (𝐶 ∩ 𝑦)) → 𝑘 ∈ 𝐴)
148	146, 147, 82	syl2anc 415	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ (𝐶 ∩ 𝑦)) → 𝑌 ∈ 𝐵)
149	148	fmpttd 5866	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌):(𝐶 ∩ 𝑦)⟶𝐵)
150	43, 44, 66, 145, 149	gsumclfi 14249	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌)) ∈ 𝐵)
151	150	adantr 276	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ (𝐺 Σ_g (𝑘 ∈ 𝑦 ↦ 𝑌)) = ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌)) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌)))) → (𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌)) ∈ 𝐵)
152		inss2 3452	. . . . . . . . . . . . 13 ⊢ (𝐷 ∩ 𝑦) ⊆ 𝑦
153	152, 68	sstrid 3259	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (𝐷 ∩ 𝑦) ⊆ 𝐴)
154		disjel 3579	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐶 ∩ 𝐷) = ∅ ∧ 𝑞 ∈ 𝐶) → ¬ 𝑞 ∈ 𝐷)
155	154	olcd 746	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐶 ∩ 𝐷) = ∅ ∧ 𝑞 ∈ 𝐶) → (𝑞 ∈ 𝐷 ∨ ¬ 𝑞 ∈ 𝐷))
156		df-dc 847	. . . . . . . . . . . . . . . . . . 19 ⊢ (DECID 𝑞 ∈ 𝐷 ↔ (𝑞 ∈ 𝐷 ∨ ¬ 𝑞 ∈ 𝐷))
157	155, 156	sylibr 134	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐶 ∩ 𝐷) = ∅ ∧ 𝑞 ∈ 𝐶) → DECID 𝑞 ∈ 𝐷)
158	157	ex 115	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐶 ∩ 𝐷) = ∅ → (𝑞 ∈ 𝐶 → DECID 𝑞 ∈ 𝐷))
159		orc 724	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑞 ∈ 𝐷 → (𝑞 ∈ 𝐷 ∨ ¬ 𝑞 ∈ 𝐷))
160	159, 156	sylibr 134	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑞 ∈ 𝐷 → DECID 𝑞 ∈ 𝐷)
161	160	a1i 9	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐶 ∩ 𝐷) = ∅ → (𝑞 ∈ 𝐷 → DECID 𝑞 ∈ 𝐷))
162	158, 161	jaod 729	. . . . . . . . . . . . . . . 16 ⊢ ((𝐶 ∩ 𝐷) = ∅ → ((𝑞 ∈ 𝐶 ∨ 𝑞 ∈ 𝐷) → DECID 𝑞 ∈ 𝐷))
163	117, 125, 162	sylc 62	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑞 ∈ 𝐴) → DECID 𝑞 ∈ 𝐷)
164	163, 138	dcand 945	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑞 ∈ 𝐴) → DECID (𝑞 ∈ 𝐷 ∧ 𝑞 ∈ 𝑦))
165		elin 3412	. . . . . . . . . . . . . . 15 ⊢ (𝑞 ∈ (𝐷 ∩ 𝑦) ↔ (𝑞 ∈ 𝐷 ∧ 𝑞 ∈ 𝑦))
166	165	dcbii 852	. . . . . . . . . . . . . 14 ⊢ (DECID 𝑞 ∈ (𝐷 ∩ 𝑦) ↔ DECID (𝑞 ∈ 𝐷 ∧ 𝑞 ∈ 𝑦))
167	164, 166	sylibr 134	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑞 ∈ 𝐴) → DECID 𝑞 ∈ (𝐷 ∩ 𝑦))
168	167	ralrimiva 2623	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ∀𝑞 ∈ 𝐴 DECID 𝑞 ∈ (𝐷 ∩ 𝑦))
169		ssfidc 7249	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Fin ∧ (𝐷 ∩ 𝑦) ⊆ 𝐴 ∧ ∀𝑞 ∈ 𝐴 DECID 𝑞 ∈ (𝐷 ∩ 𝑦)) → (𝐷 ∩ 𝑦) ∈ Fin)
170	113, 153, 168, 169	syl3anc 1278	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (𝐷 ∩ 𝑦) ∈ Fin)
171		simplll 539	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ (𝐷 ∩ 𝑦)) → 𝜑)
172	153	sselda 3248	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ (𝐷 ∩ 𝑦)) → 𝑘 ∈ 𝐴)
173	171, 172, 82	syl2anc 415	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ (𝐷 ∩ 𝑦)) → 𝑌 ∈ 𝐵)
174	173	fmpttd 5866	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌):(𝐷 ∩ 𝑦)⟶𝐵)
175	43, 44, 66, 170, 174	gsumclfi 14249	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌)) ∈ 𝐵)
176	175	adantr 276	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ (𝐺 Σ_g (𝑘 ∈ 𝑦 ↦ 𝑌)) = ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌)) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌)))) → (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌)) ∈ 𝐵)
177	102	adantr 276	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ (𝐺 Σ_g (𝑘 ∈ 𝑦 ↦ 𝑌)) = ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌)) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌)))) → ⦋𝑧 / 𝑘⦌𝑌 ∈ 𝐵)
178	43, 46	cmn32 14197	. . . . . . . . 9 ⊢ ((𝐺 ∈ CMnd ∧ ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌)) ∈ 𝐵 ∧ (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌)) ∈ 𝐵 ∧ ⦋𝑧 / 𝑘⦌𝑌 ∈ 𝐵)) → (((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌)) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌))) + ⦋𝑧 / 𝑘⦌𝑌) = (((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌)) + ⦋𝑧 / 𝑘⦌𝑌) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌))))
179	111, 151, 176, 177, 178	syl13anc 1280	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ (𝐺 Σ_g (𝑘 ∈ 𝑦 ↦ 𝑌)) = ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌)) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌)))) → (((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌)) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌))) + ⦋𝑧 / 𝑘⦌𝑌) = (((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌)) + ⦋𝑧 / 𝑘⦌𝑌) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌))))
180	108, 110, 179	3eqtrd 2275	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ (𝐺 Σ_g (𝑘 ∈ 𝑦 ↦ 𝑌)) = ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌)) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌)))) → (𝐺 Σ_g (𝑘 ∈ (𝑦 ∪ {𝑧}) ↦ 𝑌)) = (((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌)) + ⦋𝑧 / 𝑘⦌𝑌) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌))))
181	180	adantlr 481	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐶) ∧ (𝐺 Σ_g (𝑘 ∈ 𝑦 ↦ 𝑌)) = ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌)) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌)))) → (𝐺 Σ_g (𝑘 ∈ (𝑦 ∪ {𝑧}) ↦ 𝑌)) = (((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌)) + ⦋𝑧 / 𝑘⦌𝑌) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌))))
182	66	adantr 276	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐶) → 𝐺 ∈ CMnd)
183		simp-4l 547	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐶) ∧ 𝑘 ∈ (𝐶 ∩ (𝑦 ∪ {𝑧}))) → 𝜑)
184		ssun1 3392	. . . . . . . . . . . . . . . 16 ⊢ 𝐶 ⊆ (𝐶 ∪ 𝐷)
185	184, 120	sseqtrrid 3299	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐶 ⊆ 𝐴)
186	185	ad4antr 498	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐶) ∧ 𝑘 ∈ (𝐶 ∩ (𝑦 ∪ {𝑧}))) → 𝐶 ⊆ 𝐴)
187		elinel1 3415	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (𝐶 ∩ (𝑦 ∪ {𝑧})) → 𝑘 ∈ 𝐶)
188	187	adantl 277	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐶) ∧ 𝑘 ∈ (𝐶 ∩ (𝑦 ∪ {𝑧}))) → 𝑘 ∈ 𝐶)
189	186, 188	sseldd 3249	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐶) ∧ 𝑘 ∈ (𝐶 ∩ (𝑦 ∪ {𝑧}))) → 𝑘 ∈ 𝐴)
190	183, 189, 82	syl2anc 415	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐶) ∧ 𝑘 ∈ (𝐶 ∩ (𝑦 ∪ {𝑧}))) → 𝑌 ∈ 𝐵)
191	190	fmpttd 5866	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐶) → (𝑘 ∈ (𝐶 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌):(𝐶 ∩ (𝑦 ∪ {𝑧}))⟶𝐵)
192		indi 3478	. . . . . . . . . . . . . 14 ⊢ (𝐶 ∩ (𝑦 ∪ {𝑧})) = ((𝐶 ∩ 𝑦) ∪ (𝐶 ∩ {𝑧}))
193		snssi 3859	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ 𝐶 → {𝑧} ⊆ 𝐶)
194		dfss1 3435	. . . . . . . . . . . . . . . 16 ⊢ ({𝑧} ⊆ 𝐶 ↔ (𝐶 ∩ {𝑧}) = {𝑧})
195	193, 194	sylib 122	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ 𝐶 → (𝐶 ∩ {𝑧}) = {𝑧})
196	195	uneq2d 3383	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ 𝐶 → ((𝐶 ∩ 𝑦) ∪ (𝐶 ∩ {𝑧})) = ((𝐶 ∩ 𝑦) ∪ {𝑧}))
197	192, 196	eqtrid 2283	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ 𝐶 → (𝐶 ∩ (𝑦 ∪ {𝑧})) = ((𝐶 ∩ 𝑦) ∪ {𝑧}))
198	197	feq2d 5524	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ 𝐶 → ((𝑘 ∈ (𝐶 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌):(𝐶 ∩ (𝑦 ∪ {𝑧}))⟶𝐵 ↔ (𝑘 ∈ (𝐶 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌):((𝐶 ∩ 𝑦) ∪ {𝑧})⟶𝐵))
199	198	adantl 277	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐶) → ((𝑘 ∈ (𝐶 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌):(𝐶 ∩ (𝑦 ∪ {𝑧}))⟶𝐵 ↔ (𝑘 ∈ (𝐶 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌):((𝐶 ∩ 𝑦) ∪ {𝑧})⟶𝐵))
200	191, 199	mpbid 147	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐶) → (𝑘 ∈ (𝐶 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌):((𝐶 ∩ 𝑦) ∪ {𝑧})⟶𝐵)
201	145	adantr 276	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐶) → (𝐶 ∩ 𝑦) ∈ Fin)
202		simpr 110	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐶) → 𝑧 ∈ 𝐶)
203		simpr 110	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ 𝐶 ∧ 𝑧 ∈ 𝑦) → 𝑧 ∈ 𝑦)
204	203	con3i 641	. . . . . . . . . . . . 13 ⊢ (¬ 𝑧 ∈ 𝑦 → ¬ (𝑧 ∈ 𝐶 ∧ 𝑧 ∈ 𝑦))
205		elin 3412	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (𝐶 ∩ 𝑦) ↔ (𝑧 ∈ 𝐶 ∧ 𝑧 ∈ 𝑦))
206	204, 205	sylnibr 688	. . . . . . . . . . . 12 ⊢ (¬ 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ (𝐶 ∩ 𝑦))
207	86, 206	syl 14	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ¬ 𝑧 ∈ (𝐶 ∩ 𝑦))
208	207	adantr 276	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐶) → ¬ 𝑧 ∈ (𝐶 ∩ 𝑦))
209	43, 46, 182, 200, 201, 202, 208	gsump1 14247	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐶) → (𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌)) = ((𝐺 Σ_g ((𝑘 ∈ (𝐶 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌) ↾ (𝐶 ∩ 𝑦))) + ((𝑘 ∈ (𝐶 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌)‘𝑧)))
210		ssun1 3392	. . . . . . . . . . . . . . 15 ⊢ (𝐶 ∩ 𝑦) ⊆ ((𝐶 ∩ 𝑦) ∪ (𝐶 ∩ {𝑧}))
211	210, 192	sseqtrri 3283	. . . . . . . . . . . . . 14 ⊢ (𝐶 ∩ 𝑦) ⊆ (𝐶 ∩ (𝑦 ∪ {𝑧}))
212	211	a1i 9	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (𝐶 ∩ 𝑦) ⊆ (𝐶 ∩ (𝑦 ∪ {𝑧})))
213	212	resmptd 5117	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ((𝑘 ∈ (𝐶 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌) ↾ (𝐶 ∩ 𝑦)) = (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌))
214	213	oveq2d 6104	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (𝐺 Σ_g ((𝑘 ∈ (𝐶 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌) ↾ (𝐶 ∩ 𝑦))) = (𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌)))
215	214	adantr 276	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐶) → (𝐺 Σ_g ((𝑘 ∈ (𝐶 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌) ↾ (𝐶 ∩ 𝑦))) = (𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌)))
216		elin 3412	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ (𝐶 ∩ (𝑦 ∪ {𝑧})) ↔ (𝑧 ∈ 𝐶 ∧ 𝑧 ∈ (𝑦 ∪ {𝑧})))
217	202, 94, 216	sylanblrc 420	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐶) → 𝑧 ∈ (𝐶 ∩ (𝑦 ∪ {𝑧})))
218	102	adantr 276	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐶) → ⦋𝑧 / 𝑘⦌𝑌 ∈ 𝐵)
219		eqid 2238	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (𝐶 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌) = (𝑘 ∈ (𝐶 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌)
220	219	fvmpts 5786	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ (𝐶 ∩ (𝑦 ∪ {𝑧})) ∧ ⦋𝑧 / 𝑘⦌𝑌 ∈ 𝐵) → ((𝑘 ∈ (𝐶 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌)‘𝑧) = ⦋𝑧 / 𝑘⦌𝑌)
221	217, 218, 220	syl2anc 415	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐶) → ((𝑘 ∈ (𝐶 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌)‘𝑧) = ⦋𝑧 / 𝑘⦌𝑌)
222	215, 221	oveq12d 6106	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐶) → ((𝐺 Σ_g ((𝑘 ∈ (𝐶 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌) ↾ (𝐶 ∩ 𝑦))) + ((𝑘 ∈ (𝐶 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌)‘𝑧)) = ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌)) + ⦋𝑧 / 𝑘⦌𝑌))
223	209, 222	eqtrd 2271	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐶) → (𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌)) = ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌)) + ⦋𝑧 / 𝑘⦌𝑌))
224	116	ad3antrrr 496	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐶) → (𝐶 ∩ 𝐷) = ∅)
225		disjel 3579	. . . . . . . . . . . 12 ⊢ (((𝐶 ∩ 𝐷) = ∅ ∧ 𝑧 ∈ 𝐶) → ¬ 𝑧 ∈ 𝐷)
226	224, 202, 225	syl2anc 415	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐶) → ¬ 𝑧 ∈ 𝐷)
227		indi 3478	. . . . . . . . . . . 12 ⊢ (𝐷 ∩ (𝑦 ∪ {𝑧})) = ((𝐷 ∩ 𝑦) ∪ (𝐷 ∩ {𝑧}))
228		disjsn 3771	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝐷)
229	228	biimpri 133	. . . . . . . . . . . . . 14 ⊢ (¬ 𝑧 ∈ 𝐷 → (𝐷 ∩ {𝑧}) = ∅)
230	229	uneq2d 3383	. . . . . . . . . . . . 13 ⊢ (¬ 𝑧 ∈ 𝐷 → ((𝐷 ∩ 𝑦) ∪ (𝐷 ∩ {𝑧})) = ((𝐷 ∩ 𝑦) ∪ ∅))
231		un0 3556	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∩ 𝑦) ∪ ∅) = (𝐷 ∩ 𝑦)
232	230, 231	eqtrdi 2287	. . . . . . . . . . . 12 ⊢ (¬ 𝑧 ∈ 𝐷 → ((𝐷 ∩ 𝑦) ∪ (𝐷 ∩ {𝑧})) = (𝐷 ∩ 𝑦))
233	227, 232	eqtrid 2283	. . . . . . . . . . 11 ⊢ (¬ 𝑧 ∈ 𝐷 → (𝐷 ∩ (𝑦 ∪ {𝑧})) = (𝐷 ∩ 𝑦))
234	226, 233	syl 14	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐶) → (𝐷 ∩ (𝑦 ∪ {𝑧})) = (𝐷 ∩ 𝑦))
235	234	mpteq1d 4217	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐶) → (𝑘 ∈ (𝐷 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌) = (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌))
236	235	oveq2d 6104	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐶) → (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌)) = (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌)))
237	223, 236	oveq12d 6106	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐶) → ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌)) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌))) = (((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌)) + ⦋𝑧 / 𝑘⦌𝑌) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌))))
238	237	adantr 276	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐶) ∧ (𝐺 Σ_g (𝑘 ∈ 𝑦 ↦ 𝑌)) = ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌)) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌)))) → ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌)) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌))) = (((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌)) + ⦋𝑧 / 𝑘⦌𝑌) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌))))
239	181, 238	eqtr4d 2274	. . . . 5 ⊢ (((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐶) ∧ (𝐺 Σ_g (𝑘 ∈ 𝑦 ↦ 𝑌)) = ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌)) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌)))) → (𝐺 Σ_g (𝑘 ∈ (𝑦 ∪ {𝑧}) ↦ 𝑌)) = ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌)) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌))))
240	239	ex 115	. . . 4 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐶) → ((𝐺 Σ_g (𝑘 ∈ 𝑦 ↦ 𝑌)) = ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌)) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌))) → (𝐺 Σ_g (𝑘 ∈ (𝑦 ∪ {𝑧}) ↦ 𝑌)) = ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌)) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌)))))
241	180	adantlr 481	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐷) ∧ (𝐺 Σ_g (𝑘 ∈ 𝑦 ↦ 𝑌)) = ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌)) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌)))) → (𝐺 Σ_g (𝑘 ∈ (𝑦 ∪ {𝑧}) ↦ 𝑌)) = (((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌)) + ⦋𝑧 / 𝑘⦌𝑌) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌))))
242	116, 118	sylib 122	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐷 ∩ 𝐶) = ∅)
243	242	ad2antrr 492	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (𝐷 ∩ 𝐶) = ∅)
244		disjel 3579	. . . . . . . . . . . . 13 ⊢ (((𝐷 ∩ 𝐶) = ∅ ∧ 𝑧 ∈ 𝐷) → ¬ 𝑧 ∈ 𝐶)
245	243, 244	sylan 283	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐷) → ¬ 𝑧 ∈ 𝐶)
246		disjsn 3771	. . . . . . . . . . . . . . . 16 ⊢ ((𝐶 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝐶)
247	246	biimpri 133	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑧 ∈ 𝐶 → (𝐶 ∩ {𝑧}) = ∅)
248	247	uneq2d 3383	. . . . . . . . . . . . . 14 ⊢ (¬ 𝑧 ∈ 𝐶 → ((𝐶 ∩ 𝑦) ∪ (𝐶 ∩ {𝑧})) = ((𝐶 ∩ 𝑦) ∪ ∅))
249		un0 3556	. . . . . . . . . . . . . 14 ⊢ ((𝐶 ∩ 𝑦) ∪ ∅) = (𝐶 ∩ 𝑦)
250	248, 249	eqtrdi 2287	. . . . . . . . . . . . 13 ⊢ (¬ 𝑧 ∈ 𝐶 → ((𝐶 ∩ 𝑦) ∪ (𝐶 ∩ {𝑧})) = (𝐶 ∩ 𝑦))
251	192, 250	eqtrid 2283	. . . . . . . . . . . 12 ⊢ (¬ 𝑧 ∈ 𝐶 → (𝐶 ∩ (𝑦 ∪ {𝑧})) = (𝐶 ∩ 𝑦))
252	245, 251	syl 14	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐷) → (𝐶 ∩ (𝑦 ∪ {𝑧})) = (𝐶 ∩ 𝑦))
253	252	mpteq1d 4217	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐷) → (𝑘 ∈ (𝐶 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌) = (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌))
254	253	oveq2d 6104	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐷) → (𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌)) = (𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌)))
255	66	adantr 276	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐷) → 𝐺 ∈ CMnd)
256		simp-4l 547	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐷) ∧ 𝑘 ∈ (𝐷 ∩ (𝑦 ∪ {𝑧}))) → 𝜑)
257		ssun2 3393	. . . . . . . . . . . . . . . . 17 ⊢ 𝐷 ⊆ (𝐶 ∪ 𝐷)
258	257, 120	sseqtrrid 3299	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐷 ⊆ 𝐴)
259	258	ad4antr 498	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐷) ∧ 𝑘 ∈ (𝐷 ∩ (𝑦 ∪ {𝑧}))) → 𝐷 ⊆ 𝐴)
260		elinel1 3415	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ (𝐷 ∩ (𝑦 ∪ {𝑧})) → 𝑘 ∈ 𝐷)
261	260	adantl 277	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐷) ∧ 𝑘 ∈ (𝐷 ∩ (𝑦 ∪ {𝑧}))) → 𝑘 ∈ 𝐷)
262	259, 261	sseldd 3249	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐷) ∧ 𝑘 ∈ (𝐷 ∩ (𝑦 ∪ {𝑧}))) → 𝑘 ∈ 𝐴)
263	256, 262, 82	syl2anc 415	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐷) ∧ 𝑘 ∈ (𝐷 ∩ (𝑦 ∪ {𝑧}))) → 𝑌 ∈ 𝐵)
264	263	fmpttd 5866	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐷) → (𝑘 ∈ (𝐷 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌):(𝐷 ∩ (𝑦 ∪ {𝑧}))⟶𝐵)
265		snssi 3859	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ 𝐷 → {𝑧} ⊆ 𝐷)
266		dfss1 3435	. . . . . . . . . . . . . . . . 17 ⊢ ({𝑧} ⊆ 𝐷 ↔ (𝐷 ∩ {𝑧}) = {𝑧})
267	265, 266	sylib 122	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ 𝐷 → (𝐷 ∩ {𝑧}) = {𝑧})
268	267	uneq2d 3383	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ 𝐷 → ((𝐷 ∩ 𝑦) ∪ (𝐷 ∩ {𝑧})) = ((𝐷 ∩ 𝑦) ∪ {𝑧}))
269	227, 268	eqtrid 2283	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ 𝐷 → (𝐷 ∩ (𝑦 ∪ {𝑧})) = ((𝐷 ∩ 𝑦) ∪ {𝑧}))
270	269	feq2d 5524	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ 𝐷 → ((𝑘 ∈ (𝐷 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌):(𝐷 ∩ (𝑦 ∪ {𝑧}))⟶𝐵 ↔ (𝑘 ∈ (𝐷 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌):((𝐷 ∩ 𝑦) ∪ {𝑧})⟶𝐵))
271	270	adantl 277	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐷) → ((𝑘 ∈ (𝐷 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌):(𝐷 ∩ (𝑦 ∪ {𝑧}))⟶𝐵 ↔ (𝑘 ∈ (𝐷 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌):((𝐷 ∩ 𝑦) ∪ {𝑧})⟶𝐵))
272	264, 271	mpbid 147	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐷) → (𝑘 ∈ (𝐷 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌):((𝐷 ∩ 𝑦) ∪ {𝑧})⟶𝐵)
273	170	adantr 276	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐷) → (𝐷 ∩ 𝑦) ∈ Fin)
274		simpr 110	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐷) → 𝑧 ∈ 𝐷)
275		simpr 110	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ 𝐷 ∧ 𝑧 ∈ 𝑦) → 𝑧 ∈ 𝑦)
276	275	con3i 641	. . . . . . . . . . . . . 14 ⊢ (¬ 𝑧 ∈ 𝑦 → ¬ (𝑧 ∈ 𝐷 ∧ 𝑧 ∈ 𝑦))
277		elin 3412	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ (𝐷 ∩ 𝑦) ↔ (𝑧 ∈ 𝐷 ∧ 𝑧 ∈ 𝑦))
278	276, 277	sylnibr 688	. . . . . . . . . . . . 13 ⊢ (¬ 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ (𝐷 ∩ 𝑦))
279	86, 278	syl 14	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ¬ 𝑧 ∈ (𝐷 ∩ 𝑦))
280	279	adantr 276	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐷) → ¬ 𝑧 ∈ (𝐷 ∩ 𝑦))
281	43, 46, 255, 272, 273, 274, 280	gsump1 14247	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐷) → (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌)) = ((𝐺 Σ_g ((𝑘 ∈ (𝐷 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌) ↾ (𝐷 ∩ 𝑦))) + ((𝑘 ∈ (𝐷 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌)‘𝑧)))
282		ssun1 3392	. . . . . . . . . . . . . . . 16 ⊢ (𝐷 ∩ 𝑦) ⊆ ((𝐷 ∩ 𝑦) ∪ (𝐷 ∩ {𝑧}))
283	282, 227	sseqtrri 3283	. . . . . . . . . . . . . . 15 ⊢ (𝐷 ∩ 𝑦) ⊆ (𝐷 ∩ (𝑦 ∪ {𝑧}))
284	283	a1i 9	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (𝐷 ∩ 𝑦) ⊆ (𝐷 ∩ (𝑦 ∪ {𝑧})))
285	284	resmptd 5117	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ((𝑘 ∈ (𝐷 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌) ↾ (𝐷 ∩ 𝑦)) = (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌))
286	285	oveq2d 6104	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (𝐺 Σ_g ((𝑘 ∈ (𝐷 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌) ↾ (𝐷 ∩ 𝑦))) = (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌)))
287	286	adantr 276	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐷) → (𝐺 Σ_g ((𝑘 ∈ (𝐷 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌) ↾ (𝐷 ∩ 𝑦))) = (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌)))
288		elin 3412	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (𝐷 ∩ (𝑦 ∪ {𝑧})) ↔ (𝑧 ∈ 𝐷 ∧ 𝑧 ∈ (𝑦 ∪ {𝑧})))
289	274, 94, 288	sylanblrc 420	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐷) → 𝑧 ∈ (𝐷 ∩ (𝑦 ∪ {𝑧})))
290	102	adantr 276	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐷) → ⦋𝑧 / 𝑘⦌𝑌 ∈ 𝐵)
291		eqid 2238	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (𝐷 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌) = (𝑘 ∈ (𝐷 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌)
292	291	fvmpts 5786	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ (𝐷 ∩ (𝑦 ∪ {𝑧})) ∧ ⦋𝑧 / 𝑘⦌𝑌 ∈ 𝐵) → ((𝑘 ∈ (𝐷 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌)‘𝑧) = ⦋𝑧 / 𝑘⦌𝑌)
293	289, 290, 292	syl2anc 415	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐷) → ((𝑘 ∈ (𝐷 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌)‘𝑧) = ⦋𝑧 / 𝑘⦌𝑌)
294	287, 293	oveq12d 6106	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐷) → ((𝐺 Σ_g ((𝑘 ∈ (𝐷 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌) ↾ (𝐷 ∩ 𝑦))) + ((𝑘 ∈ (𝐷 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌)‘𝑧)) = ((𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌)) + ⦋𝑧 / 𝑘⦌𝑌))
295	281, 294	eqtrd 2271	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐷) → (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌)) = ((𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌)) + ⦋𝑧 / 𝑘⦌𝑌))
296	254, 295	oveq12d 6106	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐷) → ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌)) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌))) = ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌)) + ((𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌)) + ⦋𝑧 / 𝑘⦌𝑌)))
297	43, 46	cmncom 14195	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ CMnd ∧ (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌)) ∈ 𝐵 ∧ ⦋𝑧 / 𝑘⦌𝑌 ∈ 𝐵) → ((𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌)) + ⦋𝑧 / 𝑘⦌𝑌) = (⦋𝑧 / 𝑘⦌𝑌 + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌))))
298	66, 175, 102, 297	syl3anc 1278	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ((𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌)) + ⦋𝑧 / 𝑘⦌𝑌) = (⦋𝑧 / 𝑘⦌𝑌 + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌))))
299	298	oveq2d 6104	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌)) + ((𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌)) + ⦋𝑧 / 𝑘⦌𝑌)) = ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌)) + (⦋𝑧 / 𝑘⦌𝑌 + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌)))))
300	42	ad2antrr 492	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → 𝐺 ∈ Mnd)
301	43, 46	mndass 13796	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ Mnd ∧ ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌)) ∈ 𝐵 ∧ ⦋𝑧 / 𝑘⦌𝑌 ∈ 𝐵 ∧ (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌)) ∈ 𝐵)) → (((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌)) + ⦋𝑧 / 𝑘⦌𝑌) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌))) = ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌)) + (⦋𝑧 / 𝑘⦌𝑌 + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌)))))
302	300, 150, 102, 175, 301	syl13anc 1280	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌)) + ⦋𝑧 / 𝑘⦌𝑌) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌))) = ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌)) + (⦋𝑧 / 𝑘⦌𝑌 + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌)))))
303	299, 302	eqtr4d 2274	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌)) + ((𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌)) + ⦋𝑧 / 𝑘⦌𝑌)) = (((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌)) + ⦋𝑧 / 𝑘⦌𝑌) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌))))
304	303	adantr 276	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐷) → ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌)) + ((𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌)) + ⦋𝑧 / 𝑘⦌𝑌)) = (((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌)) + ⦋𝑧 / 𝑘⦌𝑌) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌))))
305	296, 304	eqtrd 2271	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐷) → ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌)) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌))) = (((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌)) + ⦋𝑧 / 𝑘⦌𝑌) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌))))
306	305	adantr 276	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐷) ∧ (𝐺 Σ_g (𝑘 ∈ 𝑦 ↦ 𝑌)) = ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌)) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌)))) → ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌)) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌))) = (((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌)) + ⦋𝑧 / 𝑘⦌𝑌) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌))))
307	241, 306	eqtr4d 2274	. . . . 5 ⊢ (((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐷) ∧ (𝐺 Σ_g (𝑘 ∈ 𝑦 ↦ 𝑌)) = ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌)) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌)))) → (𝐺 Σ_g (𝑘 ∈ (𝑦 ∪ {𝑧}) ↦ 𝑌)) = ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌)) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌))))
308	307	ex 115	. . . 4 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑧 ∈ 𝐷) → ((𝐺 Σ_g (𝑘 ∈ 𝑦 ↦ 𝑌)) = ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌)) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌))) → (𝐺 Σ_g (𝑘 ∈ (𝑦 ∪ {𝑧}) ↦ 𝑌)) = ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌)) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌)))))
309	120	eleq2d 2308	. . . . . . 7 ⊢ (𝜑 → (𝑧 ∈ 𝐴 ↔ 𝑧 ∈ (𝐶 ∪ 𝐷)))
310	309	ad2antrr 492	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (𝑧 ∈ 𝐴 ↔ 𝑧 ∈ (𝐶 ∪ 𝐷)))
311	73, 310	mpbid 147	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → 𝑧 ∈ (𝐶 ∪ 𝐷))
312		elun 3370	. . . . 5 ⊢ (𝑧 ∈ (𝐶 ∪ 𝐷) ↔ (𝑧 ∈ 𝐶 ∨ 𝑧 ∈ 𝐷))
313	311, 312	sylib 122	. . . 4 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (𝑧 ∈ 𝐶 ∨ 𝑧 ∈ 𝐷))
314	240, 308, 313	mpjaodan 810	. . 3 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ((𝐺 Σ_g (𝑘 ∈ 𝑦 ↦ 𝑌)) = ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝑦) ↦ 𝑌)) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝑦) ↦ 𝑌))) → (𝐺 Σ_g (𝑘 ∈ (𝑦 ∪ {𝑧}) ↦ 𝑌)) = ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌)) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ (𝑦 ∪ {𝑧})) ↦ 𝑌)))))
315	10, 20, 30, 40, 65, 314, 112	findcard2sd 7200	. 2 ⊢ (𝜑 → (𝐺 Σ_g (𝑘 ∈ 𝐴 ↦ 𝑌)) = ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝐴) ↦ 𝑌)) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝐴) ↦ 𝑌))))
316		df-ss 3233	. . . . . 6 ⊢ (𝐶 ⊆ 𝐴 ↔ (𝐶 ∩ 𝐴) = 𝐶)
317	185, 316	sylib 122	. . . . 5 ⊢ (𝜑 → (𝐶 ∩ 𝐴) = 𝐶)
318	317	mpteq1d 4217	. . . 4 ⊢ (𝜑 → (𝑘 ∈ (𝐶 ∩ 𝐴) ↦ 𝑌) = (𝑘 ∈ 𝐶 ↦ 𝑌))
319	318	oveq2d 6104	. . 3 ⊢ (𝜑 → (𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝐴) ↦ 𝑌)) = (𝐺 Σ_g (𝑘 ∈ 𝐶 ↦ 𝑌)))
320		df-ss 3233	. . . . . 6 ⊢ (𝐷 ⊆ 𝐴 ↔ (𝐷 ∩ 𝐴) = 𝐷)
321	258, 320	sylib 122	. . . . 5 ⊢ (𝜑 → (𝐷 ∩ 𝐴) = 𝐷)
322	321	mpteq1d 4217	. . . 4 ⊢ (𝜑 → (𝑘 ∈ (𝐷 ∩ 𝐴) ↦ 𝑌) = (𝑘 ∈ 𝐷 ↦ 𝑌))
323	322	oveq2d 6104	. . 3 ⊢ (𝜑 → (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝐴) ↦ 𝑌)) = (𝐺 Σ_g (𝑘 ∈ 𝐷 ↦ 𝑌)))
324	319, 323	oveq12d 6106	. 2 ⊢ (𝜑 → ((𝐺 Σ_g (𝑘 ∈ (𝐶 ∩ 𝐴) ↦ 𝑌)) + (𝐺 Σ_g (𝑘 ∈ (𝐷 ∩ 𝐴) ↦ 𝑌))) = ((𝐺 Σ_g (𝑘 ∈ 𝐶 ↦ 𝑌)) + (𝐺 Σ_g (𝑘 ∈ 𝐷 ↦ 𝑌))))
325	315, 324	eqtrd 2271	1 ⊢ (𝜑 → (𝐺 Σ_g (𝑘 ∈ 𝐴 ↦ 𝑌)) = ((𝐺 Σ_g (𝑘 ∈ 𝐶 ↦ 𝑌)) + (𝐺 Σ_g (𝑘 ∈ 𝐷 ↦ 𝑌))))

Colors of variables: wff set class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 720 DECID wdc 846 = wceq 1402 ∈ wcel 2209 ∀wral 2528 ⦋csb 3147 ∖ cdif 3217 ∪ cun 3218 ∩ cin 3219 ⊆ wss 3220 ∅c0 3520 {csn 3709 ↦ cmpt 4193 ↾ cres 4778 ⟶wf 5376 ‘cfv 5380 (class class class)co 6088 Fincfn 7026 Basecbs 13410 +_gcplusg 13490 0_gc0g 13669 Mndcmnd 13788 CMndccmn 14177 Σ_g cgsu 14240

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 623 ax-in2 624 ax-io 721 ax-5 1500 ax-7 1501 ax-gen 1502 ax-ie1 1546 ax-ie2 1547 ax-8 1557 ax-10 1558 ax-11 1559 ax-i12 1560 ax-bndl 1562 ax-4 1563 ax-17 1579 ax-i9 1583 ax-ial 1587 ax-i5r 1588 ax-14 2212 ax-ext 2220 ax-coll 4248 ax-sep 4251 ax-nul 4261 ax-pow 4313 ax-pr 4348 ax-un 4580 ax-setind 4686 ax-iinf 4737 ax-cnex 8276 ax-resscn 8277 ax-1cn 8278 ax-1re 8279 ax-icn 8280 ax-addcl 8281 ax-addrcl 8282 ax-mulcl 8283 ax-mulrcl 8284 ax-addcom 8285 ax-mulcom 8286 ax-addass 8287 ax-mulass 8288 ax-distr 8289 ax-i2m1 8290 ax-0lt1 8291 ax-1rid 8292 ax-0id 8293 ax-rnegex 8294 ax-precex 8295 ax-cnre 8296 ax-pre-ltirr 8297 ax-pre-ltwlin 8298 ax-pre-lttrn 8299 ax-pre-apti 8300 ax-pre-ltadd 8301 ax-pre-mulgt0 8302

This proof depends on definitions: df-bi 117 df-stab 843 df-dc 847 df-3or 1010 df-3an 1011 df-tru 1405 df-fal 1408 df-nf 1514 df-sb 1816 df-eu 2089 df-mo 2090 df-clab 2225 df-cleq 2231 df-clel 2234 df-nfc 2381 df-ne 2421 df-nel 2516 df-ral 2533 df-rex 2534 df-reu 2535 df-rmo 2536 df-rab 2537 df-v 2823 df-sbc 3052 df-csb 3148 df-dif 3222 df-un 3224 df-in 3226 df-ss 3233 df-nul 3521 df-if 3639 df-pw 3690 df-sn 3715 df-pr 3716 df-op 3718 df-uni 3936 df-int 3971 df-iun 4014 df-br 4132 df-opab 4194 df-mpt 4195 df-tr 4232 df-id 4440 df-iord 4513 df-on 4515 df-ilim 4516 df-suc 4518 df-iom 4740 df-xp 4782 df-rel 4783 df-cnv 4784 df-co 4785 df-dm 4786 df-rn 4787 df-res 4788 df-ima 4789 df-iota 5340 df-fun 5382 df-fn 5383 df-f 5384 df-f1 5385 df-fo 5386 df-f1o 5387 df-fv 5388 df-riota 6041 df-ov 6091 df-oprab 6092 df-mpo 6093 df-1st 6378 df-2nd 6379 df-recs 6580 df-irdg 6645 df-frec 6666 df-1o 6691 df-oadd 6695 df-er 6811 df-en 7027 df-dom 7028 df-fin 7029 df-pnf 8368 df-mnf 8369 df-xr 8370 df-ltxr 8371 df-le 8372 df-sub 8506 df-neg 8507 df-reap 8911 df-ap 8918 df-inn 9314 df-2 9372 df-n0 9575 df-z 9656 df-uz 9938 df-fz 10429 df-fzo 10567 df-seqfrec 10906 df-ihash 11237 df-ndx 13413 df-slot 13414 df-base 13416 df-plusg 13503 df-0g 13671 df-gzsum 13672 df-mgm 13735 df-sgrp 13776 df-mnd 13789 df-minusg 13868 df-mulg 13982 df-cmn 14179 df-gsumfi 14241

This theorem is used by: gsummptfidmsplitres 14255 gsumunsnfd 14259

W3C validator