Theorem tsmsxplem1 22454

Description: Lemma for tsmsxp 22456. (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 4060	. . 3 ⊢ (𝜑 → 𝐾 ∈ Fin)
3		elfpw 8613	. . . . . . . 8 ⊢ (𝐾 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝐾 ⊆ 𝐴 ∧ 𝐾 ∈ Fin))
4	3	simplbi 490	. . . . . . 7 ⊢ (𝐾 ∈ (𝒫 𝐴 ∩ Fin) → 𝐾 ⊆ 𝐴)
5	1, 4	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐾 ⊆ 𝐴)
6	5	sselda 3854	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐾) → 𝑗 ∈ 𝐴)
7		tsmsxp.b	. . . . . 6 ⊢ 𝐵 = (Base‘𝐺)
8		tsmsxp.j	. . . . . 6 ⊢ 𝐽 = (TopOpen‘𝐺)
9		eqid 2772	. . . . . 6 ⊢ (𝒫 𝐶 ∩ Fin) = (𝒫 𝐶 ∩ Fin)
10		tsmsxp.g	. . . . . . 7 ⊢ (𝜑 → 𝐺 ∈ CMnd)
11	10	adantr 473	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐺 ∈ CMnd)
12		tsmsxp.2	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ TopGrp)
13		tgptps 22382	. . . . . . . 8 ⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ TopSp)
14	12, 13	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐺 ∈ TopSp)
15	14	adantr 473	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐺 ∈ TopSp)
16		tsmsxp.c	. . . . . . 7 ⊢ (𝜑 → 𝐶 ∈ 𝑊)
17	16	adantr 473	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐶 ∈ 𝑊)
18		tsmsxp.f	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:(𝐴 × 𝐶)⟶𝐵)
19		fovrn 7128	. . . . . . . . 9 ⊢ ((𝐹:(𝐴 × 𝐶)⟶𝐵 ∧ 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶) → (𝑗𝐹𝑘) ∈ 𝐵)
20	18, 19	syl3an1 1143	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶) → (𝑗𝐹𝑘) ∈ 𝐵)
21	20	3expa 1098	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴) ∧ 𝑘 ∈ 𝐶) → (𝑗𝐹𝑘) ∈ 𝐵)
22	21	fmpttd 6696	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)):𝐶⟶𝐵)
23		tsmsxp.1	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝐻‘𝑗) ∈ (𝐺 tsums (𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘))))
24		df-ima 5413	. . . . . . . 8 ⊢ ((𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) “ 𝐿) = ran ((𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) ↾ 𝐿)
25	8, 7	tgptopon 22384	. . . . . . . . . . . . 13 ⊢ (𝐺 ∈ TopGrp → 𝐽 ∈ (TopOn‘𝐵))
26	12, 25	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝐵))
27		tsmsxp.l	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐿 ∈ 𝐽)
28		toponss 21229	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ (TopOn‘𝐵) ∧ 𝐿 ∈ 𝐽) → 𝐿 ⊆ 𝐵)
29	26, 27, 28	syl2anc 576	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐿 ⊆ 𝐵)
30	29	adantr 473	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐿 ⊆ 𝐵)
31	30	resmptd 5747	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ((𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) ↾ 𝐿) = (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))
32	31	rneqd 5644	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ran ((𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) ↾ 𝐿) = ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))
33	24, 32	syl5eq 2820	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ((𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) “ 𝐿) = ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))
34		tsmsxp.h	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐻:𝐴⟶𝐵)
35	34	ffvelrnda 6670	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝐻‘𝑗) ∈ 𝐵)
36		tsmsxp.p	. . . . . . . . . . . . 13 ⊢ + = (+g‘𝐺)
37		eqid 2772	. . . . . . . . . . . . 13 ⊢ (invg‘𝐺) = (invg‘𝐺)
38		tsmsxp.m	. . . . . . . . . . . . 13 ⊢ − = (-g‘𝐺)
39	7, 36, 37, 38	grpsubval 17926	. . . . . . . . . . . 12 ⊢ (((𝐻‘𝑗) ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → ((𝐻‘𝑗) − 𝑔) = ((𝐻‘𝑗) + ((invg‘𝐺)‘𝑔)))
40	35, 39	sylan 572	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴) ∧ 𝑔 ∈ 𝐵) → ((𝐻‘𝑗) − 𝑔) = ((𝐻‘𝑗) + ((invg‘𝐺)‘𝑔)))
41	40	mpteq2dva 5016	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) = (𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) + ((invg‘𝐺)‘𝑔))))
42		tgpgrp 22380	. . . . . . . . . . . . . 14 ⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ Grp)
43	12, 42	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐺 ∈ Grp)
44	43	adantr 473	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐺 ∈ Grp)
45	7, 37	grpinvcl 17928	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ Grp ∧ 𝑔 ∈ 𝐵) → ((invg‘𝐺)‘𝑔) ∈ 𝐵)
46	44, 45	sylan 572	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴) ∧ 𝑔 ∈ 𝐵) → ((invg‘𝐺)‘𝑔) ∈ 𝐵)
47	7, 37	grpinvf 17927	. . . . . . . . . . . . 13 ⊢ (𝐺 ∈ Grp → (invg‘𝐺):𝐵⟶𝐵)
48	44, 47	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (invg‘𝐺):𝐵⟶𝐵)
49	48	feqmptd 6556	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (invg‘𝐺) = (𝑔 ∈ 𝐵 ↦ ((invg‘𝐺)‘𝑔)))
50		eqidd 2773	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) = (𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)))
51		oveq2 6978	. . . . . . . . . . 11 ⊢ (𝑦 = ((invg‘𝐺)‘𝑔) → ((𝐻‘𝑗) + 𝑦) = ((𝐻‘𝑗) + ((invg‘𝐺)‘𝑔)))
52	46, 49, 50, 51	fmptco 6708	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ((𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) ∘ (invg‘𝐺)) = (𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) + ((invg‘𝐺)‘𝑔))))
53	41, 52	eqtr4d 2811	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) = ((𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) ∘ (invg‘𝐺)))
54	12	adantr 473	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐺 ∈ TopGrp)
55	8, 37	grpinvhmeo 22388	. . . . . . . . . . 11 ⊢ (𝐺 ∈ TopGrp → (invg‘𝐺) ∈ (𝐽Homeo𝐽))
56	54, 55	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (invg‘𝐺) ∈ (𝐽Homeo𝐽))
57		eqid 2772	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) = (𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦))
58	57, 7, 36, 8	tgplacthmeo 22405	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ TopGrp ∧ (𝐻‘𝑗) ∈ 𝐵) → (𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) ∈ (𝐽Homeo𝐽))
59	54, 35, 58	syl2anc 576	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) ∈ (𝐽Homeo𝐽))
60		hmeoco 22074	. . . . . . . . . 10 ⊢ (((invg‘𝐺) ∈ (𝐽Homeo𝐽) ∧ (𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) ∈ (𝐽Homeo𝐽)) → ((𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) ∘ (invg‘𝐺)) ∈ (𝐽Homeo𝐽))
61	56, 59, 60	syl2anc 576	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ((𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) ∘ (invg‘𝐺)) ∈ (𝐽Homeo𝐽))
62	53, 61	eqeltrd 2860	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) ∈ (𝐽Homeo𝐽))
63	27	adantr 473	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐿 ∈ 𝐽)
64		hmeoima 22067	. . . . . . . 8 ⊢ (((𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) ∈ (𝐽Homeo𝐽) ∧ 𝐿 ∈ 𝐽) → ((𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) “ 𝐿) ∈ 𝐽)
65	62, 63, 64	syl2anc 576	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ((𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) “ 𝐿) ∈ 𝐽)
66	33, 65	eqeltrrd 2861	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)) ∈ 𝐽)
67		tsmsxp.z	. . . . . . . . 9 ⊢ 0 = (0g‘𝐺)
68	7, 67, 38	grpsubid1 17961	. . . . . . . 8 ⊢ ((𝐺 ∈ Grp ∧ (𝐻‘𝑗) ∈ 𝐵) → ((𝐻‘𝑗) − 0 ) = (𝐻‘𝑗))
69	44, 35, 68	syl2anc 576	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ((𝐻‘𝑗) − 0 ) = (𝐻‘𝑗))
70		tsmsxp.3	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ 𝐿)
71	70	adantr 473	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 0 ∈ 𝐿)
72		ovex 7002	. . . . . . . 8 ⊢ ((𝐻‘𝑗) − 0 ) ∈ V
73		eqid 2772	. . . . . . . . 9 ⊢ (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)) = (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))
74		oveq2 6978	. . . . . . . . 9 ⊢ (𝑔 = 0 → ((𝐻‘𝑗) − 𝑔) = ((𝐻‘𝑗) − 0 ))
75	73, 74	elrnmpt1s 5665	. . . . . . . 8 ⊢ (( 0 ∈ 𝐿 ∧ ((𝐻‘𝑗) − 0 ) ∈ V) → ((𝐻‘𝑗) − 0 ) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))
76	71, 72, 75	sylancl 577	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ((𝐻‘𝑗) − 0 ) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))
77	69, 76	eqeltrrd 2861	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝐻‘𝑗) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))
78	7, 8, 9, 11, 15, 17, 22, 23, 66, 77	tsmsi 22435	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ∃𝑦 ∈ (𝒫 𝐶 ∩ Fin)∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))
79	6, 78	syldan 582	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐾) → ∃𝑦 ∈ (𝒫 𝐶 ∩ Fin)∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))
80	79	ralrimiva 3126	. . 3 ⊢ (𝜑 → ∀𝑗 ∈ 𝐾 ∃𝑦 ∈ (𝒫 𝐶 ∩ Fin)∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))
81		sseq1 3878	. . . . . 6 ⊢ (𝑦 = (𝑓‘𝑗) → (𝑦 ⊆ 𝑧 ↔ (𝑓‘𝑗) ⊆ 𝑧))
82	81	imbi1d 334	. . . . 5 ⊢ (𝑦 = (𝑓‘𝑗) → ((𝑦 ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) ↔ ((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))))
83	82	ralbidv 3141	. . . 4 ⊢ (𝑦 = (𝑓‘𝑗) → (∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) ↔ ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))))
84	83	ac6sfi 8549	. . 3 ⊢ ((𝐾 ∈ Fin ∧ ∀𝑗 ∈ 𝐾 ∃𝑦 ∈ (𝒫 𝐶 ∩ Fin)∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))) → ∃𝑓(𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗 ∈ 𝐾 ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))))
85	2, 80, 84	syl2anc 576	. 2 ⊢ (𝜑 → ∃𝑓(𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗 ∈ 𝐾 ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))))
86		frn 6344	. . . . . . . . 9 ⊢ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) → ran 𝑓 ⊆ (𝒫 𝐶 ∩ Fin))
87	86	adantl 474	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝑓 ⊆ (𝒫 𝐶 ∩ Fin))
88		inss1 4087	. . . . . . . 8 ⊢ (𝒫 𝐶 ∩ Fin) ⊆ 𝒫 𝐶
89	87, 88	syl6ss 3866	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝑓 ⊆ 𝒫 𝐶)
90		sspwuni 4882	. . . . . . 7 ⊢ (ran 𝑓 ⊆ 𝒫 𝐶 ↔ ∪ ran 𝑓 ⊆ 𝐶)
91	89, 90	sylib 210	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ∪ ran 𝑓 ⊆ 𝐶)
92		tsmsxp.d	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin))
93		elfpw 8613	. . . . . . . . . 10 ⊢ (𝐷 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ↔ (𝐷 ⊆ (𝐴 × 𝐶) ∧ 𝐷 ∈ Fin))
94	93	simplbi 490	. . . . . . . . 9 ⊢ (𝐷 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) → 𝐷 ⊆ (𝐴 × 𝐶))
95		rnss 5645	. . . . . . . . 9 ⊢ (𝐷 ⊆ (𝐴 × 𝐶) → ran 𝐷 ⊆ ran (𝐴 × 𝐶))
96	92, 94, 95	3syl 18	. . . . . . . 8 ⊢ (𝜑 → ran 𝐷 ⊆ ran (𝐴 × 𝐶))
97		rnxpss 5863	. . . . . . . 8 ⊢ ran (𝐴 × 𝐶) ⊆ 𝐶
98	96, 97	syl6ss 3866	. . . . . . 7 ⊢ (𝜑 → ran 𝐷 ⊆ 𝐶)
99	98	adantr 473	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝐷 ⊆ 𝐶)
100	91, 99	unssd 4046	. . . . 5 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∪ ran 𝑓 ∪ ran 𝐷) ⊆ 𝐶)
101	2	adantr 473	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝐾 ∈ Fin)
102		ffn 6338	. . . . . . . . . 10 ⊢ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) → 𝑓 Fn 𝐾)
103	102	adantl 474	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝑓 Fn 𝐾)
104		dffn4 6419	. . . . . . . . 9 ⊢ (𝑓 Fn 𝐾 ↔ 𝑓:𝐾–onto→ran 𝑓)
105	103, 104	sylib 210	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝑓:𝐾–onto→ran 𝑓)
106		fofi 8597	. . . . . . . 8 ⊢ ((𝐾 ∈ Fin ∧ 𝑓:𝐾–onto→ran 𝑓) → ran 𝑓 ∈ Fin)
107	101, 105, 106	syl2anc 576	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝑓 ∈ Fin)
108		inss2 4088	. . . . . . . 8 ⊢ (𝒫 𝐶 ∩ Fin) ⊆ Fin
109	87, 108	syl6ss 3866	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝑓 ⊆ Fin)
110		unifi 8600	. . . . . . 7 ⊢ ((ran 𝑓 ∈ Fin ∧ ran 𝑓 ⊆ Fin) → ∪ ran 𝑓 ∈ Fin)
111	107, 109, 110	syl2anc 576	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ∪ ran 𝑓 ∈ Fin)
112		elinel2 4057	. . . . . . . 8 ⊢ (𝐷 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) → 𝐷 ∈ Fin)
113		rnfi 8594	. . . . . . . 8 ⊢ (𝐷 ∈ Fin → ran 𝐷 ∈ Fin)
114	92, 112, 113	3syl 18	. . . . . . 7 ⊢ (𝜑 → ran 𝐷 ∈ Fin)
115	114	adantr 473	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝐷 ∈ Fin)
116		unfi 8572	. . . . . 6 ⊢ ((∪ ran 𝑓 ∈ Fin ∧ ran 𝐷 ∈ Fin) → (∪ ran 𝑓 ∪ ran 𝐷) ∈ Fin)
117	111, 115, 116	syl2anc 576	. . . . 5 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∪ ran 𝑓 ∪ ran 𝐷) ∈ Fin)
118		elfpw 8613	. . . . 5 ⊢ ((∪ ran 𝑓 ∪ ran 𝐷) ∈ (𝒫 𝐶 ∩ Fin) ↔ ((∪ ran 𝑓 ∪ ran 𝐷) ⊆ 𝐶 ∧ (∪ ran 𝑓 ∪ ran 𝐷) ∈ Fin))
119	100, 117, 118	sylanbrc 575	. . . 4 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∪ ran 𝑓 ∪ ran 𝐷) ∈ (𝒫 𝐶 ∩ Fin))
120	119	adantrr 704	. . 3 ⊢ ((𝜑 ∧ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗 ∈ 𝐾 ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))) → (∪ ran 𝑓 ∪ ran 𝐷) ∈ (𝒫 𝐶 ∩ Fin))
121		ssun2 4034	. . . 4 ⊢ ran 𝐷 ⊆ (∪ ran 𝑓 ∪ ran 𝐷)
122	121	a1i 11	. . 3 ⊢ ((𝜑 ∧ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗 ∈ 𝐾 ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))) → ran 𝐷 ⊆ (∪ ran 𝑓 ∪ ran 𝐷))
123	119	adantlr 702	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∪ ran 𝑓 ∪ ran 𝐷) ∈ (𝒫 𝐶 ∩ Fin))
124		fvssunirn 6522	. . . . . . . . . . . . . 14 ⊢ (𝑓‘𝑗) ⊆ ∪ ran 𝑓
125		ssun1 4033	. . . . . . . . . . . . . 14 ⊢ ∪ ran 𝑓 ⊆ (∪ ran 𝑓 ∪ ran 𝐷)
126	124, 125	sstri 3863	. . . . . . . . . . . . 13 ⊢ (𝑓‘𝑗) ⊆ (∪ ran 𝑓 ∪ ran 𝐷)
127		id 22	. . . . . . . . . . . . 13 ⊢ (𝑧 = (∪ ran 𝑓 ∪ ran 𝐷) → 𝑧 = (∪ ran 𝑓 ∪ ran 𝐷))
128	126, 127	syl5sseqr 3906	. . . . . . . . . . . 12 ⊢ (𝑧 = (∪ ran 𝑓 ∪ ran 𝐷) → (𝑓‘𝑗) ⊆ 𝑧)
129		pm5.5 354	. . . . . . . . . . . 12 ⊢ ((𝑓‘𝑗) ⊆ 𝑧 → (((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) ↔ (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))
130	128, 129	syl 17	. . . . . . . . . . 11 ⊢ (𝑧 = (∪ ran 𝑓 ∪ ran 𝐷) → (((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) ↔ (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))
131		reseq2 5683	. . . . . . . . . . . . 13 ⊢ (𝑧 = (∪ ran 𝑓 ∪ ran 𝐷) → ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧) = ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran 𝑓 ∪ ran 𝐷)))
132	131	oveq2d 6986	. . . . . . . . . . . 12 ⊢ (𝑧 = (∪ ran 𝑓 ∪ ran 𝐷) → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) = (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran 𝑓 ∪ ran 𝐷))))
133	132	eleq1d 2844	. . . . . . . . . . 11 ⊢ (𝑧 = (∪ ran 𝑓 ∪ ran 𝐷) → ((𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)) ↔ (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran 𝑓 ∪ ran 𝐷))) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))
134	130, 133	bitrd 271	. . . . . . . . . 10 ⊢ (𝑧 = (∪ ran 𝑓 ∪ ran 𝐷) → (((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) ↔ (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran 𝑓 ∪ ran 𝐷))) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))
135	134	rspcv 3525	. . . . . . . . 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 713	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝐺 ∈ CMnd)
138		cmnmnd 18671	. . . . . . . . . . . . 13 ⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd)
139	137, 138	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝐺 ∈ Mnd)
140		simplr 756	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝑗 ∈ 𝐾)
141	117	adantlr 702	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∪ ran 𝑓 ∪ ran 𝐷) ∈ Fin)
142	100	adantlr 702	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∪ ran 𝑓 ∪ ran 𝐷) ⊆ 𝐶)
143	142	sselda 3854	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷)) → 𝑘 ∈ 𝐶)
144	18	adantr 473	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐾) → 𝐹:(𝐴 × 𝐶)⟶𝐵)
145	144, 6	jca 504	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐾) → (𝐹:(𝐴 × 𝐶)⟶𝐵 ∧ 𝑗 ∈ 𝐴))
146	19	3expa 1098	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹:(𝐴 × 𝐶)⟶𝐵 ∧ 𝑗 ∈ 𝐴) ∧ 𝑘 ∈ 𝐶) → (𝑗𝐹𝑘) ∈ 𝐵)
147	145, 146	sylan 572	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑘 ∈ 𝐶) → (𝑗𝐹𝑘) ∈ 𝐵)
148	147	adantlr 702	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ 𝐶) → (𝑗𝐹𝑘) ∈ 𝐵)
149	143, 148	syldan 582	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷)) → (𝑗𝐹𝑘) ∈ 𝐵)
150	149	fmpttd 6696	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘)):(∪ ran 𝑓 ∪ ran 𝐷)⟶𝐵)
151		eqid 2772	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘)) = (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))
152		ovexd 7004	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷)) → (𝑗𝐹𝑘) ∈ V)
153	67	fvexi 6507	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ V
154	153	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 0 ∈ V)
155	151, 141, 152, 154	fsuppmptdm 8631	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘)) finSupp 0 )
156	7, 67, 137, 141, 150, 155	gsumcl 18779	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))) ∈ 𝐵)
157		velsn 4451	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ {𝑗} ↔ 𝑦 = 𝑗)
158		ovres 7124	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ {𝑗} ∧ 𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷)) → (𝑦(𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))𝑘) = (𝑦𝐹𝑘))
159	157, 158	sylanbr 574	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 = 𝑗 ∧ 𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷)) → (𝑦(𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))𝑘) = (𝑦𝐹𝑘))
160		oveq1 6977	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑗 → (𝑦𝐹𝑘) = (𝑗𝐹𝑘))
161	160	adantr 473	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 = 𝑗 ∧ 𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷)) → (𝑦𝐹𝑘) = (𝑗𝐹𝑘))
162	159, 161	eqtrd 2808	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 = 𝑗 ∧ 𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷)) → (𝑦(𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))𝑘) = (𝑗𝐹𝑘))
163	162	mpteq2dva 5016	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑗 → (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑦(𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))𝑘)) = (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘)))
164	163	oveq2d 6986	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑗 → (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑦(𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))𝑘))) = (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))))
165	7, 164	gsumsn 18817	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ Mnd ∧ 𝑗 ∈ 𝐾 ∧ (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))) ∈ 𝐵) → (𝐺 Σg (𝑦 ∈ {𝑗} ↦ (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑦(𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))𝑘))))) = (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))))
166	139, 140, 156, 165	syl3anc 1351	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐺 Σg (𝑦 ∈ {𝑗} ↦ (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑦(𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))𝑘))))) = (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))))
167		snfi 8383	. . . . . . . . . . . . 13 ⊢ {𝑗} ∈ Fin
168	167	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → {𝑗} ∈ Fin)
169	18	ad2antrr 713	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝐹:(𝐴 × 𝐶)⟶𝐵)
170	6	adantr 473	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝑗 ∈ 𝐴)
171	170	snssd 4610	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → {𝑗} ⊆ 𝐴)
172		xpss12 5415	. . . . . . . . . . . . . 14 ⊢ (({𝑗} ⊆ 𝐴 ∧ (∪ ran 𝑓 ∪ ran 𝐷) ⊆ 𝐶) → ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)) ⊆ (𝐴 × 𝐶))
173	171, 142, 172	syl2anc 576	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)) ⊆ (𝐴 × 𝐶))
174	169, 173	fssresd 6368	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))):({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))⟶𝐵)
175		xpfi 8576	. . . . . . . . . . . . . 14 ⊢ (({𝑗} ∈ Fin ∧ (∪ ran 𝑓 ∪ ran 𝐷) ∈ Fin) → ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)) ∈ Fin)
176	167, 141, 175	sylancr 578	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)) ∈ Fin)
177	174, 176, 154	fdmfifsupp 8630	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))) finSupp 0 )
178	7, 67, 137, 168, 141, 174, 177	gsumxp 18839	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))) = (𝐺 Σg (𝑦 ∈ {𝑗} ↦ (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑦(𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))𝑘))))))
179	142	resmptd 5747	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran 𝑓 ∪ ran 𝐷)) = (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘)))
180	179	oveq2d 6986	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran 𝑓 ∪ ran 𝐷))) = (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))))
181	166, 178, 180	3eqtr4rd 2819	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran 𝑓 ∪ ran 𝐷))) = (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))))
182	181	eleq1d 2844	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ((𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran 𝑓 ∪ ran 𝐷))) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)) ↔ (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))
183		ovex 7002	. . . . . . . . . . 11 ⊢ ((𝐻‘𝑗) − 𝑔) ∈ V
184	73, 183	elrnmpti 5668	. . . . . . . . . 10 ⊢ ((𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)) ↔ ∃𝑔 ∈ 𝐿 (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))) = ((𝐻‘𝑗) − 𝑔))
185		isabl 18660	. . . . . . . . . . . . . . . 16 ⊢ (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd))
186	43, 10, 185	sylanbrc 575	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐺 ∈ Abel)
187	186	ad3antrrr 717	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔 ∈ 𝐿) → 𝐺 ∈ Abel)
188	6, 35	syldan 582	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐾) → (𝐻‘𝑗) ∈ 𝐵)
189	188	ad2antrr 713	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔 ∈ 𝐿) → (𝐻‘𝑗) ∈ 𝐵)
190	29	ad2antrr 713	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝐿 ⊆ 𝐵)
191	190	sselda 3854	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔 ∈ 𝐿) → 𝑔 ∈ 𝐵)
192	7, 38, 187, 189, 191	ablnncan 18689	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔 ∈ 𝐿) → ((𝐻‘𝑗) − ((𝐻‘𝑗) − 𝑔)) = 𝑔)
193		simpr 477	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔 ∈ 𝐿) → 𝑔 ∈ 𝐿)
194	192, 193	eqeltrd 2860	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔 ∈ 𝐿) → ((𝐻‘𝑗) − ((𝐻‘𝑗) − 𝑔)) ∈ 𝐿)
195		oveq2 6978	. . . . . . . . . . . . 13 ⊢ ((𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))) = ((𝐻‘𝑗) − 𝑔) → ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) = ((𝐻‘𝑗) − ((𝐻‘𝑗) − 𝑔)))
196	195	eleq1d 2844	. . . . . . . . . . . 12 ⊢ ((𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))) = ((𝐻‘𝑗) − 𝑔) → (((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿 ↔ ((𝐻‘𝑗) − ((𝐻‘𝑗) − 𝑔)) ∈ 𝐿))
197	194, 196	syl5ibrcom 239	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔 ∈ 𝐿) → ((𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))) = ((𝐻‘𝑗) − 𝑔) → ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
198	197	rexlimdva 3223	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∃𝑔 ∈ 𝐿 (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))) = ((𝐻‘𝑗) − 𝑔) → ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
199	184, 198	syl5bi 234	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ((𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)) → ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
200	182, 199	sylbid 232	. . . . . . . 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 639	. . . . . 6 ⊢ (((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑗 ∈ 𝐾) → (∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) → ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
203	202	ralimdva 3121	. . . . 5 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∀𝑗 ∈ 𝐾 ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) → ∀𝑗 ∈ 𝐾 ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
204	203	impr 447	. . . 4 ⊢ ((𝜑 ∧ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗 ∈ 𝐾 ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))) → ∀𝑗 ∈ 𝐾 ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿)
205		fveq2 6493	. . . . . . 7 ⊢ (𝑗 = 𝑥 → (𝐻‘𝑗) = (𝐻‘𝑥))
206		sneq 4445	. . . . . . . . . 10 ⊢ (𝑗 = 𝑥 → {𝑗} = {𝑥})
207	206	xpeq1d 5429	. . . . . . . . 9 ⊢ (𝑗 = 𝑥 → ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)) = ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷)))
208	207	reseq2d 5688	. . . . . . . 8 ⊢ (𝑗 = 𝑥 → (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))) = (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷))))
209	208	oveq2d 6986	. . . . . . 7 ⊢ (𝑗 = 𝑥 → (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))) = (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷)))))
210	205, 209	oveq12d 6988	. . . . . 6 ⊢ (𝑗 = 𝑥 → ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) = ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷))))))
211	210	eleq1d 2844	. . . . 5 ⊢ (𝑗 = 𝑥 → (((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿 ↔ ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
212	211	cbvralv 3377	. . . 4 ⊢ (∀𝑗 ∈ 𝐾 ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿 ↔ ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿)
213	204, 212	sylib 210	. . 3 ⊢ ((𝜑 ∧ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗 ∈ 𝐾 ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))) → ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿)
214		sseq2 3879	. . . . 5 ⊢ (𝑛 = (∪ ran 𝑓 ∪ ran 𝐷) → (ran 𝐷 ⊆ 𝑛 ↔ ran 𝐷 ⊆ (∪ ran 𝑓 ∪ ran 𝐷)))
215		xpeq2 5421	. . . . . . . . . 10 ⊢ (𝑛 = (∪ ran 𝑓 ∪ ran 𝐷) → ({𝑥} × 𝑛) = ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷)))
216	215	reseq2d 5688	. . . . . . . . 9 ⊢ (𝑛 = (∪ ran 𝑓 ∪ ran 𝐷) → (𝐹 ↾ ({𝑥} × 𝑛)) = (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷))))
217	216	oveq2d 6986	. . . . . . . 8 ⊢ (𝑛 = (∪ ran 𝑓 ∪ ran 𝐷) → (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛))) = (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷)))))
218	217	oveq2d 6986	. . . . . . 7 ⊢ (𝑛 = (∪ ran 𝑓 ∪ ran 𝐷) → ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) = ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷))))))
219	218	eleq1d 2844	. . . . . 6 ⊢ (𝑛 = (∪ ran 𝑓 ∪ ran 𝐷) → (((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿 ↔ ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
220	219	ralbidv 3141	. . . . 5 ⊢ (𝑛 = (∪ ran 𝑓 ∪ ran 𝐷) → (∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿 ↔ ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
221	214, 220	anbi12d 621	. . . 4 ⊢ (𝑛 = (∪ ran 𝑓 ∪ ran 𝐷) → ((ran 𝐷 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿) ↔ (ran 𝐷 ⊆ (∪ ran 𝑓 ∪ ran 𝐷) ∧ ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿)))
222	221	rspcev 3529	. . 3 ⊢ (((∪ ran 𝑓 ∪ ran 𝐷) ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝐷 ⊆ (∪ ran 𝑓 ∪ ran 𝐷) ∧ ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿)) → ∃𝑛 ∈ (𝒫 𝐶 ∩ Fin)(ran 𝐷 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿))
223	120, 122, 213, 222	syl12anc 824	. 2 ⊢ ((𝜑 ∧ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗 ∈ 𝐾 ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))) → ∃𝑛 ∈ (𝒫 𝐶 ∩ Fin)(ran 𝐷 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿))
224	85, 223	exlimddv 1894	1 ⊢ (𝜑 → ∃𝑛 ∈ (𝒫 𝐶 ∩ Fin)(ran 𝐷 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿))

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 387   = wceq 1507  ∃wex 1742   ∈ wcel 2048  ∀wral 3082  ∃wrex 3083  Vcvv 3409   ∪ cun 3823   ∩ cin 3824   ⊆ wss 3825  𝒫 cpw 4416  {csn 4435  ∪ cuni 4706   ↦ cmpt 5002   × cxp 5398  dom cdm 5400  ran crn 5401   ↾ cres 5402   “ cima 5403   ∘ ccom 5404   Fn wfn 6177  ⟶wf 6178  –onto→wfo 6180  ‘cfv 6182  (class class class)co 6970  Fincfn 8298  Basecbs 16329  +_gcplusg 16411  TopOpenctopn 16541  0_gc0g 16559   Σ_g cgsu 16560  Mndcmnd 17752  Grpcgrp 17881  inv_gcminusg 17882  -_gcsg 17883  CMndccmn 18656  Abelcabl 18657  TopOnctopon 21212  TopSpctps 21234  Homeochmeo 22055  TopGrpctgp 22373   tsums ctsu 22427

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-13 2299  ax-ext 2745  ax-rep 5043  ax-sep 5054  ax-nul 5061  ax-pow 5113  ax-pr 5180  ax-un 7273  ax-cnex 10383  ax-resscn 10384  ax-1cn 10385  ax-icn 10386  ax-addcl 10387  ax-addrcl 10388  ax-mulcl 10389  ax-mulrcl 10390  ax-mulcom 10391  ax-addass 10392  ax-mulass 10393  ax-distr 10394  ax-i2m1 10395  ax-1ne0 10396  ax-1rid 10397  ax-rnegex 10398  ax-rrecex 10399  ax-cnre 10400  ax-pre-lttri 10401  ax-pre-lttrn 10402  ax-pre-ltadd 10403  ax-pre-mulgt0 10404

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-mo 2544  df-eu 2580  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ne 2962  df-nel 3068  df-ral 3087  df-rex 3088  df-reu 3089  df-rmo 3090  df-rab 3091  df-v 3411  df-sbc 3678  df-csb 3783  df-dif 3828  df-un 3830  df-in 3832  df-ss 3839  df-pss 3841  df-nul 4174  df-if 4345  df-pw 4418  df-sn 4436  df-pr 4438  df-tp 4440  df-op 4442  df-uni 4707  df-int 4744  df-iun 4788  df-iin 4789  df-br 4924  df-opab 4986  df-mpt 5003  df-tr 5025  df-id 5305  df-eprel 5310  df-po 5319  df-so 5320  df-fr 5359  df-se 5360  df-we 5361  df-xp 5406  df-rel 5407  df-cnv 5408  df-co 5409  df-dm 5410  df-rn 5411  df-res 5412  df-ima 5413  df-pred 5980  df-ord 6026  df-on 6027  df-lim 6028  df-suc 6029  df-iota 6146  df-fun 6184  df-fn 6185  df-f 6186  df-f1 6187  df-fo 6188  df-f1o 6189  df-fv 6190  df-isom 6191  df-riota 6931  df-ov 6973  df-oprab 6974  df-mpo 6975  df-of 7221  df-om 7391  df-1st 7494  df-2nd 7495  df-supp 7627  df-wrecs 7743  df-recs 7805  df-rdg 7843  df-1o 7897  df-oadd 7901  df-er 8081  df-map 8200  df-en 8299  df-dom 8300  df-sdom 8301  df-fin 8302  df-fsupp 8621  df-oi 8761  df-card 9154  df-pnf 10468  df-mnf 10469  df-xr 10470  df-ltxr 10471  df-le 10472  df-sub 10664  df-neg 10665  df-nn 11432  df-2 11496  df-n0 11701  df-z 11787  df-uz 12052  df-fz 12702  df-fzo 12843  df-seq 13178  df-hash 13499  df-ndx 16332  df-slot 16333  df-base 16335  df-sets 16336  df-ress 16337  df-plusg 16424  df-0g 16561  df-gsum 16562  df-topgen 16563  df-mre 16705  df-mrc 16706  df-acs 16708  df-plusf 17699  df-mgm 17700  df-sgrp 17742  df-mnd 17753  df-submnd 17794  df-grp 17884  df-minusg 17885  df-sbg 17886  df-mulg 18002  df-cntz 18208  df-cmn 18658  df-abl 18659  df-fbas 20234  df-fg 20235  df-top 21196  df-topon 21213  df-topsp 21235  df-bases 21248  df-ntr 21322  df-nei 21400  df-cn 21529  df-cnp 21530  df-tx 21864  df-hmeo 22057  df-fil 22148  df-fm 22240  df-flim 22241  df-flf 22242  df-tmd 22374  df-tgp 22375  df-tsms 22428

This theorem is referenced by:  tsmsxp  22456