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 23304

Description: Write a sum over a two-dimensional region as a double sum. This infinite group sum version of gsumxp 19575 is also known as Fubini's theorem. The converse is not necessarily true without additional assumptions. See tsmsxplem1 23302 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 23228	. . . . . . . . . . 11 ⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ TopMnd)
3	1, 2	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺 ∈ TopMnd)
4	3	3ad2ant1 1132	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → 𝐺 ∈ TopMnd)
5		simp2 1136	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → 𝑢 ∈ (TopOpen‘𝐺))
6		eqid 2738	. . . . . . . . . . . . 13 ⊢ (TopOpen‘𝐺) = (TopOpen‘𝐺)
7		tsmsxp.b	. . . . . . . . . . . . 13 ⊢ 𝐵 = (Base‘𝐺)
8	6, 7	tmdtopon 23230	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ TopMnd → (TopOpen‘𝐺) ∈ (TopOn‘𝐵))
9	4, 8	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → (TopOpen‘𝐺) ∈ (TopOn‘𝐵))
10		toponss 22074	. . . . . . . . . . 11 ⊢ (((TopOpen‘𝐺) ∈ (TopOn‘𝐵) ∧ 𝑢 ∈ (TopOpen‘𝐺)) → 𝑢 ⊆ 𝐵)
11	9, 5, 10	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → 𝑢 ⊆ 𝐵)
12		simp3 1137	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → 𝑥 ∈ 𝑢)
13	11, 12	sseldd 3923	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → 𝑥 ∈ 𝐵)
14		tmdmnd 23224	. . . . . . . . . . 11 ⊢ (𝐺 ∈ TopMnd → 𝐺 ∈ Mnd)
15	4, 14	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → 𝐺 ∈ Mnd)
16		eqid 2738	. . . . . . . . . . 11 ⊢ (0_g‘𝐺) = (0_g‘𝐺)
17	7, 16	mndidcl 18398	. . . . . . . . . 10 ⊢ (𝐺 ∈ Mnd → (0_g‘𝐺) ∈ 𝐵)
18	15, 17	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → (0_g‘𝐺) ∈ 𝐵)
19		eqid 2738	. . . . . . . . . . . 12 ⊢ (+_g‘𝐺) = (+_g‘𝐺)
20	7, 19, 16	mndrid 18404	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵) → (𝑥(+_g‘𝐺)(0_g‘𝐺)) = 𝑥)
21	15, 13, 20	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → (𝑥(+_g‘𝐺)(0_g‘𝐺)) = 𝑥)
22	21, 12	eqeltrd 2839	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → (𝑥(+_g‘𝐺)(0_g‘𝐺)) ∈ 𝑢)
23	7, 6, 19	tmdcn2 23238	. . . . . . . . 9 ⊢ (((𝐺 ∈ TopMnd ∧ 𝑢 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝐵 ∧ (0_g‘𝐺) ∈ 𝐵 ∧ (𝑥(+_g‘𝐺)(0_g‘𝐺)) ∈ 𝑢)) → ∃𝑣 ∈ (TopOpen‘𝐺)∃𝑡 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢))
24	4, 5, 13, 18, 22, 23	syl23anc 1376	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → ∃𝑣 ∈ (TopOpen‘𝐺)∃𝑡 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢))
25		r19.29 3183	. . . . . . . . 9 ⊢ ((∀𝑣 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ ∃𝑣 ∈ (TopOpen‘𝐺)∃𝑡 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) → ∃𝑣 ∈ (TopOpen‘𝐺)((𝑥 ∈ 𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ ∃𝑡 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)))
26		simp31 1208	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) → 𝑥 ∈ 𝑣)
27		elfpw 9119	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ↔ (𝑦 ⊆ (𝐴 × 𝐶) ∧ 𝑦 ∈ Fin))
28	27	simplbi 498	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) → 𝑦 ⊆ (𝐴 × 𝐶))
29	28	ad2antrl 725	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣))) → 𝑦 ⊆ (𝐴 × 𝐶))
30		dmss 5813	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ⊆ (𝐴 × 𝐶) → dom 𝑦 ⊆ dom (𝐴 × 𝐶))
31	29, 30	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣))) → dom 𝑦 ⊆ dom (𝐴 × 𝐶))
32		dmxpss 6076	. . . . . . . . . . . . . . . . . . 19 ⊢ dom (𝐴 × 𝐶) ⊆ 𝐴
33	31, 32	sstrdi 3934	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣))) → dom 𝑦 ⊆ 𝐴)
34		elinel2 4131	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) → 𝑦 ∈ Fin)
35	34	ad2antrl 725	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣))) → 𝑦 ∈ Fin)
36		dmfi 9095	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ Fin → dom 𝑦 ∈ Fin)
37	35, 36	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣))) → dom 𝑦 ∈ Fin)
38		elfpw 9119	. . . . . . . . . . . . . . . . . 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 2738	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (._g‘𝐺) = (._g‘𝐺)
41		simpl11 1247	. . . . . . . . . . . . . . . . . . . . . . 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 778	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏))) → 𝑏 ∈ (𝒫 𝐴 ∩ Fin))
46	45	elin2d 4134	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏))) → 𝑏 ∈ Fin)
47		simpl2r 1226	. . . . . . . . . . . . . . . . . . . . . 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 14069	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑏 ∈ Fin → (♯‘𝑏) ∈ ℕ₀)
51	46, 50	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏))) → (♯‘𝑏) ∈ ℕ₀)
52	7, 40, 16	mulgnn0z 18728	. . . . . . . . . . . . . . . . . . . . . . . 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 1254	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏))) → (0_g‘𝐺) ∈ 𝑡)
55	53, 54	eqeltrd 2839	. . . . . . . . . . . . . . . . . . . . . 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 23245	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏))) → ∃𝑠 ∈ (TopOpen‘𝐺)((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡))
57		simp111 1301	. . . . . . . . . . . . . . . . . . . . . . . . 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 2738	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (-_g‘𝐺) = (-_g‘𝐺)
71		simp3l 1200	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡))) → 𝑠 ∈ (TopOpen‘𝐺))
72		simp3rl 1245	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡))) → (0_g‘𝐺) ∈ 𝑠)
73		simp2rl 1241	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡))) → 𝑏 ∈ (𝒫 𝐴 ∩ Fin))
74		simp2rr 1242	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡))) → dom 𝑦 ⊆ 𝑏)
75		simp2ll 1239	. . . . . . . . . . . . . . . . . . . . . . . 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 23302	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡))) → ∃𝑛 ∈ (𝒫 𝐶 ∩ Fin)(ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠))
77	43	3adant3 1131	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 1180	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 1180	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝐴 ∈ 𝑉)
80	63	3adant3r 1180	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝐶 ∈ 𝑊)
81	65	3adant3r 1180	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝐹:(𝐴 × 𝐶)⟶𝐵)
82	67	3adant3r 1180	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝐻:𝐴⟶𝐵)
83	41	3adant3 1131	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1243	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 1180	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 1241	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝑏 ∈ (𝒫 𝐴 ∩ Fin))
88		simp133 1309	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)
89		simp3rl 1245	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝑛 ∈ (𝒫 𝐶 ∩ Fin))
90		simp2ll 1239	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin))
91		simp2rr 1242	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → dom 𝑦 ⊆ 𝑏)
92		simp3rr 1246	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 495	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → ran 𝑦 ⊆ 𝑛)
94		relxp 5609	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ Rel (𝐴 × 𝐶)
95		relss 5694	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑦 ⊆ (𝐴 × 𝐶) → (Rel (𝐴 × 𝐶) → Rel 𝑦))
96	28, 94, 95	mpisyl 21	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) → Rel 𝑦)
97		relssdmrn 6174	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (Rel 𝑦 → 𝑦 ⊆ (dom 𝑦 × ran 𝑦))
98	96, 97	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) → 𝑦 ⊆ (dom 𝑦 × ran 𝑦))
99		xpss12 5606	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((dom 𝑦 ⊆ 𝑏 ∧ ran 𝑦 ⊆ 𝑛) → (dom 𝑦 × ran 𝑦) ⊆ (𝑏 × 𝑛))
100	98, 99	sylan9ss 3935	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ (dom 𝑦 ⊆ 𝑏 ∧ ran 𝑦 ⊆ 𝑛)) → 𝑦 ⊆ (𝑏 × 𝑛))
101	90, 91, 93, 100	syl12anc 834	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝑦 ⊆ (𝑏 × 𝑛))
102	92	simprd 496	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 3948	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑧 = (𝑏 × 𝑛) → (𝑦 ⊆ 𝑧 ↔ 𝑦 ⊆ (𝑏 × 𝑛)))
104		reseq2 5888	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑧 = (𝑏 × 𝑛) → (𝐹 ↾ 𝑧) = (𝐹 ↾ (𝑏 × 𝑛)))
105	104	oveq2d 7293	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑧 = (𝑏 × 𝑛) → (𝐺 Σ_g (𝐹 ↾ 𝑧)) = (𝐺 Σ_g (𝐹 ↾ (𝑏 × 𝑛))))
106	105	eleq1d 2823	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑧 = (𝑏 × 𝑛) → ((𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣 ↔ (𝐺 Σ_g (𝐹 ↾ (𝑏 × 𝑛))) ∈ 𝑣))
107	103, 106	imbi12d 345	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑧 = (𝑏 × 𝑛) → ((𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣) ↔ (𝑦 ⊆ (𝑏 × 𝑛) → (𝐺 Σ_g (𝐹 ↾ (𝑏 × 𝑛))) ∈ 𝑣)))
108		simp2lr 1240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9119	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝑏 ⊆ 𝐴 ∧ 𝑏 ∈ Fin))
110		elfpw 9119	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ↔ (𝑛 ⊆ 𝐶 ∧ 𝑛 ∈ Fin))
111		xpss12 5606	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑏 ⊆ 𝐴 ∧ 𝑛 ⊆ 𝐶) → (𝑏 × 𝑛) ⊆ (𝐴 × 𝐶))
112		xpfi 9083	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑏 ∈ Fin ∧ 𝑛 ∈ Fin) → (𝑏 × 𝑛) ∈ Fin)
113	111, 112	anim12i 613	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑏 ⊆ 𝐴 ∧ 𝑛 ⊆ 𝐶) ∧ (𝑏 ∈ Fin ∧ 𝑛 ∈ Fin)) → ((𝑏 × 𝑛) ⊆ (𝐴 × 𝐶) ∧ (𝑏 × 𝑛) ∈ Fin))
114	113	an4s 657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑏 ⊆ 𝐴 ∧ 𝑏 ∈ Fin) ∧ (𝑛 ⊆ 𝐶 ∧ 𝑛 ∈ Fin)) → ((𝑏 × 𝑛) ⊆ (𝐴 × 𝐶) ∧ (𝑏 × 𝑛) ∈ Fin))
115	109, 110, 114	syl2anb 598	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑛 ∈ (𝒫 𝐶 ∩ Fin)) → ((𝑏 × 𝑛) ⊆ (𝐴 × 𝐶) ∧ (𝑏 × 𝑛) ∈ Fin))
116		elfpw 9119	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑏 × 𝑛) ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ↔ ((𝑏 × 𝑛) ⊆ (𝐴 × 𝐶) ∧ (𝑏 × 𝑛) ∈ Fin))
117	115, 116	sylibr 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3563	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1244	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 496	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7285	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑔 = ℎ → (𝐺 Σ_g 𝑔) = (𝐺 Σ_g ℎ))
124	123	eleq1d 2823	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑔 = ℎ → ((𝐺 Σ_g 𝑔) ∈ 𝑡 ↔ (𝐺 Σ_g ℎ) ∈ 𝑡))
125	124	cbvralvw 3382	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡 ↔ ∀ℎ ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g ℎ) ∈ 𝑡)
126	122, 125	sylib 217	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 23303	. . . . . . . . . . . . . . . . . . . . . . . . . 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 1118	. . . . . . . . . . . . . . . . . . . . . . . . 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 432	. . . . . . . . . . . . . . . . . . . . . . . 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 1346	. . . . . . . . . . . . . . . . . . . . . . 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 3219	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡))) → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢)
132	131	3expa 1117	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏))) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡))) → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢)
133	56, 132	rexlimddv 3219	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏))) → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢)
134	133	anassrs 468	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣))) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢)
135	134	expr 457	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣))) ∧ 𝑏 ∈ (𝒫 𝐴 ∩ Fin)) → (dom 𝑦 ⊆ 𝑏 → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢))
136	135	ralrimiva 3103	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣))) → ∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(dom 𝑦 ⊆ 𝑏 → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢))
137		sseq1 3947	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = dom 𝑦 → (𝑎 ⊆ 𝑏 ↔ dom 𝑦 ⊆ 𝑏))
138	137	rspceaimv 3566	. . . . . . . . . . . . . . . . 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 3213	. . . . . . . . . . . . . . 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 1120	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺))) → ((𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢) → ((𝑥 ∈ 𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢))))
143	142	anassrs 468	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ 𝑣 ∈ (TopOpen‘𝐺)) ∧ 𝑡 ∈ (TopOpen‘𝐺)) → ((𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢) → ((𝑥 ∈ 𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢))))
144	143	rexlimdva 3212	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ 𝑣 ∈ (TopOpen‘𝐺)) → (∃𝑡 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢) → ((𝑥 ∈ 𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢))))
145	144	impcomd 412	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ 𝑣 ∈ (TopOpen‘𝐺)) → (((𝑥 ∈ 𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ ∃𝑡 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢)))
146	145	rexlimdva 3212	. . . . . . . . 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 691	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → (∀𝑣 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢)))
149	148	3expia 1120	. . . . . 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 3106	. . . 4 ⊢ (𝜑 → (∀𝑣 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) → ∀𝑢 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑢 → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢))))
152	151	anim2d 612	. . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐵 ∧ ∀𝑣 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣))) → (𝑥 ∈ 𝐵 ∧ ∀𝑢 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑢 → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢)))))
153		eqid 2738	. . . 4 ⊢ (𝒫 (𝐴 × 𝐶) ∩ Fin) = (𝒫 (𝐴 × 𝐶) ∩ Fin)
154		tgptps 23229	. . . . 5 ⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ TopSp)
155	1, 154	syl 17	. . . 4 ⊢ (𝜑 → 𝐺 ∈ TopSp)
156	60, 62	xpexd 7601	. . . 4 ⊢ (𝜑 → (𝐴 × 𝐶) ∈ V)
157	7, 6, 153, 42, 155, 156, 64	eltsms 23282	. . 3 ⊢ (𝜑 → (𝑥 ∈ (𝐺 tsums 𝐹) ↔ (𝑥 ∈ 𝐵 ∧ ∀𝑣 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)))))
158		eqid 2738	. . . 4 ⊢ (𝒫 𝐴 ∩ Fin) = (𝒫 𝐴 ∩ Fin)
159	7, 6, 158, 42, 155, 60, 66	eltsms 23282	. . 3 ⊢ (𝜑 → (𝑥 ∈ (𝐺 tsums 𝐻) ↔ (𝑥 ∈ 𝐵 ∧ ∀𝑢 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑢 → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢)))))
160	152, 157, 159	3imtr4d 294	. 2 ⊢ (𝜑 → (𝑥 ∈ (𝐺 tsums 𝐹) → 𝑥 ∈ (𝐺 tsums 𝐻)))
161	160	ssrdv 3928	1 ⊢ (𝜑 → (𝐺 tsums 𝐹) ⊆ (𝐺 tsums 𝐻))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1086 = wceq 1539 ∈ wcel 2106 ∀wral 3064 ∃wrex 3065 Vcvv 3431 ∩ cin 3887 ⊆ wss 3888 𝒫 cpw 4535 {csn 4563 ↦ cmpt 5159 × cxp 5589 dom cdm 5591 ran crn 5592 ↾ cres 5593 Rel wrel 5596 ⟶wf 6431 ‘cfv 6435 (class class class)co 7277 ↑_m cmap 8613 Fincfn 8731 ℕ₀cn0 12231 ♯chash 14042 Basecbs 16910 +_gcplusg 16960 TopOpenctopn 17130 0_gc0g 17148 Σ_g cgsu 17149 Mndcmnd 18383 -_gcsg 18577 ._gcmg 18698 CMndccmn 19384 TopOnctopon 22057 TopSpctps 22079 TopMndctmd 23219 TopGrpctgp 23220 tsums ctsu 23275

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 5211 ax-sep 5225 ax-nul 5232 ax-pow 5290 ax-pr 5354 ax-un 7588 ax-cnex 10925 ax-resscn 10926 ax-1cn 10927 ax-icn 10928 ax-addcl 10929 ax-addrcl 10930 ax-mulcl 10931 ax-mulrcl 10932 ax-mulcom 10933 ax-addass 10934 ax-mulass 10935 ax-distr 10936 ax-i2m1 10937 ax-1ne0 10938 ax-1rid 10939 ax-rnegex 10940 ax-rrecex 10941 ax-cnre 10942 ax-pre-lttri 10943 ax-pre-lttrn 10944 ax-pre-ltadd 10945 ax-pre-mulgt0 10946

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 3433 df-sbc 3718 df-csb 3834 df-dif 3891 df-un 3893 df-in 3895 df-ss 3905 df-pss 3907 df-nul 4259 df-if 4462 df-pw 4537 df-sn 4564 df-pr 4566 df-op 4570 df-uni 4842 df-int 4882 df-iun 4928 df-iin 4929 df-br 5077 df-opab 5139 df-mpt 5160 df-tr 5194 df-id 5491 df-eprel 5497 df-po 5505 df-so 5506 df-fr 5546 df-se 5547 df-we 5548 df-xp 5597 df-rel 5598 df-cnv 5599 df-co 5600 df-dm 5601 df-rn 5602 df-res 5603 df-ima 5604 df-pred 6204 df-ord 6271 df-on 6272 df-lim 6273 df-suc 6274 df-iota 6393 df-fun 6437 df-fn 6438 df-f 6439 df-f1 6440 df-fo 6441 df-f1o 6442 df-fv 6443 df-isom 6444 df-riota 7234 df-ov 7280 df-oprab 7281 df-mpo 7282 df-of 7533 df-om 7713 df-1st 7831 df-2nd 7832 df-supp 7976 df-frecs 8095 df-wrecs 8126 df-recs 8200 df-rdg 8239 df-1o 8295 df-er 8496 df-map 8615 df-ixp 8684 df-en 8732 df-dom 8733 df-sdom 8734 df-fin 8735 df-fsupp 9127 df-fi 9168 df-oi 9267 df-card 9695 df-pnf 11009 df-mnf 11010 df-xr 11011 df-ltxr 11012 df-le 11013 df-sub 11205 df-neg 11206 df-nn 11972 df-2 12034 df-n0 12232 df-z 12318 df-uz 12581 df-fz 13238 df-fzo 13381 df-seq 13720 df-hash 14043 df-sets 16863 df-slot 16881 df-ndx 16893 df-base 16911 df-ress 16940 df-plusg 16973 df-rest 17131 df-0g 17150 df-gsum 17151 df-topgen 17152 df-pt 17153 df-mre 17293 df-mrc 17294 df-acs 17296 df-plusf 18323 df-mgm 18324 df-sgrp 18373 df-mnd 18384 df-mhm 18428 df-submnd 18429 df-grp 18578 df-minusg 18579 df-sbg 18580 df-mulg 18699 df-ghm 18830 df-cntz 18921 df-cmn 19386 df-abl 19387 df-fbas 20592 df-fg 20593 df-top 22041 df-topon 22058 df-topsp 22080 df-bases 22094 df-ntr 22169 df-nei 22247 df-cn 22376 df-cnp 22377 df-cmp 22536 df-tx 22711 df-xko 22712 df-hmeo 22904 df-fil 22995 df-fm 23087 df-flim 23088 df-flf 23089 df-tmd 23221 df-tgp 23222 df-tsms 23276

This theorem is referenced by: (None)

W3C validator