tsmsxp - Metamath Proof Explorer

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

Theorem tsmsxp 24098

Description: Write a sum over a two-dimensional region as a double sum. This infinite group sum version of gsumxp 19962 is also known as Fubini's theorem. The converse is not necessarily true without additional assumptions. See tsmsxplem1 24096 for the main proof; this part mostly sets up the local assumptions. (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 (𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘))))

**Assertion**
Ref	Expression
tsmsxp	⊢ (𝜑 → (𝐺 tsums 𝐹) ⊆ (𝐺 tsums 𝐻))

Distinct variable groups: 𝑗,𝑘,𝐺 𝐵,𝑘 𝐴,𝑗,𝑘 𝑗,𝐻,𝑘 𝐶,𝑗,𝑘 𝑗,𝐹,𝑘 𝜑,𝑗,𝑘 Allowed substitution hints: 𝐵(𝑗) 𝑉(𝑗,𝑘) 𝑊(𝑗,𝑘)

Proof of Theorem tsmsxp Dummy variables 𝑔 𝑦 𝑧 𝑎 𝑏 𝑐 𝑑 ℎ 𝑛 𝑠 𝑡 𝑢 𝑣 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		tsmsxp.2	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺 ∈ TopGrp)
2		tgptmd 24022	. . . . . . . . . . 11 ⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ TopMnd)
3	1, 2	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺 ∈ TopMnd)
4	3	3ad2ant1 1133	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → 𝐺 ∈ TopMnd)
5		simp2 1137	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → 𝑢 ∈ (TopOpen‘𝐺))
6		eqid 2736	. . . . . . . . . . . . 13 ⊢ (TopOpen‘𝐺) = (TopOpen‘𝐺)
7		tsmsxp.b	. . . . . . . . . . . . 13 ⊢ 𝐵 = (Base‘𝐺)
8	6, 7	tmdtopon 24024	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ TopMnd → (TopOpen‘𝐺) ∈ (TopOn‘𝐵))
9	4, 8	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → (TopOpen‘𝐺) ∈ (TopOn‘𝐵))
10		toponss 22870	. . . . . . . . . . 11 ⊢ (((TopOpen‘𝐺) ∈ (TopOn‘𝐵) ∧ 𝑢 ∈ (TopOpen‘𝐺)) → 𝑢 ⊆ 𝐵)
11	9, 5, 10	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → 𝑢 ⊆ 𝐵)
12		simp3 1138	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → 𝑥 ∈ 𝑢)
13	11, 12	sseldd 3964	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → 𝑥 ∈ 𝐵)
14		tmdmnd 24018	. . . . . . . . . . 11 ⊢ (𝐺 ∈ TopMnd → 𝐺 ∈ Mnd)
15	4, 14	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → 𝐺 ∈ Mnd)
16		eqid 2736	. . . . . . . . . . 11 ⊢ (0_g‘𝐺) = (0_g‘𝐺)
17	7, 16	mndidcl 18732	. . . . . . . . . 10 ⊢ (𝐺 ∈ Mnd → (0_g‘𝐺) ∈ 𝐵)
18	15, 17	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → (0_g‘𝐺) ∈ 𝐵)
19		eqid 2736	. . . . . . . . . . . 12 ⊢ (+_g‘𝐺) = (+_g‘𝐺)
20	7, 19, 16	mndrid 18738	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵) → (𝑥(+_g‘𝐺)(0_g‘𝐺)) = 𝑥)
21	15, 13, 20	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → (𝑥(+_g‘𝐺)(0_g‘𝐺)) = 𝑥)
22	21, 12	eqeltrd 2835	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → (𝑥(+_g‘𝐺)(0_g‘𝐺)) ∈ 𝑢)
23	7, 6, 19	tmdcn2 24032	. . . . . . . . 9 ⊢ (((𝐺 ∈ TopMnd ∧ 𝑢 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝐵 ∧ (0_g‘𝐺) ∈ 𝐵 ∧ (𝑥(+_g‘𝐺)(0_g‘𝐺)) ∈ 𝑢)) → ∃𝑣 ∈ (TopOpen‘𝐺)∃𝑡 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢))
24	4, 5, 13, 18, 22, 23	syl23anc 1379	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → ∃𝑣 ∈ (TopOpen‘𝐺)∃𝑡 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢))
25		r19.29 3102	. . . . . . . . 9 ⊢ ((∀𝑣 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ ∃𝑣 ∈ (TopOpen‘𝐺)∃𝑡 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) → ∃𝑣 ∈ (TopOpen‘𝐺)((𝑥 ∈ 𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ ∃𝑡 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)))
26		simp31 1210	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) → 𝑥 ∈ 𝑣)
27		elfpw 9371	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ↔ (𝑦 ⊆ (𝐴 × 𝐶) ∧ 𝑦 ∈ Fin))
28	27	simplbi 497	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) → 𝑦 ⊆ (𝐴 × 𝐶))
29	28	ad2antrl 728	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣))) → 𝑦 ⊆ (𝐴 × 𝐶))
30		dmss 5887	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ⊆ (𝐴 × 𝐶) → dom 𝑦 ⊆ dom (𝐴 × 𝐶))
31	29, 30	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣))) → dom 𝑦 ⊆ dom (𝐴 × 𝐶))
32		dmxpss 6165	. . . . . . . . . . . . . . . . . . 19 ⊢ dom (𝐴 × 𝐶) ⊆ 𝐴
33	31, 32	sstrdi 3976	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣))) → dom 𝑦 ⊆ 𝐴)
34		elinel2 4182	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) → 𝑦 ∈ Fin)
35	34	ad2antrl 728	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣))) → 𝑦 ∈ Fin)
36		dmfi 9352	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ Fin → dom 𝑦 ∈ Fin)
37	35, 36	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣))) → dom 𝑦 ∈ Fin)
38		elfpw 9371	. . . . . . . . . . . . . . . . . 18 ⊢ (dom 𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↔ (dom 𝑦 ⊆ 𝐴 ∧ dom 𝑦 ∈ Fin))
39	33, 37, 38	sylanbrc 583	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣))) → dom 𝑦 ∈ (𝒫 𝐴 ∩ Fin))
40		eqid 2736	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (._g‘𝐺) = (._g‘𝐺)
41		simpl11 1249	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏))) → 𝜑)
42		tsmsxp.g	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐺 ∈ CMnd)
43	41, 42	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏))) → 𝐺 ∈ CMnd)
44	41, 3	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏))) → 𝐺 ∈ TopMnd)
45		simprrl 780	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏))) → 𝑏 ∈ (𝒫 𝐴 ∩ Fin))
46	45	elin2d 4185	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏))) → 𝑏 ∈ Fin)
47		simpl2r 1228	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏))) → 𝑡 ∈ (TopOpen‘𝐺))
48	44, 14	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏))) → 𝐺 ∈ Mnd)
49	48, 17	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏))) → (0_g‘𝐺) ∈ 𝐵)
50		hashcl 14379	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑏 ∈ Fin → (♯‘𝑏) ∈ ℕ₀)
51	46, 50	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏))) → (♯‘𝑏) ∈ ℕ₀)
52	7, 40, 16	mulgnn0z 19089	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐺 ∈ Mnd ∧ (♯‘𝑏) ∈ ℕ₀) → ((♯‘𝑏)(._g‘𝐺)(0_g‘𝐺)) = (0_g‘𝐺))
53	48, 51, 52	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏))) → ((♯‘𝑏)(._g‘𝐺)(0_g‘𝐺)) = (0_g‘𝐺))
54		simpl32 1256	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏))) → (0_g‘𝐺) ∈ 𝑡)
55	53, 54	eqeltrd 2835	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏))) → ((♯‘𝑏)(._g‘𝐺)(0_g‘𝐺)) ∈ 𝑡)
56	6, 7, 40, 43, 44, 46, 47, 49, 55	tmdgsum2 24039	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏))) → ∃𝑠 ∈ (TopOpen‘𝐺)((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡))
57		simp111 1303	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡))) → 𝜑)
58	57, 42	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡))) → 𝐺 ∈ CMnd)
59	57, 1	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡))) → 𝐺 ∈ TopGrp)
60		tsmsxp.a	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
61	57, 60	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡))) → 𝐴 ∈ 𝑉)
62		tsmsxp.c	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐶 ∈ 𝑊)
63	57, 62	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡))) → 𝐶 ∈ 𝑊)
64		tsmsxp.f	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐹:(𝐴 × 𝐶)⟶𝐵)
65	57, 64	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡))) → 𝐹:(𝐴 × 𝐶)⟶𝐵)
66		tsmsxp.h	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐻:𝐴⟶𝐵)
67	57, 66	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡))) → 𝐻:𝐴⟶𝐵)
68		tsmsxp.1	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝐻‘𝑗) ∈ (𝐺 tsums (𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘))))
69	57, 68	sylan 580	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡))) ∧ 𝑗 ∈ 𝐴) → (𝐻‘𝑗) ∈ (𝐺 tsums (𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘))))
70		eqid 2736	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (-_g‘𝐺) = (-_g‘𝐺)
71		simp3l 1202	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡))) → 𝑠 ∈ (TopOpen‘𝐺))
72		simp3rl 1247	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡))) → (0_g‘𝐺) ∈ 𝑠)
73		simp2rl 1243	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡))) → 𝑏 ∈ (𝒫 𝐴 ∩ Fin))
74		simp2rr 1244	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡))) → dom 𝑦 ⊆ 𝑏)
75		simp2ll 1241	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡))) → 𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin))
76	7, 58, 59, 61, 63, 65, 67, 69, 6, 16, 19, 70, 71, 72, 73, 74, 75	tsmsxplem1 24096	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡))) → ∃𝑛 ∈ (𝒫 𝐶 ∩ Fin)(ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠))
77	43	3adant3 1132	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝐺 ∈ CMnd)
78	59	3adant3r 1182	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝐺 ∈ TopGrp)
79	61	3adant3r 1182	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝐴 ∈ 𝑉)
80	63	3adant3r 1182	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝐶 ∈ 𝑊)
81	65	3adant3r 1182	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝐹:(𝐴 × 𝐶)⟶𝐵)
82	67	3adant3r 1182	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝐻:𝐴⟶𝐵)
83	41	3adant3 1132	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝜑)
84	83, 68	sylan 580	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) ∧ 𝑗 ∈ 𝐴) → (𝐻‘𝑗) ∈ (𝐺 tsums (𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘))))
85		simp3ll 1245	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝑠 ∈ (TopOpen‘𝐺))
86	72	3adant3r 1182	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → (0_g‘𝐺) ∈ 𝑠)
87		simp2rl 1243	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝑏 ∈ (𝒫 𝐴 ∩ Fin))
88		simp133 1311	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)
89		simp3rl 1247	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝑛 ∈ (𝒫 𝐶 ∩ Fin))
90		simp2ll 1241	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin))
91		simp2rr 1244	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → dom 𝑦 ⊆ 𝑏)
92		simp3rr 1248	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠))
93	92	simpld 494	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → ran 𝑦 ⊆ 𝑛)
94		relxp 5677	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ Rel (𝐴 × 𝐶)
95		relss 5765	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑦 ⊆ (𝐴 × 𝐶) → (Rel (𝐴 × 𝐶) → Rel 𝑦))
96	28, 94, 95	mpisyl 21	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) → Rel 𝑦)
97		relssdmrn 6262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (Rel 𝑦 → 𝑦 ⊆ (dom 𝑦 × ran 𝑦))
98	96, 97	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) → 𝑦 ⊆ (dom 𝑦 × ran 𝑦))
99		xpss12 5674	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((dom 𝑦 ⊆ 𝑏 ∧ ran 𝑦 ⊆ 𝑛) → (dom 𝑦 × ran 𝑦) ⊆ (𝑏 × 𝑛))
100	98, 99	sylan9ss 3977	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ (dom 𝑦 ⊆ 𝑏 ∧ ran 𝑦 ⊆ 𝑛)) → 𝑦 ⊆ (𝑏 × 𝑛))
101	90, 91, 93, 100	syl12anc 836	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝑦 ⊆ (𝑏 × 𝑛))
102	92	simprd 495	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)
103		sseq2 3990	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑧 = (𝑏 × 𝑛) → (𝑦 ⊆ 𝑧 ↔ 𝑦 ⊆ (𝑏 × 𝑛)))
104		reseq2 5966	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑧 = (𝑏 × 𝑛) → (𝐹 ↾ 𝑧) = (𝐹 ↾ (𝑏 × 𝑛)))
105	104	oveq2d 7426	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑧 = (𝑏 × 𝑛) → (𝐺 Σ_g (𝐹 ↾ 𝑧)) = (𝐺 Σ_g (𝐹 ↾ (𝑏 × 𝑛))))
106	105	eleq1d 2820	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑧 = (𝑏 × 𝑛) → ((𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣 ↔ (𝐺 Σ_g (𝐹 ↾ (𝑏 × 𝑛))) ∈ 𝑣))
107	103, 106	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑧 = (𝑏 × 𝑛) → ((𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣) ↔ (𝑦 ⊆ (𝑏 × 𝑛) → (𝐺 Σ_g (𝐹 ↾ (𝑏 × 𝑛))) ∈ 𝑣)))
108		simp2lr 1242	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣))
109		elfpw 9371	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝑏 ⊆ 𝐴 ∧ 𝑏 ∈ Fin))
110		elfpw 9371	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ↔ (𝑛 ⊆ 𝐶 ∧ 𝑛 ∈ Fin))
111		xpss12 5674	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑏 ⊆ 𝐴 ∧ 𝑛 ⊆ 𝐶) → (𝑏 × 𝑛) ⊆ (𝐴 × 𝐶))
112		xpfi 9335	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑏 ∈ Fin ∧ 𝑛 ∈ Fin) → (𝑏 × 𝑛) ∈ Fin)
113	111, 112	anim12i 613	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑏 ⊆ 𝐴 ∧ 𝑛 ⊆ 𝐶) ∧ (𝑏 ∈ Fin ∧ 𝑛 ∈ Fin)) → ((𝑏 × 𝑛) ⊆ (𝐴 × 𝐶) ∧ (𝑏 × 𝑛) ∈ Fin))
114	113	an4s 660	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑏 ⊆ 𝐴 ∧ 𝑏 ∈ Fin) ∧ (𝑛 ⊆ 𝐶 ∧ 𝑛 ∈ Fin)) → ((𝑏 × 𝑛) ⊆ (𝐴 × 𝐶) ∧ (𝑏 × 𝑛) ∈ Fin))
115	109, 110, 114	syl2anb 598	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑛 ∈ (𝒫 𝐶 ∩ Fin)) → ((𝑏 × 𝑛) ⊆ (𝐴 × 𝐶) ∧ (𝑏 × 𝑛) ∈ Fin))
116		elfpw 9371	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑏 × 𝑛) ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ↔ ((𝑏 × 𝑛) ⊆ (𝐴 × 𝐶) ∧ (𝑏 × 𝑛) ∈ Fin))
117	115, 116	sylibr 234	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑛 ∈ (𝒫 𝐶 ∩ Fin)) → (𝑏 × 𝑛) ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin))
118	87, 89, 117	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → (𝑏 × 𝑛) ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin))
119	107, 108, 118	rspcdva 3607	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → (𝑦 ⊆ (𝑏 × 𝑛) → (𝐺 Σ_g (𝐹 ↾ (𝑏 × 𝑛))) ∈ 𝑣))
120	101, 119	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → (𝐺 Σ_g (𝐹 ↾ (𝑏 × 𝑛))) ∈ 𝑣)
121		simp3lr 1246	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡))
122	121	simprd 495	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)
123		oveq2 7418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑔 = ℎ → (𝐺 Σ_g 𝑔) = (𝐺 Σ_g ℎ))
124	123	eleq1d 2820	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑔 = ℎ → ((𝐺 Σ_g 𝑔) ∈ 𝑡 ↔ (𝐺 Σ_g ℎ) ∈ 𝑡))
125	124	cbvralvw 3224	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡 ↔ ∀ℎ ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g ℎ) ∈ 𝑡)
126	122, 125	sylib 218	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → ∀ℎ ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g ℎ) ∈ 𝑡)
127	7, 77, 78, 79, 80, 81, 82, 84, 6, 16, 19, 70, 85, 86, 87, 88, 89, 101, 102, 120, 126	tsmsxplem2 24097	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢)
128	127	3exp 1119	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) → (((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) → (((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠))) → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢)))
129	128	exp4a 431	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) → (((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) → ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) → ((𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)) → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢))))
130	129	3imp1 1348	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡))) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠))) → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢)
131	76, 130	rexlimddv 3148	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡))) → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢)
132	131	3expa 1118	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏))) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡))) → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢)
133	56, 132	rexlimddv 3148	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏))) → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢)
134	133	anassrs 467	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣))) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢)
135	134	expr 456	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣))) ∧ 𝑏 ∈ (𝒫 𝐴 ∩ Fin)) → (dom 𝑦 ⊆ 𝑏 → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢))
136	135	ralrimiva 3133	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣))) → ∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(dom 𝑦 ⊆ 𝑏 → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢))
137		sseq1 3989	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = dom 𝑦 → (𝑎 ⊆ 𝑏 ↔ dom 𝑦 ⊆ 𝑏))
138	137	rspceaimv 3612	. . . . . . . . . . . . . . . . 17 ⊢ ((dom 𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ ∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(dom 𝑦 ⊆ 𝑏 → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢))
139	39, 136, 138	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣))) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢))
140	139	rexlimdvaa 3143	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) → (∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢)))
141	26, 140	embantd 59	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) → ((𝑥 ∈ 𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢)))
142	141	3expia 1121	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺))) → ((𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢) → ((𝑥 ∈ 𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢))))
143	142	anassrs 467	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ 𝑣 ∈ (TopOpen‘𝐺)) ∧ 𝑡 ∈ (TopOpen‘𝐺)) → ((𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢) → ((𝑥 ∈ 𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢))))
144	143	rexlimdva 3142	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ 𝑣 ∈ (TopOpen‘𝐺)) → (∃𝑡 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢) → ((𝑥 ∈ 𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢))))
145	144	impcomd 411	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ 𝑣 ∈ (TopOpen‘𝐺)) → (((𝑥 ∈ 𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ ∃𝑡 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢)))
146	145	rexlimdva 3142	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → (∃𝑣 ∈ (TopOpen‘𝐺)((𝑥 ∈ 𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ ∃𝑡 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢)))
147	25, 146	syl5 34	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → ((∀𝑣 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ ∃𝑣 ∈ (TopOpen‘𝐺)∃𝑡 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢)))
148	24, 147	mpan2d 694	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → (∀𝑣 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢)))
149	148	3expia 1121	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺)) → (𝑥 ∈ 𝑢 → (∀𝑣 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢))))
150	149	com23 86	. . . . 5 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺)) → (∀𝑣 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) → (𝑥 ∈ 𝑢 → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢))))
151	150	ralrimdva 3141	. . . 4 ⊢ (𝜑 → (∀𝑣 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) → ∀𝑢 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑢 → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢))))
152	151	anim2d 612	. . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐵 ∧ ∀𝑣 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣))) → (𝑥 ∈ 𝐵 ∧ ∀𝑢 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑢 → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢)))))
153		eqid 2736	. . . 4 ⊢ (𝒫 (𝐴 × 𝐶) ∩ Fin) = (𝒫 (𝐴 × 𝐶) ∩ Fin)
154		tgptps 24023	. . . . 5 ⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ TopSp)
155	1, 154	syl 17	. . . 4 ⊢ (𝜑 → 𝐺 ∈ TopSp)
156	60, 62	xpexd 7750	. . . 4 ⊢ (𝜑 → (𝐴 × 𝐶) ∈ V)
157	7, 6, 153, 42, 155, 156, 64	eltsms 24076	. . 3 ⊢ (𝜑 → (𝑥 ∈ (𝐺 tsums 𝐹) ↔ (𝑥 ∈ 𝐵 ∧ ∀𝑣 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)))))
158		eqid 2736	. . . 4 ⊢ (𝒫 𝐴 ∩ Fin) = (𝒫 𝐴 ∩ Fin)
159	7, 6, 158, 42, 155, 60, 66	eltsms 24076	. . 3 ⊢ (𝜑 → (𝑥 ∈ (𝐺 tsums 𝐻) ↔ (𝑥 ∈ 𝐵 ∧ ∀𝑢 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑢 → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢)))))
160	152, 157, 159	3imtr4d 294	. 2 ⊢ (𝜑 → (𝑥 ∈ (𝐺 tsums 𝐹) → 𝑥 ∈ (𝐺 tsums 𝐻)))
161	160	ssrdv 3969	1 ⊢ (𝜑 → (𝐺 tsums 𝐹) ⊆ (𝐺 tsums 𝐻))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ∀wral 3052 ∃wrex 3061 Vcvv 3464 ∩ cin 3930 ⊆ wss 3931 𝒫 cpw 4580 {csn 4606 ↦ cmpt 5206 × cxp 5657 dom cdm 5659 ran crn 5660 ↾ cres 5661 Rel wrel 5664 ⟶wf 6532 ‘cfv 6536 (class class class)co 7410 ↑_m cmap 8845 Fincfn 8964 ℕ₀cn0 12506 ♯chash 14353 Basecbs 17233 +_gcplusg 17276 TopOpenctopn 17440 0_gc0g 17458 Σ_g cgsu 17459 Mndcmnd 18717 -_gcsg 18923 ._gcmg 19055 CMndccmn 19766 TopOnctopon 22853 TopSpctps 22875 TopMndctmd 24013 TopGrpctgp 24014 tsums ctsu 24069

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2708 ax-rep 5254 ax-sep 5271 ax-nul 5281 ax-pow 5340 ax-pr 5407 ax-un 7734 ax-cnex 11190 ax-resscn 11191 ax-1cn 11192 ax-icn 11193 ax-addcl 11194 ax-addrcl 11195 ax-mulcl 11196 ax-mulrcl 11197 ax-mulcom 11198 ax-addass 11199 ax-mulass 11200 ax-distr 11201 ax-i2m1 11202 ax-1ne0 11203 ax-1rid 11204 ax-rnegex 11205 ax-rrecex 11206 ax-cnre 11207 ax-pre-lttri 11208 ax-pre-lttrn 11209 ax-pre-ltadd 11210 ax-pre-mulgt0 11211

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2810 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3062 df-rmo 3364 df-reu 3365 df-rab 3421 df-v 3466 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-pss 3951 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-op 4613 df-uni 4889 df-int 4928 df-iun 4974 df-iin 4975 df-br 5125 df-opab 5187 df-mpt 5207 df-tr 5235 df-id 5553 df-eprel 5558 df-po 5566 df-so 5567 df-fr 5611 df-se 5612 df-we 5613 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6295 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-isom 6545 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-of 7676 df-om 7867 df-1st 7993 df-2nd 7994 df-supp 8165 df-frecs 8285 df-wrecs 8316 df-recs 8390 df-rdg 8429 df-1o 8485 df-2o 8486 df-er 8724 df-map 8847 df-ixp 8917 df-en 8965 df-dom 8966 df-sdom 8967 df-fin 8968 df-fsupp 9379 df-fi 9428 df-oi 9529 df-card 9958 df-pnf 11276 df-mnf 11277 df-xr 11278 df-ltxr 11279 df-le 11280 df-sub 11473 df-neg 11474 df-nn 12246 df-2 12308 df-n0 12507 df-z 12594 df-uz 12858 df-fz 13530 df-fzo 13677 df-seq 14025 df-hash 14354 df-sets 17188 df-slot 17206 df-ndx 17218 df-base 17234 df-ress 17257 df-plusg 17289 df-rest 17441 df-0g 17460 df-gsum 17461 df-topgen 17462 df-pt 17463 df-mre 17603 df-mrc 17604 df-acs 17606 df-plusf 18622 df-mgm 18623 df-sgrp 18702 df-mnd 18718 df-mhm 18766 df-submnd 18767 df-grp 18924 df-minusg 18925 df-sbg 18926 df-mulg 19056 df-ghm 19201 df-cntz 19305 df-cmn 19768 df-abl 19769 df-fbas 21317 df-fg 21318 df-top 22837 df-topon 22854 df-topsp 22876 df-bases 22889 df-ntr 22963 df-nei 23041 df-cn 23170 df-cnp 23171 df-cmp 23330 df-tx 23505 df-xko 23506 df-hmeo 23698 df-fil 23789 df-fm 23881 df-flim 23882 df-flf 23883 df-tmd 24015 df-tgp 24016 df-tsms 24070

This theorem is referenced by: (None)

W3C validator