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 24195

Description: Write a sum over a two-dimensional region as a double sum. This infinite group sum version of gsumxp 19999 is also known as Fubini's theorem. The converse is not necessarily true without additional assumptions. See tsmsxplem1 24193 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 24119	. . . . . . . . . . 11 ⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ TopMnd)
3	1, 2	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺 ∈ TopMnd)
4	3	3ad2ant1 1145	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → 𝐺 ∈ TopMnd)
5		simp2 1149	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → 𝑢 ∈ (TopOpen‘𝐺))
6		eqid 2761	. . . . . . . . . . . . 13 ⊢ (TopOpen‘𝐺) = (TopOpen‘𝐺)
7		tsmsxp.b	. . . . . . . . . . . . 13 ⊢ 𝐵 = (Base‘𝐺)
8	6, 7	tmdtopon 24121	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ TopMnd → (TopOpen‘𝐺) ∈ (TopOn‘𝐵))
9	4, 8	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → (TopOpen‘𝐺) ∈ (TopOn‘𝐵))
10		toponss 22967	. . . . . . . . . . 11 ⊢ (((TopOpen‘𝐺) ∈ (TopOn‘𝐵) ∧ 𝑢 ∈ (TopOpen‘𝐺)) → 𝑢 ⊆ 𝐵)
11	9, 5, 10	syl2anc 593	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → 𝑢 ⊆ 𝐵)
12		simp3 1150	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → 𝑥 ∈ 𝑢)
13	11, 12	sseldd 3937	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → 𝑥 ∈ 𝐵)
14		tmdmnd 24115	. . . . . . . . . . 11 ⊢ (𝐺 ∈ TopMnd → 𝐺 ∈ Mnd)
15	4, 14	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → 𝐺 ∈ Mnd)
16		eqid 2761	. . . . . . . . . . 11 ⊢ (0_g‘𝐺) = (0_g‘𝐺)
17	7, 16	mndidcl 18766	. . . . . . . . . 10 ⊢ (𝐺 ∈ Mnd → (0_g‘𝐺) ∈ 𝐵)
18	15, 17	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → (0_g‘𝐺) ∈ 𝐵)
19		eqid 2761	. . . . . . . . . . . 12 ⊢ (+_g‘𝐺) = (+_g‘𝐺)
20	7, 19, 16	mndrid 18772	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵) → (𝑥(+_g‘𝐺)(0_g‘𝐺)) = 𝑥)
21	15, 13, 20	syl2anc 593	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → (𝑥(+_g‘𝐺)(0_g‘𝐺)) = 𝑥)
22	21, 12	eqeltrd 2861	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → (𝑥(+_g‘𝐺)(0_g‘𝐺)) ∈ 𝑢)
23	7, 6, 19	tmdcn2 24129	. . . . . . . . 9 ⊢ (((𝐺 ∈ TopMnd ∧ 𝑢 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝐵 ∧ (0_g‘𝐺) ∈ 𝐵 ∧ (𝑥(+_g‘𝐺)(0_g‘𝐺)) ∈ 𝑢)) → ∃𝑣 ∈ (TopOpen‘𝐺)∃𝑡 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢))
24	4, 5, 13, 18, 22, 23	syl23anc 1395	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → ∃𝑣 ∈ (TopOpen‘𝐺)∃𝑡 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢))
25		r19.29 3124	. . . . . . . . 9 ⊢ ((∀𝑣 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ ∃𝑣 ∈ (TopOpen‘𝐺)∃𝑡 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) → ∃𝑣 ∈ (TopOpen‘𝐺)((𝑥 ∈ 𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ ∃𝑡 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)))
26		simp31 1222	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) → 𝑥 ∈ 𝑣)
27		elfpw 9294	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ↔ (𝑦 ⊆ (𝐴 × 𝐶) ∧ 𝑦 ∈ Fin))
28	27	simplbi 500	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) → 𝑦 ⊆ (𝐴 × 𝐶))
29	28	ad2antrl 738	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣))) → 𝑦 ⊆ (𝐴 × 𝐶))
30		dmss 5876	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ⊆ (𝐴 × 𝐶) → dom 𝑦 ⊆ dom (𝐴 × 𝐶))
31	29, 30	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣))) → dom 𝑦 ⊆ dom (𝐴 × 𝐶))
32		dmxpss 6153	. . . . . . . . . . . . . . . . . . 19 ⊢ dom (𝐴 × 𝐶) ⊆ 𝐴
33	31, 32	sstrdi 3948	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣))) → dom 𝑦 ⊆ 𝐴)
34		elinel2 4154	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) → 𝑦 ∈ Fin)
35	34	ad2antrl 738	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣))) → 𝑦 ∈ Fin)
36		dmfi 9275	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ Fin → dom 𝑦 ∈ Fin)
37	35, 36	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣))) → dom 𝑦 ∈ Fin)
38		elfpw 9294	. . . . . . . . . . . . . . . . . 18 ⊢ (dom 𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↔ (dom 𝑦 ⊆ 𝐴 ∧ dom 𝑦 ∈ Fin))
39	33, 37, 38	sylanbrc 592	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣))) → dom 𝑦 ∈ (𝒫 𝐴 ∩ Fin))
40		eqid 2761	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (._g‘𝐺) = (._g‘𝐺)
41		simpl11 1261	. . . . . . . . . . . . . . . . . . . . . . 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 790	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏))) → 𝑏 ∈ (𝒫 𝐴 ∩ Fin))
46	45	elin2d 4157	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏))) → 𝑏 ∈ Fin)
47		simpl2r 1240	. . . . . . . . . . . . . . . . . . . . . 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 14366	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑏 ∈ Fin → (♯‘𝑏) ∈ ℕ₀)
51	46, 50	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏))) → (♯‘𝑏) ∈ ℕ₀)
52	7, 40, 16	mulgnn0z 19126	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐺 ∈ Mnd ∧ (♯‘𝑏) ∈ ℕ₀) → ((♯‘𝑏)(._g‘𝐺)(0_g‘𝐺)) = (0_g‘𝐺))
53	48, 51, 52	syl2anc 593	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏))) → ((♯‘𝑏)(._g‘𝐺)(0_g‘𝐺)) = (0_g‘𝐺))
54		simpl32 1268	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏))) → (0_g‘𝐺) ∈ 𝑡)
55	53, 54	eqeltrd 2861	. . . . . . . . . . . . . . . . . . . . . 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 24136	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏))) → ∃𝑠 ∈ (TopOpen‘𝐺)((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡))
57		simp111 1315	. . . . . . . . . . . . . . . . . . . . . . . . 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 589	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡))) ∧ 𝑗 ∈ 𝐴) → (𝐻‘𝑗) ∈ (𝐺 tsums (𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘))))
70		eqid 2761	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (-_g‘𝐺) = (-_g‘𝐺)
71		simp3l 1214	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡))) → 𝑠 ∈ (TopOpen‘𝐺))
72		simp3rl 1259	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡))) → (0_g‘𝐺) ∈ 𝑠)
73		simp2rl 1255	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡))) → 𝑏 ∈ (𝒫 𝐴 ∩ Fin))
74		simp2rr 1256	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡))) → dom 𝑦 ⊆ 𝑏)
75		simp2ll 1253	. . . . . . . . . . . . . . . . . . . . . . . 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 24193	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡))) → ∃𝑛 ∈ (𝒫 𝐶 ∩ Fin)(ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠))
77	43	3adant3 1144	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 1194	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 1194	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝐴 ∈ 𝑉)
80	63	3adant3r 1194	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝐶 ∈ 𝑊)
81	65	3adant3r 1194	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝐹:(𝐴 × 𝐶)⟶𝐵)
82	67	3adant3r 1194	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝐻:𝐴⟶𝐵)
83	41	3adant3 1144	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 589	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) ∧ 𝑗 ∈ 𝐴) → (𝐻‘𝑗) ∈ (𝐺 tsums (𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘))))
85		simp3ll 1257	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 1194	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 1255	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝑏 ∈ (𝒫 𝐴 ∩ Fin))
88		simp133 1323	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)
89		simp3rl 1259	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝑛 ∈ (𝒫 𝐶 ∩ Fin))
90		simp2ll 1253	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin))
91		simp2rr 1256	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → dom 𝑦 ⊆ 𝑏)
92		simp3rr 1260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 498	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → ran 𝑦 ⊆ 𝑛)
94		relxp 5663	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ Rel (𝐴 × 𝐶)
95		relss 5752	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑦 ⊆ (𝐴 × 𝐶) → (Rel (𝐴 × 𝐶) → Rel 𝑦))
96	28, 94, 95	mpisyl 21	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) → Rel 𝑦)
97		relssdmrn 6252	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (Rel 𝑦 → 𝑦 ⊆ (dom 𝑦 × ran 𝑦))
98	96, 97	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) → 𝑦 ⊆ (dom 𝑦 × ran 𝑦))
99		xpss12 5660	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((dom 𝑦 ⊆ 𝑏 ∧ ran 𝑦 ⊆ 𝑛) → (dom 𝑦 × ran 𝑦) ⊆ (𝑏 × 𝑛))
100	98, 99	sylan9ss 3949	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ (dom 𝑦 ⊆ 𝑏 ∧ ran 𝑦 ⊆ 𝑛)) → 𝑦 ⊆ (𝑏 × 𝑛))
101	90, 91, 93, 100	syl12anc 847	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝑦 ⊆ (𝑏 × 𝑛))
102	92	simprd 499	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 3962	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑧 = (𝑏 × 𝑛) → (𝑦 ⊆ 𝑧 ↔ 𝑦 ⊆ (𝑏 × 𝑛)))
104		reseq2 5958	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑧 = (𝑏 × 𝑛) → (𝐹 ↾ 𝑧) = (𝐹 ↾ (𝑏 × 𝑛)))
105	104	oveq2d 7408	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑧 = (𝑏 × 𝑛) → (𝐺 Σ_g (𝐹 ↾ 𝑧)) = (𝐺 Σ_g (𝐹 ↾ (𝑏 × 𝑛))))
106	105	eleq1d 2846	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑧 = (𝑏 × 𝑛) → ((𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣 ↔ (𝐺 Σ_g (𝐹 ↾ (𝑏 × 𝑛))) ∈ 𝑣))
107	103, 106	imbi12d 346	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑧 = (𝑏 × 𝑛) → ((𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣) ↔ (𝑦 ⊆ (𝑏 × 𝑛) → (𝐺 Σ_g (𝐹 ↾ (𝑏 × 𝑛))) ∈ 𝑣)))
108		simp2lr 1254	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9294	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝑏 ⊆ 𝐴 ∧ 𝑏 ∈ Fin))
110		elfpw 9294	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ↔ (𝑛 ⊆ 𝐶 ∧ 𝑛 ∈ Fin))
111		xpss12 5660	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑏 ⊆ 𝐴 ∧ 𝑛 ⊆ 𝐶) → (𝑏 × 𝑛) ⊆ (𝐴 × 𝐶))
112		xpfi 9260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑏 ∈ Fin ∧ 𝑛 ∈ Fin) → (𝑏 × 𝑛) ∈ Fin)
113	111, 112	anim12i 622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑏 ⊆ 𝐴 ∧ 𝑛 ⊆ 𝐶) ∧ (𝑏 ∈ Fin ∧ 𝑛 ∈ Fin)) → ((𝑏 × 𝑛) ⊆ (𝐴 × 𝐶) ∧ (𝑏 × 𝑛) ∈ Fin))
114	113	an4s 670	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑏 ⊆ 𝐴 ∧ 𝑏 ∈ Fin) ∧ (𝑛 ⊆ 𝐶 ∧ 𝑛 ∈ Fin)) → ((𝑏 × 𝑛) ⊆ (𝐴 × 𝐶) ∧ (𝑏 × 𝑛) ∈ Fin))
115	109, 110, 114	syl2anb 607	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑛 ∈ (𝒫 𝐶 ∩ Fin)) → ((𝑏 × 𝑛) ⊆ (𝐴 × 𝐶) ∧ (𝑏 × 𝑛) ∈ Fin))
116		elfpw 9294	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑏 × 𝑛) ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ↔ ((𝑏 × 𝑛) ⊆ (𝐴 × 𝐶) ∧ (𝑏 × 𝑛) ∈ Fin))
117	115, 116	sylibr 236	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑛 ∈ (𝒫 𝐶 ∩ Fin)) → (𝑏 × 𝑛) ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin))
118	87, 89, 117	syl2anc 593	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3582	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1258	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 499	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7400	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑔 = ℎ → (𝐺 Σ_g 𝑔) = (𝐺 Σ_g ℎ))
124	123	eleq1d 2846	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑔 = ℎ → ((𝐺 Σ_g 𝑔) ∈ 𝑡 ↔ (𝐺 Σ_g ℎ) ∈ 𝑡))
125	124	cbvralvw 3239	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡 ↔ ∀ℎ ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g ℎ) ∈ 𝑡)
126	122, 125	sylib 220	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 24194	. . . . . . . . . . . . . . . . . . . . . . . . . 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 1131	. . . . . . . . . . . . . . . . . . . . . . . . 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 435	. . . . . . . . . . . . . . . . . . . . . . . 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 1360	. . . . . . . . . . . . . . . . . . . . . . 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 3168	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡))) → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢)
132	131	3expa 1130	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏))) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡))) → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢)
133	56, 132	rexlimddv 3168	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏))) → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢)
134	133	anassrs 471	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣))) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢)
135	134	expr 460	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣))) ∧ 𝑏 ∈ (𝒫 𝐴 ∩ Fin)) → (dom 𝑦 ⊆ 𝑏 → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢))
136	135	ralrimiva 3153	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣))) → ∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(dom 𝑦 ⊆ 𝑏 → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢))
137		sseq1 3961	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = dom 𝑦 → (𝑎 ⊆ 𝑏 ↔ dom 𝑦 ⊆ 𝑏))
138	137	rspceaimv 3587	. . . . . . . . . . . . . . . . 17 ⊢ ((dom 𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ ∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(dom 𝑦 ⊆ 𝑏 → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢))
139	39, 136, 138	syl2anc 593	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣))) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢))
140	139	rexlimdvaa 3163	. . . . . . . . . . . . . . 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 1133	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺))) → ((𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢) → ((𝑥 ∈ 𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢))))
143	142	anassrs 471	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ 𝑣 ∈ (TopOpen‘𝐺)) ∧ 𝑡 ∈ (TopOpen‘𝐺)) → ((𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢) → ((𝑥 ∈ 𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢))))
144	143	rexlimdva 3162	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ 𝑣 ∈ (TopOpen‘𝐺)) → (∃𝑡 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢) → ((𝑥 ∈ 𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢))))
145	144	impcomd 415	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ 𝑣 ∈ (TopOpen‘𝐺)) → (((𝑥 ∈ 𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ ∃𝑡 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢)))
146	145	rexlimdva 3162	. . . . . . . . 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 704	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → (∀𝑣 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢)))
149	148	3expia 1133	. . . . . 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 3161	. . . 4 ⊢ (𝜑 → (∀𝑣 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) → ∀𝑢 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑢 → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢))))
152	151	anim2d 621	. . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐵 ∧ ∀𝑣 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣))) → (𝑥 ∈ 𝐵 ∧ ∀𝑢 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑢 → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢)))))
153		eqid 2761	. . . 4 ⊢ (𝒫 (𝐴 × 𝐶) ∩ Fin) = (𝒫 (𝐴 × 𝐶) ∩ Fin)
154		tgptps 24120	. . . . 5 ⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ TopSp)
155	1, 154	syl 17	. . . 4 ⊢ (𝜑 → 𝐺 ∈ TopSp)
156	60, 62	xpexd 7730	. . . 4 ⊢ (𝜑 → (𝐴 × 𝐶) ∈ V)
157	7, 6, 153, 42, 155, 156, 64	eltsms 24173	. . 3 ⊢ (𝜑 → (𝑥 ∈ (𝐺 tsums 𝐹) ↔ (𝑥 ∈ 𝐵 ∧ ∀𝑣 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)))))
158		eqid 2761	. . . 4 ⊢ (𝒫 𝐴 ∩ Fin) = (𝒫 𝐴 ∩ Fin)
159	7, 6, 158, 42, 155, 60, 66	eltsms 24173	. . 3 ⊢ (𝜑 → (𝑥 ∈ (𝐺 tsums 𝐻) ↔ (𝑥 ∈ 𝐵 ∧ ∀𝑢 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑢 → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢)))))
160	152, 157, 159	3imtr4d 296	. 2 ⊢ (𝜑 → (𝑥 ∈ (𝐺 tsums 𝐹) → 𝑥 ∈ (𝐺 tsums 𝐻)))
161	160	ssrdv 3942	1 ⊢ (𝜑 → (𝐺 tsums 𝐹) ⊆ (𝐺 tsums 𝐻))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 399 ∧ w3a 1097 = wceq 1559 ∈ wcel 2141 ∀wral 3075 ∃wrex 3085 Vcvv 3453 ∩ cin 3903 ⊆ wss 3904 𝒫 cpw 4554 {csn 4581 ↦ cmpt 5180 × cxp 5643 dom cdm 5645 ran crn 5646 ↾ cres 5647 Rel wrel 5650 ⟶wf 6513 ‘cfv 6517 (class class class)co 7392 ↑_m cmap 8803 Fincfn 8923 ℕ₀cn0 12478 ♯chash 14340 Basecbs 17228 +_gcplusg 17269 TopOpenctopn 17433 0_gc0g 17451 Σ_g cgsu 17452 Mndcmnd 18751 -_gcsg 18960 ._gcmg 19092 CMndccmn 19803 TopOnctopon 22950 TopSpctps 22972 TopMndctmd 24110 TopGrpctgp 24111 tsums ctsu 24166

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-rep 5226 ax-sep 5245 ax-nul 5255 ax-pow 5321 ax-pr 5389 ax-un 7714 ax-cnex 11126 ax-resscn 11127 ax-1cn 11128 ax-icn 11129 ax-addcl 11130 ax-addrcl 11131 ax-mulcl 11132 ax-mulrcl 11133 ax-mulcom 11134 ax-addass 11135 ax-mulass 11136 ax-distr 11137 ax-i2m1 11138 ax-1ne0 11139 ax-1rid 11140 ax-rnegex 11141 ax-rrecex 11142 ax-cnre 11143 ax-pre-lttri 11144 ax-pre-lttrn 11145 ax-pre-ltadd 11146 ax-pre-mulgt0 11147

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1098 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-nf 1803 df-sb 2090 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3061 df-ral 3076 df-rex 3086 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3455 df-sbc 3745 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4582 df-pr 4584 df-op 4588 df-uni 4865 df-int 4905 df-iun 4950 df-iin 4951 df-br 5100 df-opab 5162 df-mpt 5181 df-tr 5207 df-id 5540 df-eprel 5545 df-po 5553 df-so 5554 df-fr 5598 df-se 5599 df-we 5600 df-xp 5651 df-rel 5652 df-cnv 5653 df-co 5654 df-dm 5655 df-rn 5656 df-res 5657 df-ima 5658 df-pred 6284 df-ord 6345 df-on 6346 df-lim 6347 df-suc 6348 df-iota 6473 df-fun 6519 df-fn 6520 df-f 6521 df-f1 6522 df-fo 6523 df-f1o 6524 df-fv 6525 df-isom 6526 df-riota 7349 df-ov 7395 df-oprab 7396 df-mpo 7397 df-of 7656 df-om 7843 df-1st 7966 df-2nd 7967 df-supp 8136 df-frecs 8257 df-wrecs 8288 df-recs 8337 df-rdg 8376 df-1o 8432 df-2o 8433 df-er 8673 df-map 8805 df-ixp 8876 df-en 8924 df-dom 8925 df-sdom 8926 df-fin 8927 df-fsupp 9305 df-fi 9354 df-oi 9455 df-card 9894 df-pnf 11215 df-mnf 11216 df-xr 11217 df-ltxr 11218 df-le 11219 df-sub 11413 df-neg 11414 df-nn 12208 df-2 12277 df-n0 12479 df-z 12566 df-uz 12837 df-fz 13510 df-fzo 13657 df-seq 14012 df-hash 14341 df-sets 17183 df-slot 17201 df-ndx 17213 df-base 17229 df-ress 17250 df-plusg 17282 df-rest 17434 df-0g 17453 df-gsum 17454 df-topgen 17455 df-pt 17456 df-mre 17597 df-mrc 17598 df-acs 17600 df-plusf 18656 df-mgm 18657 df-sgrp 18736 df-mnd 18752 df-mhm 18800 df-submnd 18801 df-grp 18961 df-minusg 18962 df-sbg 18963 df-mulg 19093 df-ghm 19237 df-cntz 19340 df-cmn 19805 df-abl 19806 df-fbas 21401 df-fg 21402 df-top 22934 df-topon 22951 df-topsp 22973 df-bases 22986 df-ntr 23060 df-nei 23138 df-cn 23267 df-cnp 23268 df-cmp 23427 df-tx 23602 df-xko 23603 df-hmeo 23795 df-fil 23886 df-fm 23978 df-flim 23979 df-flf 23980 df-tmd 24112 df-tgp 24113 df-tsms 24167

This theorem is referenced by: (None)

W3C validator