Theorem tsmsxplem1 24118

Description: Lemma for tsmsxp 24120. (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 = (0g‘𝐺)
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 4145	. . 3 ⊢ (𝜑 → 𝐾 ∈ Fin)
3		elfpw 9264	. . . . . . . 8 ⊢ (𝐾 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝐾 ⊆ 𝐴 ∧ 𝐾 ∈ Fin))
4	3	simplbi 496	. . . . . . 7 ⊢ (𝐾 ∈ (𝒫 𝐴 ∩ Fin) → 𝐾 ⊆ 𝐴)
5	1, 4	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐾 ⊆ 𝐴)
6	5	sselda 3921	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐾) → 𝑗 ∈ 𝐴)
7		tsmsxp.b	. . . . . 6 ⊢ 𝐵 = (Base‘𝐺)
8		tsmsxp.j	. . . . . 6 ⊢ 𝐽 = (TopOpen‘𝐺)
9		eqid 2736	. . . . . 6 ⊢ (𝒫 𝐶 ∩ Fin) = (𝒫 𝐶 ∩ Fin)
10		tsmsxp.g	. . . . . . 7 ⊢ (𝜑 → 𝐺 ∈ CMnd)
11	10	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐺 ∈ CMnd)
12		tsmsxp.2	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ TopGrp)
13		tgptps 24045	. . . . . . . 8 ⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ TopSp)
14	12, 13	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐺 ∈ TopSp)
15	14	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐺 ∈ TopSp)
16		tsmsxp.c	. . . . . . 7 ⊢ (𝜑 → 𝐶 ∈ 𝑊)
17	16	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐶 ∈ 𝑊)
18		tsmsxp.f	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:(𝐴 × 𝐶)⟶𝐵)
19		fovcdm 7537	. . . . . . . . 9 ⊢ ((𝐹:(𝐴 × 𝐶)⟶𝐵 ∧ 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶) → (𝑗𝐹𝑘) ∈ 𝐵)
20	18, 19	syl3an1 1164	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶) → (𝑗𝐹𝑘) ∈ 𝐵)
21	20	3expa 1119	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴) ∧ 𝑘 ∈ 𝐶) → (𝑗𝐹𝑘) ∈ 𝐵)
22	21	fmpttd 7067	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)):𝐶⟶𝐵)
23		tsmsxp.1	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝐻‘𝑗) ∈ (𝐺 tsums (𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘))))
24		df-ima 5644	. . . . . . . 8 ⊢ ((𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) “ 𝐿) = ran ((𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) ↾ 𝐿)
25	8, 7	tgptopon 24047	. . . . . . . . . . . . 13 ⊢ (𝐺 ∈ TopGrp → 𝐽 ∈ (TopOn‘𝐵))
26	12, 25	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝐵))
27		tsmsxp.l	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐿 ∈ 𝐽)
28		toponss 22892	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ (TopOn‘𝐵) ∧ 𝐿 ∈ 𝐽) → 𝐿 ⊆ 𝐵)
29	26, 27, 28	syl2anc 585	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐿 ⊆ 𝐵)
30	29	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐿 ⊆ 𝐵)
31	30	resmptd 6005	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ((𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) ↾ 𝐿) = (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))
32	31	rneqd 5893	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ran ((𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) ↾ 𝐿) = ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))
33	24, 32	eqtrid 2783	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ((𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) “ 𝐿) = ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))
34		tsmsxp.h	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐻:𝐴⟶𝐵)
35	34	ffvelcdmda 7036	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝐻‘𝑗) ∈ 𝐵)
36		tsmsxp.p	. . . . . . . . . . . . 13 ⊢ + = (+g‘𝐺)
37		eqid 2736	. . . . . . . . . . . . 13 ⊢ (invg‘𝐺) = (invg‘𝐺)
38		tsmsxp.m	. . . . . . . . . . . . 13 ⊢ − = (-g‘𝐺)
39	7, 36, 37, 38	grpsubval 18961	. . . . . . . . . . . 12 ⊢ (((𝐻‘𝑗) ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → ((𝐻‘𝑗) − 𝑔) = ((𝐻‘𝑗) + ((invg‘𝐺)‘𝑔)))
40	35, 39	sylan 581	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴) ∧ 𝑔 ∈ 𝐵) → ((𝐻‘𝑗) − 𝑔) = ((𝐻‘𝑗) + ((invg‘𝐺)‘𝑔)))
41	40	mpteq2dva 5178	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) = (𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) + ((invg‘𝐺)‘𝑔))))
42		tgpgrp 24043	. . . . . . . . . . . . . 14 ⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ Grp)
43	12, 42	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐺 ∈ Grp)
44	43	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐺 ∈ Grp)
45	7, 37	grpinvcl 18963	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ Grp ∧ 𝑔 ∈ 𝐵) → ((invg‘𝐺)‘𝑔) ∈ 𝐵)
46	44, 45	sylan 581	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴) ∧ 𝑔 ∈ 𝐵) → ((invg‘𝐺)‘𝑔) ∈ 𝐵)
47	7, 37	grpinvf 18962	. . . . . . . . . . . . 13 ⊢ (𝐺 ∈ Grp → (invg‘𝐺):𝐵⟶𝐵)
48	44, 47	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (invg‘𝐺):𝐵⟶𝐵)
49	48	feqmptd 6908	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (invg‘𝐺) = (𝑔 ∈ 𝐵 ↦ ((invg‘𝐺)‘𝑔)))
50		eqidd 2737	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) = (𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)))
51		oveq2 7375	. . . . . . . . . . 11 ⊢ (𝑦 = ((invg‘𝐺)‘𝑔) → ((𝐻‘𝑗) + 𝑦) = ((𝐻‘𝑗) + ((invg‘𝐺)‘𝑔)))
52	46, 49, 50, 51	fmptco 7082	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ((𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) ∘ (invg‘𝐺)) = (𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) + ((invg‘𝐺)‘𝑔))))
53	41, 52	eqtr4d 2774	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) = ((𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) ∘ (invg‘𝐺)))
54	12	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐺 ∈ TopGrp)
55	8, 37	grpinvhmeo 24051	. . . . . . . . . . 11 ⊢ (𝐺 ∈ TopGrp → (invg‘𝐺) ∈ (𝐽Homeo𝐽))
56	54, 55	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (invg‘𝐺) ∈ (𝐽Homeo𝐽))
57		eqid 2736	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) = (𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦))
58	57, 7, 36, 8	tgplacthmeo 24068	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ TopGrp ∧ (𝐻‘𝑗) ∈ 𝐵) → (𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) ∈ (𝐽Homeo𝐽))
59	54, 35, 58	syl2anc 585	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) ∈ (𝐽Homeo𝐽))
60		hmeoco 23737	. . . . . . . . . 10 ⊢ (((invg‘𝐺) ∈ (𝐽Homeo𝐽) ∧ (𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) ∈ (𝐽Homeo𝐽)) → ((𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) ∘ (invg‘𝐺)) ∈ (𝐽Homeo𝐽))
61	56, 59, 60	syl2anc 585	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ((𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) ∘ (invg‘𝐺)) ∈ (𝐽Homeo𝐽))
62	53, 61	eqeltrd 2836	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) ∈ (𝐽Homeo𝐽))
63	27	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐿 ∈ 𝐽)
64		hmeoima 23730	. . . . . . . 8 ⊢ (((𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) ∈ (𝐽Homeo𝐽) ∧ 𝐿 ∈ 𝐽) → ((𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) “ 𝐿) ∈ 𝐽)
65	62, 63, 64	syl2anc 585	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ((𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) “ 𝐿) ∈ 𝐽)
66	33, 65	eqeltrrd 2837	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)) ∈ 𝐽)
67		tsmsxp.z	. . . . . . . . 9 ⊢ 0 = (0g‘𝐺)
68	7, 67, 38	grpsubid1 19001	. . . . . . . 8 ⊢ ((𝐺 ∈ Grp ∧ (𝐻‘𝑗) ∈ 𝐵) → ((𝐻‘𝑗) − 0 ) = (𝐻‘𝑗))
69	44, 35, 68	syl2anc 585	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ((𝐻‘𝑗) − 0 ) = (𝐻‘𝑗))
70		tsmsxp.3	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ 𝐿)
71	70	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 0 ∈ 𝐿)
72		ovex 7400	. . . . . . . 8 ⊢ ((𝐻‘𝑗) − 0 ) ∈ V
73		eqid 2736	. . . . . . . . 9 ⊢ (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)) = (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))
74		oveq2 7375	. . . . . . . . 9 ⊢ (𝑔 = 0 → ((𝐻‘𝑗) − 𝑔) = ((𝐻‘𝑗) − 0 ))
75	73, 74	elrnmpt1s 5914	. . . . . . . 8 ⊢ (( 0 ∈ 𝐿 ∧ ((𝐻‘𝑗) − 0 ) ∈ V) → ((𝐻‘𝑗) − 0 ) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))
76	71, 72, 75	sylancl 587	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ((𝐻‘𝑗) − 0 ) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))
77	69, 76	eqeltrrd 2837	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝐻‘𝑗) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))
78	7, 8, 9, 11, 15, 17, 22, 23, 66, 77	tsmsi 24099	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ∃𝑦 ∈ (𝒫 𝐶 ∩ Fin)∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))
79	6, 78	syldan 592	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐾) → ∃𝑦 ∈ (𝒫 𝐶 ∩ Fin)∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))
80	79	ralrimiva 3129	. . 3 ⊢ (𝜑 → ∀𝑗 ∈ 𝐾 ∃𝑦 ∈ (𝒫 𝐶 ∩ Fin)∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))
81		sseq1 3947	. . . . . 6 ⊢ (𝑦 = (𝑓‘𝑗) → (𝑦 ⊆ 𝑧 ↔ (𝑓‘𝑗) ⊆ 𝑧))
82	81	imbi1d 341	. . . . 5 ⊢ (𝑦 = (𝑓‘𝑗) → ((𝑦 ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) ↔ ((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))))
83	82	ralbidv 3160	. . . 4 ⊢ (𝑦 = (𝑓‘𝑗) → (∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) ↔ ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))))
84	83	ac6sfi 9194	. . 3 ⊢ ((𝐾 ∈ Fin ∧ ∀𝑗 ∈ 𝐾 ∃𝑦 ∈ (𝒫 𝐶 ∩ Fin)∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))) → ∃𝑓(𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗 ∈ 𝐾 ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))))
85	2, 80, 84	syl2anc 585	. 2 ⊢ (𝜑 → ∃𝑓(𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗 ∈ 𝐾 ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))))
86		frn 6675	. . . . . . . . 9 ⊢ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) → ran 𝑓 ⊆ (𝒫 𝐶 ∩ Fin))
87	86	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝑓 ⊆ (𝒫 𝐶 ∩ Fin))
88		inss1 4177	. . . . . . . 8 ⊢ (𝒫 𝐶 ∩ Fin) ⊆ 𝒫 𝐶
89	87, 88	sstrdi 3934	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝑓 ⊆ 𝒫 𝐶)
90		sspwuni 5042	. . . . . . 7 ⊢ (ran 𝑓 ⊆ 𝒫 𝐶 ↔ ∪ ran 𝑓 ⊆ 𝐶)
91	89, 90	sylib 218	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ∪ ran 𝑓 ⊆ 𝐶)
92		tsmsxp.d	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin))
93		elfpw 9264	. . . . . . . . . 10 ⊢ (𝐷 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ↔ (𝐷 ⊆ (𝐴 × 𝐶) ∧ 𝐷 ∈ Fin))
94	93	simplbi 496	. . . . . . . . 9 ⊢ (𝐷 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) → 𝐷 ⊆ (𝐴 × 𝐶))
95		rnss 5894	. . . . . . . . 9 ⊢ (𝐷 ⊆ (𝐴 × 𝐶) → ran 𝐷 ⊆ ran (𝐴 × 𝐶))
96	92, 94, 95	3syl 18	. . . . . . . 8 ⊢ (𝜑 → ran 𝐷 ⊆ ran (𝐴 × 𝐶))
97		rnxpss 6136	. . . . . . . 8 ⊢ ran (𝐴 × 𝐶) ⊆ 𝐶
98	96, 97	sstrdi 3934	. . . . . . 7 ⊢ (𝜑 → ran 𝐷 ⊆ 𝐶)
99	98	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝐷 ⊆ 𝐶)
100	91, 99	unssd 4132	. . . . 5 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∪ ran 𝑓 ∪ ran 𝐷) ⊆ 𝐶)
101	2	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝐾 ∈ Fin)
102		ffn 6668	. . . . . . . . . 10 ⊢ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) → 𝑓 Fn 𝐾)
103	102	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝑓 Fn 𝐾)
104		dffn4 6758	. . . . . . . . 9 ⊢ (𝑓 Fn 𝐾 ↔ 𝑓:𝐾–onto→ran 𝑓)
105	103, 104	sylib 218	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝑓:𝐾–onto→ran 𝑓)
106		fofi 9223	. . . . . . . 8 ⊢ ((𝐾 ∈ Fin ∧ 𝑓:𝐾–onto→ran 𝑓) → ran 𝑓 ∈ Fin)
107	101, 105, 106	syl2anc 585	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝑓 ∈ Fin)
108		inss2 4178	. . . . . . . 8 ⊢ (𝒫 𝐶 ∩ Fin) ⊆ Fin
109	87, 108	sstrdi 3934	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝑓 ⊆ Fin)
110		unifi 9254	. . . . . . 7 ⊢ ((ran 𝑓 ∈ Fin ∧ ran 𝑓 ⊆ Fin) → ∪ ran 𝑓 ∈ Fin)
111	107, 109, 110	syl2anc 585	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ∪ ran 𝑓 ∈ Fin)
112		elinel2 4142	. . . . . . . 8 ⊢ (𝐷 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) → 𝐷 ∈ Fin)
113		rnfi 9250	. . . . . . . 8 ⊢ (𝐷 ∈ Fin → ran 𝐷 ∈ Fin)
114	92, 112, 113	3syl 18	. . . . . . 7 ⊢ (𝜑 → ran 𝐷 ∈ Fin)
115	114	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝐷 ∈ Fin)
116		unfi 9105	. . . . . 6 ⊢ ((∪ ran 𝑓 ∈ Fin ∧ ran 𝐷 ∈ Fin) → (∪ ran 𝑓 ∪ ran 𝐷) ∈ Fin)
117	111, 115, 116	syl2anc 585	. . . . 5 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∪ ran 𝑓 ∪ ran 𝐷) ∈ Fin)
118		elfpw 9264	. . . . 5 ⊢ ((∪ ran 𝑓 ∪ ran 𝐷) ∈ (𝒫 𝐶 ∩ Fin) ↔ ((∪ ran 𝑓 ∪ ran 𝐷) ⊆ 𝐶 ∧ (∪ ran 𝑓 ∪ ran 𝐷) ∈ Fin))
119	100, 117, 118	sylanbrc 584	. . . 4 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∪ ran 𝑓 ∪ ran 𝐷) ∈ (𝒫 𝐶 ∩ Fin))
120	119	adantrr 718	. . 3 ⊢ ((𝜑 ∧ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗 ∈ 𝐾 ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))) → (∪ ran 𝑓 ∪ ran 𝐷) ∈ (𝒫 𝐶 ∩ Fin))
121		ssun2 4119	. . . 4 ⊢ ran 𝐷 ⊆ (∪ ran 𝑓 ∪ ran 𝐷)
122	121	a1i 11	. . 3 ⊢ ((𝜑 ∧ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗 ∈ 𝐾 ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))) → ran 𝐷 ⊆ (∪ ran 𝑓 ∪ ran 𝐷))
123	119	adantlr 716	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∪ ran 𝑓 ∪ ran 𝐷) ∈ (𝒫 𝐶 ∩ Fin))
124		fvssunirn 6871	. . . . . . . . . . . . . 14 ⊢ (𝑓‘𝑗) ⊆ ∪ ran 𝑓
125		ssun1 4118	. . . . . . . . . . . . . 14 ⊢ ∪ ran 𝑓 ⊆ (∪ ran 𝑓 ∪ ran 𝐷)
126	124, 125	sstri 3931	. . . . . . . . . . . . 13 ⊢ (𝑓‘𝑗) ⊆ (∪ ran 𝑓 ∪ ran 𝐷)
127		id 22	. . . . . . . . . . . . 13 ⊢ (𝑧 = (∪ ran 𝑓 ∪ ran 𝐷) → 𝑧 = (∪ ran 𝑓 ∪ ran 𝐷))
128	126, 127	sseqtrrid 3965	. . . . . . . . . . . 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 5939	. . . . . . . . . . . . 13 ⊢ (𝑧 = (∪ ran 𝑓 ∪ ran 𝐷) → ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧) = ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran 𝑓 ∪ ran 𝐷)))
132	131	oveq2d 7383	. . . . . . . . . . . 12 ⊢ (𝑧 = (∪ ran 𝑓 ∪ ran 𝐷) → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) = (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran 𝑓 ∪ ran 𝐷))))
133	132	eleq1d 2821	. . . . . . . . . . 11 ⊢ (𝑧 = (∪ ran 𝑓 ∪ ran 𝐷) → ((𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)) ↔ (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran 𝑓 ∪ ran 𝐷))) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))
134	130, 133	bitrd 279	. . . . . . . . . 10 ⊢ (𝑧 = (∪ ran 𝑓 ∪ ran 𝐷) → (((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) ↔ (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran 𝑓 ∪ ran 𝐷))) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))
135	134	rspcv 3560	. . . . . . . . 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 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝐺 ∈ CMnd)
138		cmnmnd 19772	. . . . . . . . . . . . 13 ⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd)
139	137, 138	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝐺 ∈ Mnd)
140		simplr 769	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝑗 ∈ 𝐾)
141	117	adantlr 716	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∪ ran 𝑓 ∪ ran 𝐷) ∈ Fin)
142	100	adantlr 716	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∪ ran 𝑓 ∪ ran 𝐷) ⊆ 𝐶)
143	142	sselda 3921	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷)) → 𝑘 ∈ 𝐶)
144	18	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐾) → 𝐹:(𝐴 × 𝐶)⟶𝐵)
145	144, 6	jca 511	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐾) → (𝐹:(𝐴 × 𝐶)⟶𝐵 ∧ 𝑗 ∈ 𝐴))
146	19	3expa 1119	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹:(𝐴 × 𝐶)⟶𝐵 ∧ 𝑗 ∈ 𝐴) ∧ 𝑘 ∈ 𝐶) → (𝑗𝐹𝑘) ∈ 𝐵)
147	145, 146	sylan 581	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑘 ∈ 𝐶) → (𝑗𝐹𝑘) ∈ 𝐵)
148	147	adantlr 716	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ 𝐶) → (𝑗𝐹𝑘) ∈ 𝐵)
149	143, 148	syldan 592	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷)) → (𝑗𝐹𝑘) ∈ 𝐵)
150	149	fmpttd 7067	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘)):(∪ ran 𝑓 ∪ ran 𝐷)⟶𝐵)
151		eqid 2736	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘)) = (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))
152		ovexd 7402	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷)) → (𝑗𝐹𝑘) ∈ V)
153	67	fvexi 6854	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ V
154	153	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 0 ∈ V)
155	151, 141, 152, 154	fsuppmptdm 9289	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘)) finSupp 0 )
156	7, 67, 137, 141, 150, 155	gsumcl 19890	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))) ∈ 𝐵)
157		velsn 4583	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ {𝑗} ↔ 𝑦 = 𝑗)
158		ovres 7533	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ {𝑗} ∧ 𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷)) → (𝑦(𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))𝑘) = (𝑦𝐹𝑘))
159	157, 158	sylanbr 583	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 = 𝑗 ∧ 𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷)) → (𝑦(𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))𝑘) = (𝑦𝐹𝑘))
160		oveq1 7374	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑗 → (𝑦𝐹𝑘) = (𝑗𝐹𝑘))
161	160	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 = 𝑗 ∧ 𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷)) → (𝑦𝐹𝑘) = (𝑗𝐹𝑘))
162	159, 161	eqtrd 2771	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 = 𝑗 ∧ 𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷)) → (𝑦(𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))𝑘) = (𝑗𝐹𝑘))
163	162	mpteq2dva 5178	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑗 → (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑦(𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))𝑘)) = (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘)))
164	163	oveq2d 7383	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑗 → (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑦(𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))𝑘))) = (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))))
165	7, 164	gsumsn 19929	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ Mnd ∧ 𝑗 ∈ 𝐾 ∧ (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))) ∈ 𝐵) → (𝐺 Σg (𝑦 ∈ {𝑗} ↦ (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑦(𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))𝑘))))) = (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))))
166	139, 140, 156, 165	syl3anc 1374	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐺 Σg (𝑦 ∈ {𝑗} ↦ (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑦(𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))𝑘))))) = (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))))
167		snfi 8990	. . . . . . . . . . . . 13 ⊢ {𝑗} ∈ Fin
168	167	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → {𝑗} ∈ Fin)
169	18	ad2antrr 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝐹:(𝐴 × 𝐶)⟶𝐵)
170	6	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝑗 ∈ 𝐴)
171	170	snssd 4730	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → {𝑗} ⊆ 𝐴)
172		xpss12 5646	. . . . . . . . . . . . . 14 ⊢ (({𝑗} ⊆ 𝐴 ∧ (∪ ran 𝑓 ∪ ran 𝐷) ⊆ 𝐶) → ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)) ⊆ (𝐴 × 𝐶))
173	171, 142, 172	syl2anc 585	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)) ⊆ (𝐴 × 𝐶))
174	169, 173	fssresd 6707	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))):({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))⟶𝐵)
175		xpfi 9230	. . . . . . . . . . . . . 14 ⊢ (({𝑗} ∈ Fin ∧ (∪ ran 𝑓 ∪ ran 𝐷) ∈ Fin) → ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)) ∈ Fin)
176	167, 141, 175	sylancr 588	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)) ∈ Fin)
177	174, 176, 154	fdmfifsupp 9288	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))) finSupp 0 )
178	7, 67, 137, 168, 141, 174, 177	gsumxp 19951	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))) = (𝐺 Σg (𝑦 ∈ {𝑗} ↦ (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑦(𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))𝑘))))))
179	142	resmptd 6005	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran 𝑓 ∪ ran 𝐷)) = (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘)))
180	179	oveq2d 7383	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran 𝑓 ∪ ran 𝐷))) = (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))))
181	166, 178, 180	3eqtr4rd 2782	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran 𝑓 ∪ ran 𝐷))) = (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))))
182	181	eleq1d 2821	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ((𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran 𝑓 ∪ ran 𝐷))) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)) ↔ (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))
183		ovex 7400	. . . . . . . . . . 11 ⊢ ((𝐻‘𝑗) − 𝑔) ∈ V
184	73, 183	elrnmpti 5917	. . . . . . . . . 10 ⊢ ((𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)) ↔ ∃𝑔 ∈ 𝐿 (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))) = ((𝐻‘𝑗) − 𝑔))
185		isabl 19759	. . . . . . . . . . . . . . . 16 ⊢ (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd))
186	43, 10, 185	sylanbrc 584	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐺 ∈ Abel)
187	186	ad3antrrr 731	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔 ∈ 𝐿) → 𝐺 ∈ Abel)
188	6, 35	syldan 592	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐾) → (𝐻‘𝑗) ∈ 𝐵)
189	188	ad2antrr 727	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔 ∈ 𝐿) → (𝐻‘𝑗) ∈ 𝐵)
190	29	ad2antrr 727	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝐿 ⊆ 𝐵)
191	190	sselda 3921	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔 ∈ 𝐿) → 𝑔 ∈ 𝐵)
192	7, 38, 187, 189, 191	ablnncan 19795	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔 ∈ 𝐿) → ((𝐻‘𝑗) − ((𝐻‘𝑗) − 𝑔)) = 𝑔)
193		simpr 484	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔 ∈ 𝐿) → 𝑔 ∈ 𝐿)
194	192, 193	eqeltrd 2836	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔 ∈ 𝐿) → ((𝐻‘𝑗) − ((𝐻‘𝑗) − 𝑔)) ∈ 𝐿)
195		oveq2 7375	. . . . . . . . . . . . 13 ⊢ ((𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))) = ((𝐻‘𝑗) − 𝑔) → ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) = ((𝐻‘𝑗) − ((𝐻‘𝑗) − 𝑔)))
196	195	eleq1d 2821	. . . . . . . . . . . 12 ⊢ ((𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))) = ((𝐻‘𝑗) − 𝑔) → (((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿 ↔ ((𝐻‘𝑗) − ((𝐻‘𝑗) − 𝑔)) ∈ 𝐿))
197	194, 196	syl5ibrcom 247	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔 ∈ 𝐿) → ((𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))) = ((𝐻‘𝑗) − 𝑔) → ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
198	197	rexlimdva 3138	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∃𝑔 ∈ 𝐿 (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))) = ((𝐻‘𝑗) − 𝑔) → ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
199	184, 198	biimtrid 242	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ((𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)) → ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
200	182, 199	sylbid 240	. . . . . . . 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 653	. . . . . 6 ⊢ (((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑗 ∈ 𝐾) → (∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) → ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
203	202	ralimdva 3149	. . . . 5 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∀𝑗 ∈ 𝐾 ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) → ∀𝑗 ∈ 𝐾 ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
204	203	impr 454	. . . 4 ⊢ ((𝜑 ∧ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗 ∈ 𝐾 ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))) → ∀𝑗 ∈ 𝐾 ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿)
205		fveq2 6840	. . . . . . 7 ⊢ (𝑗 = 𝑥 → (𝐻‘𝑗) = (𝐻‘𝑥))
206		sneq 4577	. . . . . . . . . 10 ⊢ (𝑗 = 𝑥 → {𝑗} = {𝑥})
207	206	xpeq1d 5660	. . . . . . . . 9 ⊢ (𝑗 = 𝑥 → ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)) = ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷)))
208	207	reseq2d 5944	. . . . . . . 8 ⊢ (𝑗 = 𝑥 → (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))) = (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷))))
209	208	oveq2d 7383	. . . . . . 7 ⊢ (𝑗 = 𝑥 → (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))) = (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷)))))
210	205, 209	oveq12d 7385	. . . . . 6 ⊢ (𝑗 = 𝑥 → ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) = ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷))))))
211	210	eleq1d 2821	. . . . 5 ⊢ (𝑗 = 𝑥 → (((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿 ↔ ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
212	211	cbvralvw 3215	. . . 4 ⊢ (∀𝑗 ∈ 𝐾 ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿 ↔ ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿)
213	204, 212	sylib 218	. . 3 ⊢ ((𝜑 ∧ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗 ∈ 𝐾 ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))) → ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿)
214		sseq2 3948	. . . . 5 ⊢ (𝑛 = (∪ ran 𝑓 ∪ ran 𝐷) → (ran 𝐷 ⊆ 𝑛 ↔ ran 𝐷 ⊆ (∪ ran 𝑓 ∪ ran 𝐷)))
215		xpeq2 5652	. . . . . . . . . 10 ⊢ (𝑛 = (∪ ran 𝑓 ∪ ran 𝐷) → ({𝑥} × 𝑛) = ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷)))
216	215	reseq2d 5944	. . . . . . . . 9 ⊢ (𝑛 = (∪ ran 𝑓 ∪ ran 𝐷) → (𝐹 ↾ ({𝑥} × 𝑛)) = (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷))))
217	216	oveq2d 7383	. . . . . . . 8 ⊢ (𝑛 = (∪ ran 𝑓 ∪ ran 𝐷) → (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛))) = (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷)))))
218	217	oveq2d 7383	. . . . . . 7 ⊢ (𝑛 = (∪ ran 𝑓 ∪ ran 𝐷) → ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) = ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷))))))
219	218	eleq1d 2821	. . . . . 6 ⊢ (𝑛 = (∪ ran 𝑓 ∪ ran 𝐷) → (((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿 ↔ ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
220	219	ralbidv 3160	. . . . 5 ⊢ (𝑛 = (∪ ran 𝑓 ∪ ran 𝐷) → (∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿 ↔ ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
221	214, 220	anbi12d 633	. . . 4 ⊢ (𝑛 = (∪ ran 𝑓 ∪ ran 𝐷) → ((ran 𝐷 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿) ↔ (ran 𝐷 ⊆ (∪ ran 𝑓 ∪ ran 𝐷) ∧ ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿)))
222	221	rspcev 3564	. . 3 ⊢ (((∪ ran 𝑓 ∪ ran 𝐷) ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝐷 ⊆ (∪ ran 𝑓 ∪ ran 𝐷) ∧ ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿)) → ∃𝑛 ∈ (𝒫 𝐶 ∩ Fin)(ran 𝐷 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿))
223	120, 122, 213, 222	syl12anc 837	. 2 ⊢ ((𝜑 ∧ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗 ∈ 𝐾 ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))) → ∃𝑛 ∈ (𝒫 𝐶 ∩ Fin)(ran 𝐷 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿))
224	85, 223	exlimddv 1937	1 ⊢ (𝜑 → ∃𝑛 ∈ (𝒫 𝐶 ∩ Fin)(ran 𝐷 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542  ∃wex 1781   ∈ wcel 2114  ∀wral 3051  ∃wrex 3061  Vcvv 3429   ∪ cun 3887   ∩ cin 3888   ⊆ wss 3889  𝒫 cpw 4541  {csn 4567  ∪ cuni 4850   ↦ cmpt 5166   × cxp 5629  dom cdm 5631  ran crn 5632   ↾ cres 5633   “ cima 5634   ∘ ccom 5635   Fn wfn 6493  ⟶wf 6494  –onto→wfo 6496  ‘cfv 6498  (class class class)co 7367  Fincfn 8893  Basecbs 17179  +_gcplusg 17220  TopOpenctopn 17384  0_gc0g 17402   Σ_g cgsu 17403  Mndcmnd 18702  Grpcgrp 18909  inv_gcminusg 18910  -_gcsg 18911  CMndccmn 19755  Abelcabl 19756  TopOnctopon 22875  TopSpctps 22897  Homeochmeo 23718  TopGrpctgp 24036   tsums ctsu 24091

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689  ax-cnex 11094  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3062  df-rmo 3342  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-int 4890  df-iun 4935  df-iin 4936  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-se 5585  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6265  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-isom 6507  df-riota 7324  df-ov 7370  df-oprab 7371  df-mpo 7372  df-of 7631  df-om 7818  df-1st 7942  df-2nd 7943  df-supp 8111  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-1o 8405  df-2o 8406  df-er 8643  df-map 8775  df-en 8894  df-dom 8895  df-sdom 8896  df-fin 8897  df-fsupp 9275  df-oi 9425  df-card 9863  df-pnf 11181  df-mnf 11182  df-xr 11183  df-ltxr 11184  df-le 11185  df-sub 11379  df-neg 11380  df-nn 12175  df-2 12244  df-n0 12438  df-z 12525  df-uz 12789  df-fz 13462  df-fzo 13609  df-seq 13964  df-hash 14293  df-sets 17134  df-slot 17152  df-ndx 17164  df-base 17180  df-ress 17201  df-plusg 17233  df-0g 17404  df-gsum 17405  df-topgen 17406  df-mre 17548  df-mrc 17549  df-acs 17551  df-plusf 18607  df-mgm 18608  df-sgrp 18687  df-mnd 18703  df-submnd 18752  df-grp 18912  df-minusg 18913  df-sbg 18914  df-mulg 19044  df-cntz 19292  df-cmn 19757  df-abl 19758  df-fbas 21349  df-fg 21350  df-top 22859  df-topon 22876  df-topsp 22898  df-bases 22911  df-ntr 22985  df-nei 23063  df-cn 23192  df-cnp 23193  df-tx 23527  df-hmeo 23720  df-fil 23811  df-fm 23903  df-flim 23904  df-flf 23905  df-tmd 24037  df-tgp 24038  df-tsms 24092

This theorem is referenced by:  tsmsxp  24120