Theorem tsmsxplem1 23304

Description: Lemma for tsmsxp 23306. (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 4133	. . 3 ⊢ (𝜑 → 𝐾 ∈ Fin)
3		elfpw 9121	. . . . . . . 8 ⊢ (𝐾 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝐾 ⊆ 𝐴 ∧ 𝐾 ∈ Fin))
4	3	simplbi 498	. . . . . . 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 2738	. . . . . 6 ⊢ (𝒫 𝐶 ∩ Fin) = (𝒫 𝐶 ∩ Fin)
10		tsmsxp.g	. . . . . . 7 ⊢ (𝜑 → 𝐺 ∈ CMnd)
11	10	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐺 ∈ CMnd)
12		tsmsxp.2	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ TopGrp)
13		tgptps 23231	. . . . . . . 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		fovrn 7442	. . . . . . . . 9 ⊢ ((𝐹:(𝐴 × 𝐶)⟶𝐵 ∧ 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶) → (𝑗𝐹𝑘) ∈ 𝐵)
20	18, 19	syl3an1 1162	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶) → (𝑗𝐹𝑘) ∈ 𝐵)
21	20	3expa 1117	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴) ∧ 𝑘 ∈ 𝐶) → (𝑗𝐹𝑘) ∈ 𝐵)
22	21	fmpttd 6989	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)):𝐶⟶𝐵)
23		tsmsxp.1	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝐻‘𝑗) ∈ (𝐺 tsums (𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘))))
24		df-ima 5602	. . . . . . . 8 ⊢ ((𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) “ 𝐿) = ran ((𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) ↾ 𝐿)
25	8, 7	tgptopon 23233	. . . . . . . . . . . . 13 ⊢ (𝐺 ∈ TopGrp → 𝐽 ∈ (TopOn‘𝐵))
26	12, 25	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝐵))
27		tsmsxp.l	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐿 ∈ 𝐽)
28		toponss 22076	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ (TopOn‘𝐵) ∧ 𝐿 ∈ 𝐽) → 𝐿 ⊆ 𝐵)
29	26, 27, 28	syl2anc 584	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐿 ⊆ 𝐵)
30	29	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐿 ⊆ 𝐵)
31	30	resmptd 5948	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ((𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) ↾ 𝐿) = (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))
32	31	rneqd 5847	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ran ((𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) ↾ 𝐿) = ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))
33	24, 32	eqtrid 2790	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ((𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) “ 𝐿) = ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))
34		tsmsxp.h	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐻:𝐴⟶𝐵)
35	34	ffvelrnda 6961	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝐻‘𝑗) ∈ 𝐵)
36		tsmsxp.p	. . . . . . . . . . . . 13 ⊢ + = (+g‘𝐺)
37		eqid 2738	. . . . . . . . . . . . 13 ⊢ (invg‘𝐺) = (invg‘𝐺)
38		tsmsxp.m	. . . . . . . . . . . . 13 ⊢ − = (-g‘𝐺)
39	7, 36, 37, 38	grpsubval 18625	. . . . . . . . . . . 12 ⊢ (((𝐻‘𝑗) ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → ((𝐻‘𝑗) − 𝑔) = ((𝐻‘𝑗) + ((invg‘𝐺)‘𝑔)))
40	35, 39	sylan 580	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴) ∧ 𝑔 ∈ 𝐵) → ((𝐻‘𝑗) − 𝑔) = ((𝐻‘𝑗) + ((invg‘𝐺)‘𝑔)))
41	40	mpteq2dva 5174	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) = (𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) + ((invg‘𝐺)‘𝑔))))
42		tgpgrp 23229	. . . . . . . . . . . . . 14 ⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ Grp)
43	12, 42	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐺 ∈ Grp)
44	43	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐺 ∈ Grp)
45	7, 37	grpinvcl 18627	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ Grp ∧ 𝑔 ∈ 𝐵) → ((invg‘𝐺)‘𝑔) ∈ 𝐵)
46	44, 45	sylan 580	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴) ∧ 𝑔 ∈ 𝐵) → ((invg‘𝐺)‘𝑔) ∈ 𝐵)
47	7, 37	grpinvf 18626	. . . . . . . . . . . . 13 ⊢ (𝐺 ∈ Grp → (invg‘𝐺):𝐵⟶𝐵)
48	44, 47	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (invg‘𝐺):𝐵⟶𝐵)
49	48	feqmptd 6837	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (invg‘𝐺) = (𝑔 ∈ 𝐵 ↦ ((invg‘𝐺)‘𝑔)))
50		eqidd 2739	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) = (𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)))
51		oveq2 7283	. . . . . . . . . . 11 ⊢ (𝑦 = ((invg‘𝐺)‘𝑔) → ((𝐻‘𝑗) + 𝑦) = ((𝐻‘𝑗) + ((invg‘𝐺)‘𝑔)))
52	46, 49, 50, 51	fmptco 7001	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ((𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) ∘ (invg‘𝐺)) = (𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) + ((invg‘𝐺)‘𝑔))))
53	41, 52	eqtr4d 2781	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) = ((𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) ∘ (invg‘𝐺)))
54	12	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐺 ∈ TopGrp)
55	8, 37	grpinvhmeo 23237	. . . . . . . . . . 11 ⊢ (𝐺 ∈ TopGrp → (invg‘𝐺) ∈ (𝐽Homeo𝐽))
56	54, 55	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (invg‘𝐺) ∈ (𝐽Homeo𝐽))
57		eqid 2738	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) = (𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦))
58	57, 7, 36, 8	tgplacthmeo 23254	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ TopGrp ∧ (𝐻‘𝑗) ∈ 𝐵) → (𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) ∈ (𝐽Homeo𝐽))
59	54, 35, 58	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) ∈ (𝐽Homeo𝐽))
60		hmeoco 22923	. . . . . . . . . 10 ⊢ (((invg‘𝐺) ∈ (𝐽Homeo𝐽) ∧ (𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) ∈ (𝐽Homeo𝐽)) → ((𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) ∘ (invg‘𝐺)) ∈ (𝐽Homeo𝐽))
61	56, 59, 60	syl2anc 584	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ((𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) ∘ (invg‘𝐺)) ∈ (𝐽Homeo𝐽))
62	53, 61	eqeltrd 2839	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) ∈ (𝐽Homeo𝐽))
63	27	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐿 ∈ 𝐽)
64		hmeoima 22916	. . . . . . . 8 ⊢ (((𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) ∈ (𝐽Homeo𝐽) ∧ 𝐿 ∈ 𝐽) → ((𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) “ 𝐿) ∈ 𝐽)
65	62, 63, 64	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ((𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) “ 𝐿) ∈ 𝐽)
66	33, 65	eqeltrrd 2840	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)) ∈ 𝐽)
67		tsmsxp.z	. . . . . . . . 9 ⊢ 0 = (0g‘𝐺)
68	7, 67, 38	grpsubid1 18660	. . . . . . . 8 ⊢ ((𝐺 ∈ Grp ∧ (𝐻‘𝑗) ∈ 𝐵) → ((𝐻‘𝑗) − 0 ) = (𝐻‘𝑗))
69	44, 35, 68	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ((𝐻‘𝑗) − 0 ) = (𝐻‘𝑗))
70		tsmsxp.3	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ 𝐿)
71	70	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 0 ∈ 𝐿)
72		ovex 7308	. . . . . . . 8 ⊢ ((𝐻‘𝑗) − 0 ) ∈ V
73		eqid 2738	. . . . . . . . 9 ⊢ (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)) = (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))
74		oveq2 7283	. . . . . . . . 9 ⊢ (𝑔 = 0 → ((𝐻‘𝑗) − 𝑔) = ((𝐻‘𝑗) − 0 ))
75	73, 74	elrnmpt1s 5866	. . . . . . . 8 ⊢ (( 0 ∈ 𝐿 ∧ ((𝐻‘𝑗) − 0 ) ∈ V) → ((𝐻‘𝑗) − 0 ) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))
76	71, 72, 75	sylancl 586	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ((𝐻‘𝑗) − 0 ) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))
77	69, 76	eqeltrrd 2840	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝐻‘𝑗) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))
78	7, 8, 9, 11, 15, 17, 22, 23, 66, 77	tsmsi 23285	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ∃𝑦 ∈ (𝒫 𝐶 ∩ Fin)∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))
79	6, 78	syldan 591	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐾) → ∃𝑦 ∈ (𝒫 𝐶 ∩ Fin)∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))
80	79	ralrimiva 3103	. . 3 ⊢ (𝜑 → ∀𝑗 ∈ 𝐾 ∃𝑦 ∈ (𝒫 𝐶 ∩ Fin)∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))
81		sseq1 3946	. . . . . 6 ⊢ (𝑦 = (𝑓‘𝑗) → (𝑦 ⊆ 𝑧 ↔ (𝑓‘𝑗) ⊆ 𝑧))
82	81	imbi1d 342	. . . . 5 ⊢ (𝑦 = (𝑓‘𝑗) → ((𝑦 ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) ↔ ((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))))
83	82	ralbidv 3112	. . . 4 ⊢ (𝑦 = (𝑓‘𝑗) → (∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) ↔ ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))))
84	83	ac6sfi 9058	. . 3 ⊢ ((𝐾 ∈ Fin ∧ ∀𝑗 ∈ 𝐾 ∃𝑦 ∈ (𝒫 𝐶 ∩ Fin)∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))) → ∃𝑓(𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗 ∈ 𝐾 ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))))
85	2, 80, 84	syl2anc 584	. 2 ⊢ (𝜑 → ∃𝑓(𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗 ∈ 𝐾 ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))))
86		frn 6607	. . . . . . . . 9 ⊢ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) → ran 𝑓 ⊆ (𝒫 𝐶 ∩ Fin))
87	86	adantl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝑓 ⊆ (𝒫 𝐶 ∩ Fin))
88		inss1 4162	. . . . . . . 8 ⊢ (𝒫 𝐶 ∩ Fin) ⊆ 𝒫 𝐶
89	87, 88	sstrdi 3933	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝑓 ⊆ 𝒫 𝐶)
90		sspwuni 5029	. . . . . . 7 ⊢ (ran 𝑓 ⊆ 𝒫 𝐶 ↔ ∪ ran 𝑓 ⊆ 𝐶)
91	89, 90	sylib 217	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ∪ ran 𝑓 ⊆ 𝐶)
92		tsmsxp.d	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin))
93		elfpw 9121	. . . . . . . . . 10 ⊢ (𝐷 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ↔ (𝐷 ⊆ (𝐴 × 𝐶) ∧ 𝐷 ∈ Fin))
94	93	simplbi 498	. . . . . . . . 9 ⊢ (𝐷 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) → 𝐷 ⊆ (𝐴 × 𝐶))
95		rnss 5848	. . . . . . . . 9 ⊢ (𝐷 ⊆ (𝐴 × 𝐶) → ran 𝐷 ⊆ ran (𝐴 × 𝐶))
96	92, 94, 95	3syl 18	. . . . . . . 8 ⊢ (𝜑 → ran 𝐷 ⊆ ran (𝐴 × 𝐶))
97		rnxpss 6075	. . . . . . . 8 ⊢ ran (𝐴 × 𝐶) ⊆ 𝐶
98	96, 97	sstrdi 3933	. . . . . . 7 ⊢ (𝜑 → ran 𝐷 ⊆ 𝐶)
99	98	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝐷 ⊆ 𝐶)
100	91, 99	unssd 4120	. . . . 5 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∪ ran 𝑓 ∪ ran 𝐷) ⊆ 𝐶)
101	2	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝐾 ∈ Fin)
102		ffn 6600	. . . . . . . . . 10 ⊢ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) → 𝑓 Fn 𝐾)
103	102	adantl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝑓 Fn 𝐾)
104		dffn4 6694	. . . . . . . . 9 ⊢ (𝑓 Fn 𝐾 ↔ 𝑓:𝐾–onto→ran 𝑓)
105	103, 104	sylib 217	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝑓:𝐾–onto→ran 𝑓)
106		fofi 9105	. . . . . . . 8 ⊢ ((𝐾 ∈ Fin ∧ 𝑓:𝐾–onto→ran 𝑓) → ran 𝑓 ∈ Fin)
107	101, 105, 106	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝑓 ∈ Fin)
108		inss2 4163	. . . . . . . 8 ⊢ (𝒫 𝐶 ∩ Fin) ⊆ Fin
109	87, 108	sstrdi 3933	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝑓 ⊆ Fin)
110		unifi 9108	. . . . . . 7 ⊢ ((ran 𝑓 ∈ Fin ∧ ran 𝑓 ⊆ Fin) → ∪ ran 𝑓 ∈ Fin)
111	107, 109, 110	syl2anc 584	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ∪ ran 𝑓 ∈ Fin)
112		elinel2 4130	. . . . . . . 8 ⊢ (𝐷 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) → 𝐷 ∈ Fin)
113		rnfi 9102	. . . . . . . 8 ⊢ (𝐷 ∈ Fin → ran 𝐷 ∈ Fin)
114	92, 112, 113	3syl 18	. . . . . . 7 ⊢ (𝜑 → ran 𝐷 ∈ Fin)
115	114	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝐷 ∈ Fin)
116		unfi 8955	. . . . . 6 ⊢ ((∪ ran 𝑓 ∈ Fin ∧ ran 𝐷 ∈ Fin) → (∪ ran 𝑓 ∪ ran 𝐷) ∈ Fin)
117	111, 115, 116	syl2anc 584	. . . . 5 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∪ ran 𝑓 ∪ ran 𝐷) ∈ Fin)
118		elfpw 9121	. . . . 5 ⊢ ((∪ ran 𝑓 ∪ ran 𝐷) ∈ (𝒫 𝐶 ∩ Fin) ↔ ((∪ ran 𝑓 ∪ ran 𝐷) ⊆ 𝐶 ∧ (∪ ran 𝑓 ∪ ran 𝐷) ∈ Fin))
119	100, 117, 118	sylanbrc 583	. . . 4 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∪ ran 𝑓 ∪ ran 𝐷) ∈ (𝒫 𝐶 ∩ Fin))
120	119	adantrr 714	. . 3 ⊢ ((𝜑 ∧ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗 ∈ 𝐾 ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))) → (∪ ran 𝑓 ∪ ran 𝐷) ∈ (𝒫 𝐶 ∩ Fin))
121		ssun2 4107	. . . 4 ⊢ ran 𝐷 ⊆ (∪ ran 𝑓 ∪ ran 𝐷)
122	121	a1i 11	. . 3 ⊢ ((𝜑 ∧ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗 ∈ 𝐾 ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))) → ran 𝐷 ⊆ (∪ ran 𝑓 ∪ ran 𝐷))
123	119	adantlr 712	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∪ ran 𝑓 ∪ ran 𝐷) ∈ (𝒫 𝐶 ∩ Fin))
124		fvssunirn 6803	. . . . . . . . . . . . . 14 ⊢ (𝑓‘𝑗) ⊆ ∪ ran 𝑓
125		ssun1 4106	. . . . . . . . . . . . . 14 ⊢ ∪ ran 𝑓 ⊆ (∪ ran 𝑓 ∪ ran 𝐷)
126	124, 125	sstri 3930	. . . . . . . . . . . . 13 ⊢ (𝑓‘𝑗) ⊆ (∪ ran 𝑓 ∪ ran 𝐷)
127		id 22	. . . . . . . . . . . . 13 ⊢ (𝑧 = (∪ ran 𝑓 ∪ ran 𝐷) → 𝑧 = (∪ ran 𝑓 ∪ ran 𝐷))
128	126, 127	sseqtrrid 3974	. . . . . . . . . . . 12 ⊢ (𝑧 = (∪ ran 𝑓 ∪ ran 𝐷) → (𝑓‘𝑗) ⊆ 𝑧)
129		pm5.5 362	. . . . . . . . . . . 12 ⊢ ((𝑓‘𝑗) ⊆ 𝑧 → (((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) ↔ (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))
130	128, 129	syl 17	. . . . . . . . . . 11 ⊢ (𝑧 = (∪ ran 𝑓 ∪ ran 𝐷) → (((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) ↔ (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))
131		reseq2 5886	. . . . . . . . . . . . 13 ⊢ (𝑧 = (∪ ran 𝑓 ∪ ran 𝐷) → ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧) = ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran 𝑓 ∪ ran 𝐷)))
132	131	oveq2d 7291	. . . . . . . . . . . 12 ⊢ (𝑧 = (∪ ran 𝑓 ∪ ran 𝐷) → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) = (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran 𝑓 ∪ ran 𝐷))))
133	132	eleq1d 2823	. . . . . . . . . . 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 3557	. . . . . . . . 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 723	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝐺 ∈ CMnd)
138		cmnmnd 19402	. . . . . . . . . . . . 13 ⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd)
139	137, 138	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝐺 ∈ Mnd)
140		simplr 766	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝑗 ∈ 𝐾)
141	117	adantlr 712	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∪ ran 𝑓 ∪ ran 𝐷) ∈ Fin)
142	100	adantlr 712	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∪ ran 𝑓 ∪ ran 𝐷) ⊆ 𝐶)
143	142	sselda 3921	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷)) → 𝑘 ∈ 𝐶)
144	18	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐾) → 𝐹:(𝐴 × 𝐶)⟶𝐵)
145	144, 6	jca 512	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐾) → (𝐹:(𝐴 × 𝐶)⟶𝐵 ∧ 𝑗 ∈ 𝐴))
146	19	3expa 1117	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹:(𝐴 × 𝐶)⟶𝐵 ∧ 𝑗 ∈ 𝐴) ∧ 𝑘 ∈ 𝐶) → (𝑗𝐹𝑘) ∈ 𝐵)
147	145, 146	sylan 580	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑘 ∈ 𝐶) → (𝑗𝐹𝑘) ∈ 𝐵)
148	147	adantlr 712	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ 𝐶) → (𝑗𝐹𝑘) ∈ 𝐵)
149	143, 148	syldan 591	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷)) → (𝑗𝐹𝑘) ∈ 𝐵)
150	149	fmpttd 6989	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘)):(∪ ran 𝑓 ∪ ran 𝐷)⟶𝐵)
151		eqid 2738	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘)) = (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))
152		ovexd 7310	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷)) → (𝑗𝐹𝑘) ∈ V)
153	67	fvexi 6788	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ V
154	153	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 0 ∈ V)
155	151, 141, 152, 154	fsuppmptdm 9139	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘)) finSupp 0 )
156	7, 67, 137, 141, 150, 155	gsumcl 19516	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))) ∈ 𝐵)
157		velsn 4577	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ {𝑗} ↔ 𝑦 = 𝑗)
158		ovres 7438	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ {𝑗} ∧ 𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷)) → (𝑦(𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))𝑘) = (𝑦𝐹𝑘))
159	157, 158	sylanbr 582	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 = 𝑗 ∧ 𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷)) → (𝑦(𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))𝑘) = (𝑦𝐹𝑘))
160		oveq1 7282	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑗 → (𝑦𝐹𝑘) = (𝑗𝐹𝑘))
161	160	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 = 𝑗 ∧ 𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷)) → (𝑦𝐹𝑘) = (𝑗𝐹𝑘))
162	159, 161	eqtrd 2778	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 = 𝑗 ∧ 𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷)) → (𝑦(𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))𝑘) = (𝑗𝐹𝑘))
163	162	mpteq2dva 5174	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑗 → (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑦(𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))𝑘)) = (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘)))
164	163	oveq2d 7291	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑗 → (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑦(𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))𝑘))) = (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))))
165	7, 164	gsumsn 19555	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ Mnd ∧ 𝑗 ∈ 𝐾 ∧ (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))) ∈ 𝐵) → (𝐺 Σg (𝑦 ∈ {𝑗} ↦ (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑦(𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))𝑘))))) = (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))))
166	139, 140, 156, 165	syl3anc 1370	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐺 Σg (𝑦 ∈ {𝑗} ↦ (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑦(𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))𝑘))))) = (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))))
167		snfi 8834	. . . . . . . . . . . . 13 ⊢ {𝑗} ∈ Fin
168	167	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → {𝑗} ∈ Fin)
169	18	ad2antrr 723	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝐹:(𝐴 × 𝐶)⟶𝐵)
170	6	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝑗 ∈ 𝐴)
171	170	snssd 4742	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → {𝑗} ⊆ 𝐴)
172		xpss12 5604	. . . . . . . . . . . . . 14 ⊢ (({𝑗} ⊆ 𝐴 ∧ (∪ ran 𝑓 ∪ ran 𝐷) ⊆ 𝐶) → ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)) ⊆ (𝐴 × 𝐶))
173	171, 142, 172	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)) ⊆ (𝐴 × 𝐶))
174	169, 173	fssresd 6641	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))):({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))⟶𝐵)
175		xpfi 9085	. . . . . . . . . . . . . 14 ⊢ (({𝑗} ∈ Fin ∧ (∪ ran 𝑓 ∪ ran 𝐷) ∈ Fin) → ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)) ∈ Fin)
176	167, 141, 175	sylancr 587	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)) ∈ Fin)
177	174, 176, 154	fdmfifsupp 9138	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))) finSupp 0 )
178	7, 67, 137, 168, 141, 174, 177	gsumxp 19577	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))) = (𝐺 Σg (𝑦 ∈ {𝑗} ↦ (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑦(𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))𝑘))))))
179	142	resmptd 5948	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran 𝑓 ∪ ran 𝐷)) = (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘)))
180	179	oveq2d 7291	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran 𝑓 ∪ ran 𝐷))) = (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))))
181	166, 178, 180	3eqtr4rd 2789	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran 𝑓 ∪ ran 𝐷))) = (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))))
182	181	eleq1d 2823	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ((𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran 𝑓 ∪ ran 𝐷))) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)) ↔ (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))
183		ovex 7308	. . . . . . . . . . 11 ⊢ ((𝐻‘𝑗) − 𝑔) ∈ V
184	73, 183	elrnmpti 5869	. . . . . . . . . 10 ⊢ ((𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)) ↔ ∃𝑔 ∈ 𝐿 (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))) = ((𝐻‘𝑗) − 𝑔))
185		isabl 19390	. . . . . . . . . . . . . . . 16 ⊢ (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd))
186	43, 10, 185	sylanbrc 583	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐺 ∈ Abel)
187	186	ad3antrrr 727	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔 ∈ 𝐿) → 𝐺 ∈ Abel)
188	6, 35	syldan 591	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐾) → (𝐻‘𝑗) ∈ 𝐵)
189	188	ad2antrr 723	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔 ∈ 𝐿) → (𝐻‘𝑗) ∈ 𝐵)
190	29	ad2antrr 723	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝐿 ⊆ 𝐵)
191	190	sselda 3921	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔 ∈ 𝐿) → 𝑔 ∈ 𝐵)
192	7, 38, 187, 189, 191	ablnncan 19422	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔 ∈ 𝐿) → ((𝐻‘𝑗) − ((𝐻‘𝑗) − 𝑔)) = 𝑔)
193		simpr 485	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔 ∈ 𝐿) → 𝑔 ∈ 𝐿)
194	192, 193	eqeltrd 2839	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔 ∈ 𝐿) → ((𝐻‘𝑗) − ((𝐻‘𝑗) − 𝑔)) ∈ 𝐿)
195		oveq2 7283	. . . . . . . . . . . . 13 ⊢ ((𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))) = ((𝐻‘𝑗) − 𝑔) → ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) = ((𝐻‘𝑗) − ((𝐻‘𝑗) − 𝑔)))
196	195	eleq1d 2823	. . . . . . . . . . . 12 ⊢ ((𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))) = ((𝐻‘𝑗) − 𝑔) → (((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿 ↔ ((𝐻‘𝑗) − ((𝐻‘𝑗) − 𝑔)) ∈ 𝐿))
197	194, 196	syl5ibrcom 246	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔 ∈ 𝐿) → ((𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))) = ((𝐻‘𝑗) − 𝑔) → ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
198	197	rexlimdva 3213	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∃𝑔 ∈ 𝐿 (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))) = ((𝐻‘𝑗) − 𝑔) → ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
199	184, 198	syl5bi 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 649	. . . . . 6 ⊢ (((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑗 ∈ 𝐾) → (∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) → ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
203	202	ralimdva 3108	. . . . 5 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∀𝑗 ∈ 𝐾 ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) → ∀𝑗 ∈ 𝐾 ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
204	203	impr 455	. . . 4 ⊢ ((𝜑 ∧ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗 ∈ 𝐾 ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))) → ∀𝑗 ∈ 𝐾 ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿)
205		fveq2 6774	. . . . . . 7 ⊢ (𝑗 = 𝑥 → (𝐻‘𝑗) = (𝐻‘𝑥))
206		sneq 4571	. . . . . . . . . 10 ⊢ (𝑗 = 𝑥 → {𝑗} = {𝑥})
207	206	xpeq1d 5618	. . . . . . . . 9 ⊢ (𝑗 = 𝑥 → ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)) = ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷)))
208	207	reseq2d 5891	. . . . . . . 8 ⊢ (𝑗 = 𝑥 → (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))) = (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷))))
209	208	oveq2d 7291	. . . . . . 7 ⊢ (𝑗 = 𝑥 → (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))) = (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷)))))
210	205, 209	oveq12d 7293	. . . . . 6 ⊢ (𝑗 = 𝑥 → ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) = ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷))))))
211	210	eleq1d 2823	. . . . 5 ⊢ (𝑗 = 𝑥 → (((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿 ↔ ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
212	211	cbvralvw 3383	. . . 4 ⊢ (∀𝑗 ∈ 𝐾 ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿 ↔ ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿)
213	204, 212	sylib 217	. . 3 ⊢ ((𝜑 ∧ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗 ∈ 𝐾 ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))) → ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿)
214		sseq2 3947	. . . . 5 ⊢ (𝑛 = (∪ ran 𝑓 ∪ ran 𝐷) → (ran 𝐷 ⊆ 𝑛 ↔ ran 𝐷 ⊆ (∪ ran 𝑓 ∪ ran 𝐷)))
215		xpeq2 5610	. . . . . . . . . 10 ⊢ (𝑛 = (∪ ran 𝑓 ∪ ran 𝐷) → ({𝑥} × 𝑛) = ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷)))
216	215	reseq2d 5891	. . . . . . . . 9 ⊢ (𝑛 = (∪ ran 𝑓 ∪ ran 𝐷) → (𝐹 ↾ ({𝑥} × 𝑛)) = (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷))))
217	216	oveq2d 7291	. . . . . . . 8 ⊢ (𝑛 = (∪ ran 𝑓 ∪ ran 𝐷) → (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛))) = (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷)))))
218	217	oveq2d 7291	. . . . . . 7 ⊢ (𝑛 = (∪ ran 𝑓 ∪ ran 𝐷) → ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) = ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷))))))
219	218	eleq1d 2823	. . . . . 6 ⊢ (𝑛 = (∪ ran 𝑓 ∪ ran 𝐷) → (((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿 ↔ ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
220	219	ralbidv 3112	. . . . 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 3561	. . 3 ⊢ (((∪ ran 𝑓 ∪ ran 𝐷) ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝐷 ⊆ (∪ ran 𝑓 ∪ ran 𝐷) ∧ ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿)) → ∃𝑛 ∈ (𝒫 𝐶 ∩ Fin)(ran 𝐷 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿))
223	120, 122, 213, 222	syl12anc 834	. 2 ⊢ ((𝜑 ∧ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗 ∈ 𝐾 ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))) → ∃𝑛 ∈ (𝒫 𝐶 ∩ Fin)(ran 𝐷 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿))
224	85, 223	exlimddv 1938	1 ⊢ (𝜑 → ∃𝑛 ∈ (𝒫 𝐶 ∩ Fin)(ran 𝐷 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539  ∃wex 1782   ∈ wcel 2106  ∀wral 3064  ∃wrex 3065  Vcvv 3432   ∪ cun 3885   ∩ cin 3886   ⊆ wss 3887  𝒫 cpw 4533  {csn 4561  ∪ cuni 4839   ↦ cmpt 5157   × cxp 5587  dom cdm 5589  ran crn 5590   ↾ cres 5591   “ cima 5592   ∘ ccom 5593   Fn wfn 6428  ⟶wf 6429  –onto→wfo 6431  ‘cfv 6433  (class class class)co 7275  Fincfn 8733  Basecbs 16912  +_gcplusg 16962  TopOpenctopn 17132  0_gc0g 17150   Σ_g cgsu 17151  Mndcmnd 18385  Grpcgrp 18577  inv_gcminusg 18578  -_gcsg 18579  CMndccmn 19386  Abelcabl 19387  TopOnctopon 22059  TopSpctps 22081  Homeochmeo 22904  TopGrpctgp 23222   tsums ctsu 23277

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  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 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-cnex 10927  ax-resscn 10928  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-addrcl 10932  ax-mulcl 10933  ax-mulrcl 10934  ax-mulcom 10935  ax-addass 10936  ax-mulass 10937  ax-distr 10938  ax-i2m1 10939  ax-1ne0 10940  ax-1rid 10941  ax-rnegex 10942  ax-rrecex 10943  ax-cnre 10944  ax-pre-lttri 10945  ax-pre-lttrn 10946  ax-pre-ltadd 10947  ax-pre-mulgt0 10948

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-rmo 3071  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-int 4880  df-iun 4926  df-iin 4927  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-se 5545  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-isom 6442  df-riota 7232  df-ov 7278  df-oprab 7279  df-mpo 7280  df-of 7533  df-om 7713  df-1st 7831  df-2nd 7832  df-supp 7978  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-rdg 8241  df-1o 8297  df-er 8498  df-map 8617  df-en 8734  df-dom 8735  df-sdom 8736  df-fin 8737  df-fsupp 9129  df-oi 9269  df-card 9697  df-pnf 11011  df-mnf 11012  df-xr 11013  df-ltxr 11014  df-le 11015  df-sub 11207  df-neg 11208  df-nn 11974  df-2 12036  df-n0 12234  df-z 12320  df-uz 12583  df-fz 13240  df-fzo 13383  df-seq 13722  df-hash 14045  df-sets 16865  df-slot 16883  df-ndx 16895  df-base 16913  df-ress 16942  df-plusg 16975  df-0g 17152  df-gsum 17153  df-topgen 17154  df-mre 17295  df-mrc 17296  df-acs 17298  df-plusf 18325  df-mgm 18326  df-sgrp 18375  df-mnd 18386  df-submnd 18431  df-grp 18580  df-minusg 18581  df-sbg 18582  df-mulg 18701  df-cntz 18923  df-cmn 19388  df-abl 19389  df-fbas 20594  df-fg 20595  df-top 22043  df-topon 22060  df-topsp 22082  df-bases 22096  df-ntr 22171  df-nei 22249  df-cn 22378  df-cnp 22379  df-tx 22713  df-hmeo 22906  df-fil 22997  df-fm 23089  df-flim 23090  df-flf 23091  df-tmd 23223  df-tgp 23224  df-tsms 23278

This theorem is referenced by:  tsmsxp  23306