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 24058

Description: Write a sum over a two-dimensional region as a double sum. This infinite group sum version of gsumxp 19873 is also known as Fubini's theorem. The converse is not necessarily true without additional assumptions. See tsmsxplem1 24056 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 23982	. . . . . . . . . . 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 2729	. . . . . . . . . . . . 13 ⊢ (TopOpen‘𝐺) = (TopOpen‘𝐺)
7		tsmsxp.b	. . . . . . . . . . . . 13 ⊢ 𝐵 = (Base‘𝐺)
8	6, 7	tmdtopon 23984	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ TopMnd → (TopOpen‘𝐺) ∈ (TopOn‘𝐵))
9	4, 8	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → (TopOpen‘𝐺) ∈ (TopOn‘𝐵))
10		toponss 22830	. . . . . . . . . . 11 ⊢ (((TopOpen‘𝐺) ∈ (TopOn‘𝐵) ∧ 𝑢 ∈ (TopOpen‘𝐺)) → 𝑢 ⊆ 𝐵)
11	9, 5, 10	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → 𝑢 ⊆ 𝐵)
12		simp3 1138	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → 𝑥 ∈ 𝑢)
13	11, 12	sseldd 3938	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → 𝑥 ∈ 𝐵)
14		tmdmnd 23978	. . . . . . . . . . 11 ⊢ (𝐺 ∈ TopMnd → 𝐺 ∈ Mnd)
15	4, 14	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → 𝐺 ∈ Mnd)
16		eqid 2729	. . . . . . . . . . 11 ⊢ (0_g‘𝐺) = (0_g‘𝐺)
17	7, 16	mndidcl 18641	. . . . . . . . . 10 ⊢ (𝐺 ∈ Mnd → (0_g‘𝐺) ∈ 𝐵)
18	15, 17	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → (0_g‘𝐺) ∈ 𝐵)
19		eqid 2729	. . . . . . . . . . . 12 ⊢ (+_g‘𝐺) = (+_g‘𝐺)
20	7, 19, 16	mndrid 18647	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵) → (𝑥(+_g‘𝐺)(0_g‘𝐺)) = 𝑥)
21	15, 13, 20	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → (𝑥(+_g‘𝐺)(0_g‘𝐺)) = 𝑥)
22	21, 12	eqeltrd 2828	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → (𝑥(+_g‘𝐺)(0_g‘𝐺)) ∈ 𝑢)
23	7, 6, 19	tmdcn2 23992	. . . . . . . . 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 3092	. . . . . . . . 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 9263	. . . . . . . . . . . . . . . . . . . . . 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 5849	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ⊆ (𝐴 × 𝐶) → dom 𝑦 ⊆ dom (𝐴 × 𝐶))
31	29, 30	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣))) → dom 𝑦 ⊆ dom (𝐴 × 𝐶))
32		dmxpss 6124	. . . . . . . . . . . . . . . . . . 19 ⊢ dom (𝐴 × 𝐶) ⊆ 𝐴
33	31, 32	sstrdi 3950	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣))) → dom 𝑦 ⊆ 𝐴)
34		elinel2 4155	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) → 𝑦 ∈ Fin)
35	34	ad2antrl 728	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣))) → 𝑦 ∈ Fin)
36		dmfi 9244	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ Fin → dom 𝑦 ∈ Fin)
37	35, 36	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣))) → dom 𝑦 ∈ Fin)
38		elfpw 9263	. . . . . . . . . . . . . . . . . 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 2729	. . . . . . . . . . . . . . . . . . . . . 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 4158	. . . . . . . . . . . . . . . . . . . . . 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 14281	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑏 ∈ Fin → (♯‘𝑏) ∈ ℕ₀)
51	46, 50	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏))) → (♯‘𝑏) ∈ ℕ₀)
52	7, 40, 16	mulgnn0z 18998	. . . . . . . . . . . . . . . . . . . . . . . 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 2828	. . . . . . . . . . . . . . . . . . . . . 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 23999	. . . . . . . . . . . . . . . . . . . . 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 2729	. . . . . . . . . . . . . . . . . . . . . . . 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 24056	. . . . . . . . . . . . . . . . . . . . . . 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 5641	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ Rel (𝐴 × 𝐶)
95		relss 5729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑦 ⊆ (𝐴 × 𝐶) → (Rel (𝐴 × 𝐶) → Rel 𝑦))
96	28, 94, 95	mpisyl 21	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) → Rel 𝑦)
97		relssdmrn 6221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (Rel 𝑦 → 𝑦 ⊆ (dom 𝑦 × ran 𝑦))
98	96, 97	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) → 𝑦 ⊆ (dom 𝑦 × ran 𝑦))
99		xpss12 5638	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((dom 𝑦 ⊆ 𝑏 ∧ ran 𝑦 ⊆ 𝑛) → (dom 𝑦 × ran 𝑦) ⊆ (𝑏 × 𝑛))
100	98, 99	sylan9ss 3951	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3964	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑧 = (𝑏 × 𝑛) → (𝑦 ⊆ 𝑧 ↔ 𝑦 ⊆ (𝑏 × 𝑛)))
104		reseq2 5929	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑧 = (𝑏 × 𝑛) → (𝐹 ↾ 𝑧) = (𝐹 ↾ (𝑏 × 𝑛)))
105	104	oveq2d 7369	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑧 = (𝑏 × 𝑛) → (𝐺 Σ_g (𝐹 ↾ 𝑧)) = (𝐺 Σ_g (𝐹 ↾ (𝑏 × 𝑛))))
106	105	eleq1d 2813	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9263	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝑏 ⊆ 𝐴 ∧ 𝑏 ∈ Fin))
110		elfpw 9263	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ↔ (𝑛 ⊆ 𝐶 ∧ 𝑛 ∈ Fin))
111		xpss12 5638	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑏 ⊆ 𝐴 ∧ 𝑛 ⊆ 𝐶) → (𝑏 × 𝑛) ⊆ (𝐴 × 𝐶))
112		xpfi 9227	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9263	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3580	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7361	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑔 = ℎ → (𝐺 Σ_g 𝑔) = (𝐺 Σ_g ℎ))
124	123	eleq1d 2813	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑔 = ℎ → ((𝐺 Σ_g 𝑔) ∈ 𝑡 ↔ (𝐺 Σ_g ℎ) ∈ 𝑡))
125	124	cbvralvw 3207	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 24057	. . . . . . . . . . . . . . . . . . . . . . . . . 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 3136	. . . . . . . . . . . . . . . . . . . . . 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 3136	. . . . . . . . . . . . . . . . . . . 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 3121	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣))) → ∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(dom 𝑦 ⊆ 𝑏 → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢))
137		sseq1 3963	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = dom 𝑦 → (𝑎 ⊆ 𝑏 ↔ dom 𝑦 ⊆ 𝑏))
138	137	rspceaimv 3585	. . . . . . . . . . . . . . . . 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 3131	. . . . . . . . . . . . . . 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 3130	. . . . . . . . . . 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 3130	. . . . . . . . 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 3129	. . . 4 ⊢ (𝜑 → (∀𝑣 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) → ∀𝑢 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑢 → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢))))
152	151	anim2d 612	. . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐵 ∧ ∀𝑣 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣))) → (𝑥 ∈ 𝐵 ∧ ∀𝑢 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑢 → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢)))))
153		eqid 2729	. . . 4 ⊢ (𝒫 (𝐴 × 𝐶) ∩ Fin) = (𝒫 (𝐴 × 𝐶) ∩ Fin)
154		tgptps 23983	. . . . 5 ⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ TopSp)
155	1, 154	syl 17	. . . 4 ⊢ (𝜑 → 𝐺 ∈ TopSp)
156	60, 62	xpexd 7691	. . . 4 ⊢ (𝜑 → (𝐴 × 𝐶) ∈ V)
157	7, 6, 153, 42, 155, 156, 64	eltsms 24036	. . 3 ⊢ (𝜑 → (𝑥 ∈ (𝐺 tsums 𝐹) ↔ (𝑥 ∈ 𝐵 ∧ ∀𝑣 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)))))
158		eqid 2729	. . . 4 ⊢ (𝒫 𝐴 ∩ Fin) = (𝒫 𝐴 ∩ Fin)
159	7, 6, 158, 42, 155, 60, 66	eltsms 24036	. . 3 ⊢ (𝜑 → (𝑥 ∈ (𝐺 tsums 𝐻) ↔ (𝑥 ∈ 𝐵 ∧ ∀𝑢 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑢 → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢)))))
160	152, 157, 159	3imtr4d 294	. 2 ⊢ (𝜑 → (𝑥 ∈ (𝐺 tsums 𝐹) → 𝑥 ∈ (𝐺 tsums 𝐻)))
161	160	ssrdv 3943	1 ⊢ (𝜑 → (𝐺 tsums 𝐹) ⊆ (𝐺 tsums 𝐻))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ∀wral 3044 ∃wrex 3053 Vcvv 3438 ∩ cin 3904 ⊆ wss 3905 𝒫 cpw 4553 {csn 4579 ↦ cmpt 5176 × cxp 5621 dom cdm 5623 ran crn 5624 ↾ cres 5625 Rel wrel 5628 ⟶wf 6482 ‘cfv 6486 (class class class)co 7353 ↑_m cmap 8760 Fincfn 8879 ℕ₀cn0 12402 ♯chash 14255 Basecbs 17138 +_gcplusg 17179 TopOpenctopn 17343 0_gc0g 17361 Σ_g cgsu 17362 Mndcmnd 18626 -_gcsg 18832 ._gcmg 18964 CMndccmn 19677 TopOnctopon 22813 TopSpctps 22835 TopMndctmd 23973 TopGrpctgp 23974 tsums ctsu 24029

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 2701 ax-rep 5221 ax-sep 5238 ax-nul 5248 ax-pow 5307 ax-pr 5374 ax-un 7675 ax-cnex 11084 ax-resscn 11085 ax-1cn 11086 ax-icn 11087 ax-addcl 11088 ax-addrcl 11089 ax-mulcl 11090 ax-mulrcl 11091 ax-mulcom 11092 ax-addass 11093 ax-mulass 11094 ax-distr 11095 ax-i2m1 11096 ax-1ne0 11097 ax-1rid 11098 ax-rnegex 11099 ax-rrecex 11100 ax-cnre 11101 ax-pre-lttri 11102 ax-pre-lttrn 11103 ax-pre-ltadd 11104 ax-pre-mulgt0 11105

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 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3345 df-reu 3346 df-rab 3397 df-v 3440 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4479 df-pw 4555 df-sn 4580 df-pr 4582 df-op 4586 df-uni 4862 df-int 4900 df-iun 4946 df-iin 4947 df-br 5096 df-opab 5158 df-mpt 5177 df-tr 5203 df-id 5518 df-eprel 5523 df-po 5531 df-so 5532 df-fr 5576 df-se 5577 df-we 5578 df-xp 5629 df-rel 5630 df-cnv 5631 df-co 5632 df-dm 5633 df-rn 5634 df-res 5635 df-ima 5636 df-pred 6253 df-ord 6314 df-on 6315 df-lim 6316 df-suc 6317 df-iota 6442 df-fun 6488 df-fn 6489 df-f 6490 df-f1 6491 df-fo 6492 df-f1o 6493 df-fv 6494 df-isom 6495 df-riota 7310 df-ov 7356 df-oprab 7357 df-mpo 7358 df-of 7617 df-om 7807 df-1st 7931 df-2nd 7932 df-supp 8101 df-frecs 8221 df-wrecs 8252 df-recs 8301 df-rdg 8339 df-1o 8395 df-2o 8396 df-er 8632 df-map 8762 df-ixp 8832 df-en 8880 df-dom 8881 df-sdom 8882 df-fin 8883 df-fsupp 9271 df-fi 9320 df-oi 9421 df-card 9854 df-pnf 11170 df-mnf 11171 df-xr 11172 df-ltxr 11173 df-le 11174 df-sub 11367 df-neg 11368 df-nn 12147 df-2 12209 df-n0 12403 df-z 12490 df-uz 12754 df-fz 13429 df-fzo 13576 df-seq 13927 df-hash 14256 df-sets 17093 df-slot 17111 df-ndx 17123 df-base 17139 df-ress 17160 df-plusg 17192 df-rest 17344 df-0g 17363 df-gsum 17364 df-topgen 17365 df-pt 17366 df-mre 17506 df-mrc 17507 df-acs 17509 df-plusf 18531 df-mgm 18532 df-sgrp 18611 df-mnd 18627 df-mhm 18675 df-submnd 18676 df-grp 18833 df-minusg 18834 df-sbg 18835 df-mulg 18965 df-ghm 19110 df-cntz 19214 df-cmn 19679 df-abl 19680 df-fbas 21276 df-fg 21277 df-top 22797 df-topon 22814 df-topsp 22836 df-bases 22849 df-ntr 22923 df-nei 23001 df-cn 23130 df-cnp 23131 df-cmp 23290 df-tx 23465 df-xko 23466 df-hmeo 23658 df-fil 23749 df-fm 23841 df-flim 23842 df-flf 23843 df-tmd 23975 df-tgp 23976 df-tsms 24030

This theorem is referenced by: (None)

W3C validator