tsmsxplem1 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > tsmsxplem1		Structured version Visualization version GIF version

Theorem tsmsxplem1 23664

Description: Lemma for tsmsxp 23666. (Contributed by Mario Carneiro, 21-Sep-2015.)

**Hypotheses**
Ref	Expression
tsmsxp.b	⊢ 𝐵 = (Base‘𝐺)
tsmsxp.g	⊢ (𝜑 → 𝐺 ∈ CMnd)
tsmsxp.2	⊢ (𝜑 → 𝐺 ∈ TopGrp)
tsmsxp.a	⊢ (𝜑 → 𝐴 ∈ 𝑉)
tsmsxp.c	⊢ (𝜑 → 𝐶 ∈ 𝑊)
tsmsxp.f	⊢ (𝜑 → 𝐹:(𝐴 × 𝐶)⟶𝐵)
tsmsxp.h	⊢ (𝜑 → 𝐻:𝐴⟶𝐵)
tsmsxp.1	⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝐻‘𝑗) ∈ (𝐺 tsums (𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘))))
tsmsxp.j	⊢ 𝐽 = (TopOpen‘𝐺)
tsmsxp.z	⊢ 0 = (0_g‘𝐺)
tsmsxp.p	⊢ + = (+_g‘𝐺)
tsmsxp.m	⊢ − = (-_g‘𝐺)
tsmsxp.l	⊢ (𝜑 → 𝐿 ∈ 𝐽)
tsmsxp.3	⊢ (𝜑 → 0 ∈ 𝐿)
tsmsxp.k	⊢ (𝜑 → 𝐾 ∈ (𝒫 𝐴 ∩ Fin))
tsmsxp.ks	⊢ (𝜑 → dom 𝐷 ⊆ 𝐾)
tsmsxp.d	⊢ (𝜑 → 𝐷 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin))

**Assertion**
Ref	Expression
tsmsxplem1	⊢ (𝜑 → ∃𝑛 ∈ (𝒫 𝐶 ∩ Fin)(ran 𝐷 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿))

Distinct variable groups: 0 ,𝑘 𝑗,𝑘,𝑛,𝑥,𝐺 𝐵,𝑘 𝐷,𝑗,𝑘,𝑛,𝑥 𝑗,𝐿,𝑛,𝑥 𝐴,𝑗,𝑘,𝑛 𝑗,𝐾,𝑘,𝑛,𝑥 𝑗,𝐻,𝑘,𝑛,𝑥 − ,𝑗,𝑛,𝑥 𝐶,𝑗,𝑘,𝑛 𝑗,𝐹,𝑘,𝑛,𝑥 𝜑,𝑗,𝑘,𝑛 Allowed substitution hints: 𝜑(𝑥) 𝐴(𝑥) 𝐵(𝑥,𝑗,𝑛) 𝐶(𝑥) + (𝑥,𝑗,𝑘,𝑛) 𝐽(𝑥,𝑗,𝑘,𝑛) 𝐿(𝑘) − (𝑘) 𝑉(𝑥,𝑗,𝑘,𝑛) 𝑊(𝑥,𝑗,𝑘,𝑛) 0 (𝑥,𝑗,𝑛)

Proof of Theorem tsmsxplem1 Dummy variables 𝑔 𝑦 𝑧 𝑓 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		tsmsxp.k	. . . 4 ⊢ (𝜑 → 𝐾 ∈ (𝒫 𝐴 ∩ Fin))
2	1	elin2d 4199	. . 3 ⊢ (𝜑 → 𝐾 ∈ Fin)
3		elfpw 9356	. . . . . . . 8 ⊢ (𝐾 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝐾 ⊆ 𝐴 ∧ 𝐾 ∈ Fin))
4	3	simplbi 498	. . . . . . 7 ⊢ (𝐾 ∈ (𝒫 𝐴 ∩ Fin) → 𝐾 ⊆ 𝐴)
5	1, 4	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐾 ⊆ 𝐴)
6	5	sselda 3982	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐾) → 𝑗 ∈ 𝐴)
7		tsmsxp.b	. . . . . 6 ⊢ 𝐵 = (Base‘𝐺)
8		tsmsxp.j	. . . . . 6 ⊢ 𝐽 = (TopOpen‘𝐺)
9		eqid 2732	. . . . . 6 ⊢ (𝒫 𝐶 ∩ Fin) = (𝒫 𝐶 ∩ Fin)
10		tsmsxp.g	. . . . . . 7 ⊢ (𝜑 → 𝐺 ∈ CMnd)
11	10	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐺 ∈ CMnd)
12		tsmsxp.2	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ TopGrp)
13		tgptps 23591	. . . . . . . 8 ⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ TopSp)
14	12, 13	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐺 ∈ TopSp)
15	14	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐺 ∈ TopSp)
16		tsmsxp.c	. . . . . . 7 ⊢ (𝜑 → 𝐶 ∈ 𝑊)
17	16	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐶 ∈ 𝑊)
18		tsmsxp.f	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:(𝐴 × 𝐶)⟶𝐵)
19		fovcdm 7579	. . . . . . . . 9 ⊢ ((𝐹:(𝐴 × 𝐶)⟶𝐵 ∧ 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶) → (𝑗𝐹𝑘) ∈ 𝐵)
20	18, 19	syl3an1 1163	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶) → (𝑗𝐹𝑘) ∈ 𝐵)
21	20	3expa 1118	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴) ∧ 𝑘 ∈ 𝐶) → (𝑗𝐹𝑘) ∈ 𝐵)
22	21	fmpttd 7116	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)):𝐶⟶𝐵)
23		tsmsxp.1	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝐻‘𝑗) ∈ (𝐺 tsums (𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘))))
24		df-ima 5689	. . . . . . . 8 ⊢ ((𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) “ 𝐿) = ran ((𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) ↾ 𝐿)
25	8, 7	tgptopon 23593	. . . . . . . . . . . . 13 ⊢ (𝐺 ∈ TopGrp → 𝐽 ∈ (TopOn‘𝐵))
26	12, 25	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝐵))
27		tsmsxp.l	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐿 ∈ 𝐽)
28		toponss 22436	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ (TopOn‘𝐵) ∧ 𝐿 ∈ 𝐽) → 𝐿 ⊆ 𝐵)
29	26, 27, 28	syl2anc 584	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐿 ⊆ 𝐵)
30	29	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐿 ⊆ 𝐵)
31	30	resmptd 6040	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ((𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) ↾ 𝐿) = (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))
32	31	rneqd 5937	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ran ((𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) ↾ 𝐿) = ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))
33	24, 32	eqtrid 2784	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ((𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) “ 𝐿) = ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))
34		tsmsxp.h	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐻:𝐴⟶𝐵)
35	34	ffvelcdmda 7086	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝐻‘𝑗) ∈ 𝐵)
36		tsmsxp.p	. . . . . . . . . . . . 13 ⊢ + = (+_g‘𝐺)
37		eqid 2732	. . . . . . . . . . . . 13 ⊢ (inv_g‘𝐺) = (inv_g‘𝐺)
38		tsmsxp.m	. . . . . . . . . . . . 13 ⊢ − = (-_g‘𝐺)
39	7, 36, 37, 38	grpsubval 18872	. . . . . . . . . . . 12 ⊢ (((𝐻‘𝑗) ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → ((𝐻‘𝑗) − 𝑔) = ((𝐻‘𝑗) + ((inv_g‘𝐺)‘𝑔)))
40	35, 39	sylan 580	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴) ∧ 𝑔 ∈ 𝐵) → ((𝐻‘𝑗) − 𝑔) = ((𝐻‘𝑗) + ((inv_g‘𝐺)‘𝑔)))
41	40	mpteq2dva 5248	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) = (𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) + ((inv_g‘𝐺)‘𝑔))))
42		tgpgrp 23589	. . . . . . . . . . . . . 14 ⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ Grp)
43	12, 42	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐺 ∈ Grp)
44	43	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐺 ∈ Grp)
45	7, 37	grpinvcl 18874	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ Grp ∧ 𝑔 ∈ 𝐵) → ((inv_g‘𝐺)‘𝑔) ∈ 𝐵)
46	44, 45	sylan 580	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴) ∧ 𝑔 ∈ 𝐵) → ((inv_g‘𝐺)‘𝑔) ∈ 𝐵)
47	7, 37	grpinvf 18873	. . . . . . . . . . . . 13 ⊢ (𝐺 ∈ Grp → (inv_g‘𝐺):𝐵⟶𝐵)
48	44, 47	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (inv_g‘𝐺):𝐵⟶𝐵)
49	48	feqmptd 6960	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (inv_g‘𝐺) = (𝑔 ∈ 𝐵 ↦ ((inv_g‘𝐺)‘𝑔)))
50		eqidd 2733	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) = (𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)))
51		oveq2 7419	. . . . . . . . . . 11 ⊢ (𝑦 = ((inv_g‘𝐺)‘𝑔) → ((𝐻‘𝑗) + 𝑦) = ((𝐻‘𝑗) + ((inv_g‘𝐺)‘𝑔)))
52	46, 49, 50, 51	fmptco 7129	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ((𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) ∘ (inv_g‘𝐺)) = (𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) + ((inv_g‘𝐺)‘𝑔))))
53	41, 52	eqtr4d 2775	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) = ((𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) ∘ (inv_g‘𝐺)))
54	12	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐺 ∈ TopGrp)
55	8, 37	grpinvhmeo 23597	. . . . . . . . . . 11 ⊢ (𝐺 ∈ TopGrp → (inv_g‘𝐺) ∈ (𝐽Homeo𝐽))
56	54, 55	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (inv_g‘𝐺) ∈ (𝐽Homeo𝐽))
57		eqid 2732	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) = (𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦))
58	57, 7, 36, 8	tgplacthmeo 23614	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ TopGrp ∧ (𝐻‘𝑗) ∈ 𝐵) → (𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) ∈ (𝐽Homeo𝐽))
59	54, 35, 58	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) ∈ (𝐽Homeo𝐽))
60		hmeoco 23283	. . . . . . . . . 10 ⊢ (((inv_g‘𝐺) ∈ (𝐽Homeo𝐽) ∧ (𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) ∈ (𝐽Homeo𝐽)) → ((𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) ∘ (inv_g‘𝐺)) ∈ (𝐽Homeo𝐽))
61	56, 59, 60	syl2anc 584	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ((𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) ∘ (inv_g‘𝐺)) ∈ (𝐽Homeo𝐽))
62	53, 61	eqeltrd 2833	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) ∈ (𝐽Homeo𝐽))
63	27	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐿 ∈ 𝐽)
64		hmeoima 23276	. . . . . . . 8 ⊢ (((𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) ∈ (𝐽Homeo𝐽) ∧ 𝐿 ∈ 𝐽) → ((𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) “ 𝐿) ∈ 𝐽)
65	62, 63, 64	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ((𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) “ 𝐿) ∈ 𝐽)
66	33, 65	eqeltrrd 2834	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)) ∈ 𝐽)
67		tsmsxp.z	. . . . . . . . 9 ⊢ 0 = (0_g‘𝐺)
68	7, 67, 38	grpsubid1 18910	. . . . . . . 8 ⊢ ((𝐺 ∈ Grp ∧ (𝐻‘𝑗) ∈ 𝐵) → ((𝐻‘𝑗) − 0 ) = (𝐻‘𝑗))
69	44, 35, 68	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ((𝐻‘𝑗) − 0 ) = (𝐻‘𝑗))
70		tsmsxp.3	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ 𝐿)
71	70	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 0 ∈ 𝐿)
72		ovex 7444	. . . . . . . 8 ⊢ ((𝐻‘𝑗) − 0 ) ∈ V
73		eqid 2732	. . . . . . . . 9 ⊢ (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)) = (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))
74		oveq2 7419	. . . . . . . . 9 ⊢ (𝑔 = 0 → ((𝐻‘𝑗) − 𝑔) = ((𝐻‘𝑗) − 0 ))
75	73, 74	elrnmpt1s 5956	. . . . . . . 8 ⊢ (( 0 ∈ 𝐿 ∧ ((𝐻‘𝑗) − 0 ) ∈ V) → ((𝐻‘𝑗) − 0 ) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))
76	71, 72, 75	sylancl 586	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ((𝐻‘𝑗) − 0 ) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))
77	69, 76	eqeltrrd 2834	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝐻‘𝑗) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))
78	7, 8, 9, 11, 15, 17, 22, 23, 66, 77	tsmsi 23645	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ∃𝑦 ∈ (𝒫 𝐶 ∩ Fin)∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))
79	6, 78	syldan 591	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐾) → ∃𝑦 ∈ (𝒫 𝐶 ∩ Fin)∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))
80	79	ralrimiva 3146	. . 3 ⊢ (𝜑 → ∀𝑗 ∈ 𝐾 ∃𝑦 ∈ (𝒫 𝐶 ∩ Fin)∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))
81		sseq1 4007	. . . . . 6 ⊢ (𝑦 = (𝑓‘𝑗) → (𝑦 ⊆ 𝑧 ↔ (𝑓‘𝑗) ⊆ 𝑧))
82	81	imbi1d 341	. . . . 5 ⊢ (𝑦 = (𝑓‘𝑗) → ((𝑦 ⊆ 𝑧 → (𝐺 Σ_g ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) ↔ ((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σ_g ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))))
83	82	ralbidv 3177	. . . 4 ⊢ (𝑦 = (𝑓‘𝑗) → (∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) ↔ ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σ_g ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))))
84	83	ac6sfi 9289	. . 3 ⊢ ((𝐾 ∈ Fin ∧ ∀𝑗 ∈ 𝐾 ∃𝑦 ∈ (𝒫 𝐶 ∩ Fin)∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))) → ∃𝑓(𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗 ∈ 𝐾 ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σ_g ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))))
85	2, 80, 84	syl2anc 584	. 2 ⊢ (𝜑 → ∃𝑓(𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗 ∈ 𝐾 ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σ_g ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))))
86		frn 6724	. . . . . . . . 9 ⊢ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) → ran 𝑓 ⊆ (𝒫 𝐶 ∩ Fin))
87	86	adantl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝑓 ⊆ (𝒫 𝐶 ∩ Fin))
88		inss1 4228	. . . . . . . 8 ⊢ (𝒫 𝐶 ∩ Fin) ⊆ 𝒫 𝐶
89	87, 88	sstrdi 3994	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝑓 ⊆ 𝒫 𝐶)
90		sspwuni 5103	. . . . . . 7 ⊢ (ran 𝑓 ⊆ 𝒫 𝐶 ↔ ∪ ran 𝑓 ⊆ 𝐶)
91	89, 90	sylib 217	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ∪ ran 𝑓 ⊆ 𝐶)
92		tsmsxp.d	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin))
93		elfpw 9356	. . . . . . . . . 10 ⊢ (𝐷 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ↔ (𝐷 ⊆ (𝐴 × 𝐶) ∧ 𝐷 ∈ Fin))
94	93	simplbi 498	. . . . . . . . 9 ⊢ (𝐷 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) → 𝐷 ⊆ (𝐴 × 𝐶))
95		rnss 5938	. . . . . . . . 9 ⊢ (𝐷 ⊆ (𝐴 × 𝐶) → ran 𝐷 ⊆ ran (𝐴 × 𝐶))
96	92, 94, 95	3syl 18	. . . . . . . 8 ⊢ (𝜑 → ran 𝐷 ⊆ ran (𝐴 × 𝐶))
97		rnxpss 6171	. . . . . . . 8 ⊢ ran (𝐴 × 𝐶) ⊆ 𝐶
98	96, 97	sstrdi 3994	. . . . . . 7 ⊢ (𝜑 → ran 𝐷 ⊆ 𝐶)
99	98	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝐷 ⊆ 𝐶)
100	91, 99	unssd 4186	. . . . 5 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∪ ran 𝑓 ∪ ran 𝐷) ⊆ 𝐶)
101	2	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝐾 ∈ Fin)
102		ffn 6717	. . . . . . . . . 10 ⊢ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) → 𝑓 Fn 𝐾)
103	102	adantl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝑓 Fn 𝐾)
104		dffn4 6811	. . . . . . . . 9 ⊢ (𝑓 Fn 𝐾 ↔ 𝑓:𝐾–onto→ran 𝑓)
105	103, 104	sylib 217	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝑓:𝐾–onto→ran 𝑓)
106		fofi 9340	. . . . . . . 8 ⊢ ((𝐾 ∈ Fin ∧ 𝑓:𝐾–onto→ran 𝑓) → ran 𝑓 ∈ Fin)
107	101, 105, 106	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝑓 ∈ Fin)
108		inss2 4229	. . . . . . . 8 ⊢ (𝒫 𝐶 ∩ Fin) ⊆ Fin
109	87, 108	sstrdi 3994	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝑓 ⊆ Fin)
110		unifi 9343	. . . . . . 7 ⊢ ((ran 𝑓 ∈ Fin ∧ ran 𝑓 ⊆ Fin) → ∪ ran 𝑓 ∈ Fin)
111	107, 109, 110	syl2anc 584	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ∪ ran 𝑓 ∈ Fin)
112		elinel2 4196	. . . . . . . 8 ⊢ (𝐷 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) → 𝐷 ∈ Fin)
113		rnfi 9337	. . . . . . . 8 ⊢ (𝐷 ∈ Fin → ran 𝐷 ∈ Fin)
114	92, 112, 113	3syl 18	. . . . . . 7 ⊢ (𝜑 → ran 𝐷 ∈ Fin)
115	114	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝐷 ∈ Fin)
116		unfi 9174	. . . . . 6 ⊢ ((∪ ran 𝑓 ∈ Fin ∧ ran 𝐷 ∈ Fin) → (∪ ran 𝑓 ∪ ran 𝐷) ∈ Fin)
117	111, 115, 116	syl2anc 584	. . . . 5 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∪ ran 𝑓 ∪ ran 𝐷) ∈ Fin)
118		elfpw 9356	. . . . 5 ⊢ ((∪ ran 𝑓 ∪ ran 𝐷) ∈ (𝒫 𝐶 ∩ Fin) ↔ ((∪ ran 𝑓 ∪ ran 𝐷) ⊆ 𝐶 ∧ (∪ ran 𝑓 ∪ ran 𝐷) ∈ Fin))
119	100, 117, 118	sylanbrc 583	. . . 4 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∪ ran 𝑓 ∪ ran 𝐷) ∈ (𝒫 𝐶 ∩ Fin))
120	119	adantrr 715	. . 3 ⊢ ((𝜑 ∧ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗 ∈ 𝐾 ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σ_g ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))) → (∪ ran 𝑓 ∪ ran 𝐷) ∈ (𝒫 𝐶 ∩ Fin))
121		ssun2 4173	. . . 4 ⊢ ran 𝐷 ⊆ (∪ ran 𝑓 ∪ ran 𝐷)
122	121	a1i 11	. . 3 ⊢ ((𝜑 ∧ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗 ∈ 𝐾 ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σ_g ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))) → ran 𝐷 ⊆ (∪ ran 𝑓 ∪ ran 𝐷))
123	119	adantlr 713	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∪ ran 𝑓 ∪ ran 𝐷) ∈ (𝒫 𝐶 ∩ Fin))
124		fvssunirn 6924	. . . . . . . . . . . . . 14 ⊢ (𝑓‘𝑗) ⊆ ∪ ran 𝑓
125		ssun1 4172	. . . . . . . . . . . . . 14 ⊢ ∪ ran 𝑓 ⊆ (∪ ran 𝑓 ∪ ran 𝐷)
126	124, 125	sstri 3991	. . . . . . . . . . . . 13 ⊢ (𝑓‘𝑗) ⊆ (∪ ran 𝑓 ∪ ran 𝐷)
127		id 22	. . . . . . . . . . . . 13 ⊢ (𝑧 = (∪ ran 𝑓 ∪ ran 𝐷) → 𝑧 = (∪ ran 𝑓 ∪ ran 𝐷))
128	126, 127	sseqtrrid 4035	. . . . . . . . . . . 12 ⊢ (𝑧 = (∪ ran 𝑓 ∪ ran 𝐷) → (𝑓‘𝑗) ⊆ 𝑧)
129		pm5.5 361	. . . . . . . . . . . 12 ⊢ ((𝑓‘𝑗) ⊆ 𝑧 → (((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σ_g ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) ↔ (𝐺 Σ_g ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))
130	128, 129	syl 17	. . . . . . . . . . 11 ⊢ (𝑧 = (∪ ran 𝑓 ∪ ran 𝐷) → (((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σ_g ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) ↔ (𝐺 Σ_g ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))
131		reseq2 5976	. . . . . . . . . . . . 13 ⊢ (𝑧 = (∪ ran 𝑓 ∪ ran 𝐷) → ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧) = ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran 𝑓 ∪ ran 𝐷)))
132	131	oveq2d 7427	. . . . . . . . . . . 12 ⊢ (𝑧 = (∪ ran 𝑓 ∪ ran 𝐷) → (𝐺 Σ_g ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) = (𝐺 Σ_g ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran 𝑓 ∪ ran 𝐷))))
133	132	eleq1d 2818	. . . . . . . . . . 11 ⊢ (𝑧 = (∪ ran 𝑓 ∪ ran 𝐷) → ((𝐺 Σ_g ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)) ↔ (𝐺 Σ_g ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran 𝑓 ∪ ran 𝐷))) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))
134	130, 133	bitrd 278	. . . . . . . . . 10 ⊢ (𝑧 = (∪ ran 𝑓 ∪ ran 𝐷) → (((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σ_g ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) ↔ (𝐺 Σ_g ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran 𝑓 ∪ ran 𝐷))) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))
135	134	rspcv 3608	. . . . . . . . 9 ⊢ ((∪ ran 𝑓 ∪ ran 𝐷) ∈ (𝒫 𝐶 ∩ Fin) → (∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σ_g ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) → (𝐺 Σ_g ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran 𝑓 ∪ ran 𝐷))) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))
136	123, 135	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σ_g ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) → (𝐺 Σ_g ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran 𝑓 ∪ ran 𝐷))) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))
137	10	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝐺 ∈ CMnd)
138		cmnmnd 19667	. . . . . . . . . . . . 13 ⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd)
139	137, 138	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝐺 ∈ Mnd)
140		simplr 767	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝑗 ∈ 𝐾)
141	117	adantlr 713	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∪ ran 𝑓 ∪ ran 𝐷) ∈ Fin)
142	100	adantlr 713	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∪ ran 𝑓 ∪ ran 𝐷) ⊆ 𝐶)
143	142	sselda 3982	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷)) → 𝑘 ∈ 𝐶)
144	18	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐾) → 𝐹:(𝐴 × 𝐶)⟶𝐵)
145	144, 6	jca 512	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐾) → (𝐹:(𝐴 × 𝐶)⟶𝐵 ∧ 𝑗 ∈ 𝐴))
146	19	3expa 1118	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹:(𝐴 × 𝐶)⟶𝐵 ∧ 𝑗 ∈ 𝐴) ∧ 𝑘 ∈ 𝐶) → (𝑗𝐹𝑘) ∈ 𝐵)
147	145, 146	sylan 580	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑘 ∈ 𝐶) → (𝑗𝐹𝑘) ∈ 𝐵)
148	147	adantlr 713	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ 𝐶) → (𝑗𝐹𝑘) ∈ 𝐵)
149	143, 148	syldan 591	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷)) → (𝑗𝐹𝑘) ∈ 𝐵)
150	149	fmpttd 7116	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘)):(∪ ran 𝑓 ∪ ran 𝐷)⟶𝐵)
151		eqid 2732	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘)) = (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))
152		ovexd 7446	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷)) → (𝑗𝐹𝑘) ∈ V)
153	67	fvexi 6905	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ V
154	153	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 0 ∈ V)
155	151, 141, 152, 154	fsuppmptdm 9376	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘)) finSupp 0 )
156	7, 67, 137, 141, 150, 155	gsumcl 19785	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐺 Σ_g (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))) ∈ 𝐵)
157		velsn 4644	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ {𝑗} ↔ 𝑦 = 𝑗)
158		ovres 7575	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ {𝑗} ∧ 𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷)) → (𝑦(𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))𝑘) = (𝑦𝐹𝑘))
159	157, 158	sylanbr 582	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 = 𝑗 ∧ 𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷)) → (𝑦(𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))𝑘) = (𝑦𝐹𝑘))
160		oveq1 7418	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑗 → (𝑦𝐹𝑘) = (𝑗𝐹𝑘))
161	160	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 = 𝑗 ∧ 𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷)) → (𝑦𝐹𝑘) = (𝑗𝐹𝑘))
162	159, 161	eqtrd 2772	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 = 𝑗 ∧ 𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷)) → (𝑦(𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))𝑘) = (𝑗𝐹𝑘))
163	162	mpteq2dva 5248	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑗 → (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑦(𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))𝑘)) = (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘)))
164	163	oveq2d 7427	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑗 → (𝐺 Σ_g (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑦(𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))𝑘))) = (𝐺 Σ_g (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))))
165	7, 164	gsumsn 19824	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ Mnd ∧ 𝑗 ∈ 𝐾 ∧ (𝐺 Σ_g (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))) ∈ 𝐵) → (𝐺 Σ_g (𝑦 ∈ {𝑗} ↦ (𝐺 Σ_g (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑦(𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))𝑘))))) = (𝐺 Σ_g (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))))
166	139, 140, 156, 165	syl3anc 1371	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐺 Σ_g (𝑦 ∈ {𝑗} ↦ (𝐺 Σ_g (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑦(𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))𝑘))))) = (𝐺 Σ_g (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))))
167		snfi 9046	. . . . . . . . . . . . 13 ⊢ {𝑗} ∈ Fin
168	167	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → {𝑗} ∈ Fin)
169	18	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝐹:(𝐴 × 𝐶)⟶𝐵)
170	6	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝑗 ∈ 𝐴)
171	170	snssd 4812	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → {𝑗} ⊆ 𝐴)
172		xpss12 5691	. . . . . . . . . . . . . 14 ⊢ (({𝑗} ⊆ 𝐴 ∧ (∪ ran 𝑓 ∪ ran 𝐷) ⊆ 𝐶) → ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)) ⊆ (𝐴 × 𝐶))
173	171, 142, 172	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)) ⊆ (𝐴 × 𝐶))
174	169, 173	fssresd 6758	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))):({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))⟶𝐵)
175		xpfi 9319	. . . . . . . . . . . . . 14 ⊢ (({𝑗} ∈ Fin ∧ (∪ ran 𝑓 ∪ ran 𝐷) ∈ Fin) → ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)) ∈ Fin)
176	167, 141, 175	sylancr 587	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)) ∈ Fin)
177	174, 176, 154	fdmfifsupp 9375	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))) finSupp 0 )
178	7, 67, 137, 168, 141, 174, 177	gsumxp 19846	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐺 Σ_g (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))) = (𝐺 Σ_g (𝑦 ∈ {𝑗} ↦ (𝐺 Σ_g (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑦(𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))𝑘))))))
179	142	resmptd 6040	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran 𝑓 ∪ ran 𝐷)) = (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘)))
180	179	oveq2d 7427	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐺 Σ_g ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran 𝑓 ∪ ran 𝐷))) = (𝐺 Σ_g (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))))
181	166, 178, 180	3eqtr4rd 2783	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐺 Σ_g ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran 𝑓 ∪ ran 𝐷))) = (𝐺 Σ_g (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))))
182	181	eleq1d 2818	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ((𝐺 Σ_g ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran 𝑓 ∪ ran 𝐷))) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)) ↔ (𝐺 Σ_g (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))
183		ovex 7444	. . . . . . . . . . 11 ⊢ ((𝐻‘𝑗) − 𝑔) ∈ V
184	73, 183	elrnmpti 5959	. . . . . . . . . 10 ⊢ ((𝐺 Σ_g (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)) ↔ ∃𝑔 ∈ 𝐿 (𝐺 Σ_g (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))) = ((𝐻‘𝑗) − 𝑔))
185		isabl 19654	. . . . . . . . . . . . . . . 16 ⊢ (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd))
186	43, 10, 185	sylanbrc 583	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐺 ∈ Abel)
187	186	ad3antrrr 728	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔 ∈ 𝐿) → 𝐺 ∈ Abel)
188	6, 35	syldan 591	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐾) → (𝐻‘𝑗) ∈ 𝐵)
189	188	ad2antrr 724	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔 ∈ 𝐿) → (𝐻‘𝑗) ∈ 𝐵)
190	29	ad2antrr 724	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝐿 ⊆ 𝐵)
191	190	sselda 3982	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔 ∈ 𝐿) → 𝑔 ∈ 𝐵)
192	7, 38, 187, 189, 191	ablnncan 19690	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔 ∈ 𝐿) → ((𝐻‘𝑗) − ((𝐻‘𝑗) − 𝑔)) = 𝑔)
193		simpr 485	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔 ∈ 𝐿) → 𝑔 ∈ 𝐿)
194	192, 193	eqeltrd 2833	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔 ∈ 𝐿) → ((𝐻‘𝑗) − ((𝐻‘𝑗) − 𝑔)) ∈ 𝐿)
195		oveq2 7419	. . . . . . . . . . . . 13 ⊢ ((𝐺 Σ_g (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))) = ((𝐻‘𝑗) − 𝑔) → ((𝐻‘𝑗) − (𝐺 Σ_g (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) = ((𝐻‘𝑗) − ((𝐻‘𝑗) − 𝑔)))
196	195	eleq1d 2818	. . . . . . . . . . . 12 ⊢ ((𝐺 Σ_g (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))) = ((𝐻‘𝑗) − 𝑔) → (((𝐻‘𝑗) − (𝐺 Σ_g (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿 ↔ ((𝐻‘𝑗) − ((𝐻‘𝑗) − 𝑔)) ∈ 𝐿))
197	194, 196	syl5ibrcom 246	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔 ∈ 𝐿) → ((𝐺 Σ_g (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))) = ((𝐻‘𝑗) − 𝑔) → ((𝐻‘𝑗) − (𝐺 Σ_g (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
198	197	rexlimdva 3155	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∃𝑔 ∈ 𝐿 (𝐺 Σ_g (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))) = ((𝐻‘𝑗) − 𝑔) → ((𝐻‘𝑗) − (𝐺 Σ_g (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
199	184, 198	biimtrid 241	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ((𝐺 Σ_g (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)) → ((𝐻‘𝑗) − (𝐺 Σ_g (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
200	182, 199	sylbid 239	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ((𝐺 Σ_g ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran 𝑓 ∪ ran 𝐷))) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)) → ((𝐻‘𝑗) − (𝐺 Σ_g (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
201	136, 200	syld 47	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σ_g ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) → ((𝐻‘𝑗) − (𝐺 Σ_g (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
202	201	an32s 650	. . . . . 6 ⊢ (((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑗 ∈ 𝐾) → (∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σ_g ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) → ((𝐻‘𝑗) − (𝐺 Σ_g (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
203	202	ralimdva 3167	. . . . 5 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∀𝑗 ∈ 𝐾 ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σ_g ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) → ∀𝑗 ∈ 𝐾 ((𝐻‘𝑗) − (𝐺 Σ_g (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
204	203	impr 455	. . . 4 ⊢ ((𝜑 ∧ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗 ∈ 𝐾 ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σ_g ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))) → ∀𝑗 ∈ 𝐾 ((𝐻‘𝑗) − (𝐺 Σ_g (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿)
205		fveq2 6891	. . . . . . 7 ⊢ (𝑗 = 𝑥 → (𝐻‘𝑗) = (𝐻‘𝑥))
206		sneq 4638	. . . . . . . . . 10 ⊢ (𝑗 = 𝑥 → {𝑗} = {𝑥})
207	206	xpeq1d 5705	. . . . . . . . 9 ⊢ (𝑗 = 𝑥 → ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)) = ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷)))
208	207	reseq2d 5981	. . . . . . . 8 ⊢ (𝑗 = 𝑥 → (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))) = (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷))))
209	208	oveq2d 7427	. . . . . . 7 ⊢ (𝑗 = 𝑥 → (𝐺 Σ_g (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))) = (𝐺 Σ_g (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷)))))
210	205, 209	oveq12d 7429	. . . . . 6 ⊢ (𝑗 = 𝑥 → ((𝐻‘𝑗) − (𝐺 Σ_g (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) = ((𝐻‘𝑥) − (𝐺 Σ_g (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷))))))
211	210	eleq1d 2818	. . . . 5 ⊢ (𝑗 = 𝑥 → (((𝐻‘𝑗) − (𝐺 Σ_g (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿 ↔ ((𝐻‘𝑥) − (𝐺 Σ_g (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
212	211	cbvralvw 3234	. . . 4 ⊢ (∀𝑗 ∈ 𝐾 ((𝐻‘𝑗) − (𝐺 Σ_g (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿 ↔ ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σ_g (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿)
213	204, 212	sylib 217	. . 3 ⊢ ((𝜑 ∧ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗 ∈ 𝐾 ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σ_g ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))) → ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σ_g (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿)
214		sseq2 4008	. . . . 5 ⊢ (𝑛 = (∪ ran 𝑓 ∪ ran 𝐷) → (ran 𝐷 ⊆ 𝑛 ↔ ran 𝐷 ⊆ (∪ ran 𝑓 ∪ ran 𝐷)))
215		xpeq2 5697	. . . . . . . . . 10 ⊢ (𝑛 = (∪ ran 𝑓 ∪ ran 𝐷) → ({𝑥} × 𝑛) = ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷)))
216	215	reseq2d 5981	. . . . . . . . 9 ⊢ (𝑛 = (∪ ran 𝑓 ∪ ran 𝐷) → (𝐹 ↾ ({𝑥} × 𝑛)) = (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷))))
217	216	oveq2d 7427	. . . . . . . 8 ⊢ (𝑛 = (∪ ran 𝑓 ∪ ran 𝐷) → (𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛))) = (𝐺 Σ_g (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷)))))
218	217	oveq2d 7427	. . . . . . 7 ⊢ (𝑛 = (∪ ran 𝑓 ∪ ran 𝐷) → ((𝐻‘𝑥) − (𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) = ((𝐻‘𝑥) − (𝐺 Σ_g (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷))))))
219	218	eleq1d 2818	. . . . . 6 ⊢ (𝑛 = (∪ ran 𝑓 ∪ ran 𝐷) → (((𝐻‘𝑥) − (𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿 ↔ ((𝐻‘𝑥) − (𝐺 Σ_g (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
220	219	ralbidv 3177	. . . . 5 ⊢ (𝑛 = (∪ ran 𝑓 ∪ ran 𝐷) → (∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿 ↔ ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σ_g (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
221	214, 220	anbi12d 631	. . . 4 ⊢ (𝑛 = (∪ ran 𝑓 ∪ ran 𝐷) → ((ran 𝐷 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿) ↔ (ran 𝐷 ⊆ (∪ ran 𝑓 ∪ ran 𝐷) ∧ ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σ_g (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿)))
222	221	rspcev 3612	. . 3 ⊢ (((∪ ran 𝑓 ∪ ran 𝐷) ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝐷 ⊆ (∪ ran 𝑓 ∪ ran 𝐷) ∧ ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σ_g (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿)) → ∃𝑛 ∈ (𝒫 𝐶 ∩ Fin)(ran 𝐷 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿))
223	120, 122, 213, 222	syl12anc 835	. 2 ⊢ ((𝜑 ∧ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗 ∈ 𝐾 ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σ_g ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))) → ∃𝑛 ∈ (𝒫 𝐶 ∩ Fin)(ran 𝐷 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿))
224	85, 223	exlimddv 1938	1 ⊢ (𝜑 → ∃𝑛 ∈ (𝒫 𝐶 ∩ Fin)(ran 𝐷 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1541 ∃wex 1781 ∈ wcel 2106 ∀wral 3061 ∃wrex 3070 Vcvv 3474 ∪ cun 3946 ∩ cin 3947 ⊆ wss 3948 𝒫 cpw 4602 {csn 4628 ∪ cuni 4908 ↦ cmpt 5231 × cxp 5674 dom cdm 5676 ran crn 5677 ↾ cres 5678 “ cima 5679 ∘ ccom 5680 Fn wfn 6538 ⟶wf 6539 –onto→wfo 6541 ‘cfv 6543 (class class class)co 7411 Fincfn 8941 Basecbs 17146 +_gcplusg 17199 TopOpenctopn 17369 0_gc0g 17387 Σ_g cgsu 17388 Mndcmnd 18627 Grpcgrp 18821 inv_gcminusg 18822 -_gcsg 18823 CMndccmn 19650 Abelcabl 19651 TopOnctopon 22419 TopSpctps 22441 Homeochmeo 23264 TopGrpctgp 23582 tsums ctsu 23637

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7727 ax-cnex 11168 ax-resscn 11169 ax-1cn 11170 ax-icn 11171 ax-addcl 11172 ax-addrcl 11173 ax-mulcl 11174 ax-mulrcl 11175 ax-mulcom 11176 ax-addass 11177 ax-mulass 11178 ax-distr 11179 ax-i2m1 11180 ax-1ne0 11181 ax-1rid 11182 ax-rnegex 11183 ax-rrecex 11184 ax-cnre 11185 ax-pre-lttri 11186 ax-pre-lttrn 11187 ax-pre-ltadd 11188 ax-pre-mulgt0 11189

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3376 df-reu 3377 df-rab 3433 df-v 3476 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-pss 3967 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-int 4951 df-iun 4999 df-iin 5000 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5574 df-eprel 5580 df-po 5588 df-so 5589 df-fr 5631 df-se 5632 df-we 5633 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-pred 6300 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6495 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-isom 6552 df-riota 7367 df-ov 7414 df-oprab 7415 df-mpo 7416 df-of 7672 df-om 7858 df-1st 7977 df-2nd 7978 df-supp 8149 df-frecs 8268 df-wrecs 8299 df-recs 8373 df-rdg 8412 df-1o 8468 df-er 8705 df-map 8824 df-en 8942 df-dom 8943 df-sdom 8944 df-fin 8945 df-fsupp 9364 df-oi 9507 df-card 9936 df-pnf 11252 df-mnf 11253 df-xr 11254 df-ltxr 11255 df-le 11256 df-sub 11448 df-neg 11449 df-nn 12215 df-2 12277 df-n0 12475 df-z 12561 df-uz 12825 df-fz 13487 df-fzo 13630 df-seq 13969 df-hash 14293 df-sets 17099 df-slot 17117 df-ndx 17129 df-base 17147 df-ress 17176 df-plusg 17212 df-0g 17389 df-gsum 17390 df-topgen 17391 df-mre 17532 df-mrc 17533 df-acs 17535 df-plusf 18562 df-mgm 18563 df-sgrp 18612 df-mnd 18628 df-submnd 18674 df-grp 18824 df-minusg 18825 df-sbg 18826 df-mulg 18953 df-cntz 19183 df-cmn 19652 df-abl 19653 df-fbas 20947 df-fg 20948 df-top 22403 df-topon 22420 df-topsp 22442 df-bases 22456 df-ntr 22531 df-nei 22609 df-cn 22738 df-cnp 22739 df-tx 23073 df-hmeo 23266 df-fil 23357 df-fm 23449 df-flim 23450 df-flf 23451 df-tmd 23583 df-tgp 23584 df-tsms 23638

This theorem is referenced by: tsmsxp 23666

W3C validator