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 24139

Description: Write a sum over a two-dimensional region as a double sum. This infinite group sum version of gsumxp 19943 is also known as Fubini's theorem. The converse is not necessarily true without additional assumptions. See tsmsxplem1 24137 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 24063	. . . . . . . . . . 11 ⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ TopMnd)
3	1, 2	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺 ∈ TopMnd)
4	3	3ad2ant1 1139	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → 𝐺 ∈ TopMnd)
5		simp2 1143	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → 𝑢 ∈ (TopOpen‘𝐺))
6		eqid 2739	. . . . . . . . . . . . 13 ⊢ (TopOpen‘𝐺) = (TopOpen‘𝐺)
7		tsmsxp.b	. . . . . . . . . . . . 13 ⊢ 𝐵 = (Base‘𝐺)
8	6, 7	tmdtopon 24065	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ TopMnd → (TopOpen‘𝐺) ∈ (TopOn‘𝐵))
9	4, 8	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → (TopOpen‘𝐺) ∈ (TopOn‘𝐵))
10		toponss 22911	. . . . . . . . . . 11 ⊢ (((TopOpen‘𝐺) ∈ (TopOn‘𝐵) ∧ 𝑢 ∈ (TopOpen‘𝐺)) → 𝑢 ⊆ 𝐵)
11	9, 5, 10	syl2anc 590	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → 𝑢 ⊆ 𝐵)
12		simp3 1144	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → 𝑥 ∈ 𝑢)
13	11, 12	sseldd 3916	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → 𝑥 ∈ 𝐵)
14		tmdmnd 24059	. . . . . . . . . . 11 ⊢ (𝐺 ∈ TopMnd → 𝐺 ∈ Mnd)
15	4, 14	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → 𝐺 ∈ Mnd)
16		eqid 2739	. . . . . . . . . . 11 ⊢ (0_g‘𝐺) = (0_g‘𝐺)
17	7, 16	mndidcl 18709	. . . . . . . . . 10 ⊢ (𝐺 ∈ Mnd → (0_g‘𝐺) ∈ 𝐵)
18	15, 17	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → (0_g‘𝐺) ∈ 𝐵)
19		eqid 2739	. . . . . . . . . . . 12 ⊢ (+_g‘𝐺) = (+_g‘𝐺)
20	7, 19, 16	mndrid 18715	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵) → (𝑥(+_g‘𝐺)(0_g‘𝐺)) = 𝑥)
21	15, 13, 20	syl2anc 590	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → (𝑥(+_g‘𝐺)(0_g‘𝐺)) = 𝑥)
22	21, 12	eqeltrd 2839	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → (𝑥(+_g‘𝐺)(0_g‘𝐺)) ∈ 𝑢)
23	7, 6, 19	tmdcn2 24073	. . . . . . . . 9 ⊢ (((𝐺 ∈ TopMnd ∧ 𝑢 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝐵 ∧ (0_g‘𝐺) ∈ 𝐵 ∧ (𝑥(+_g‘𝐺)(0_g‘𝐺)) ∈ 𝑢)) → ∃𝑣 ∈ (TopOpen‘𝐺)∃𝑡 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢))
24	4, 5, 13, 18, 22, 23	syl23anc 1385	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → ∃𝑣 ∈ (TopOpen‘𝐺)∃𝑡 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢))
25		r19.29 3102	. . . . . . . . 9 ⊢ ((∀𝑣 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ ∃𝑣 ∈ (TopOpen‘𝐺)∃𝑡 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) → ∃𝑣 ∈ (TopOpen‘𝐺)((𝑥 ∈ 𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ ∃𝑡 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)))
26		simp31 1216	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) → 𝑥 ∈ 𝑣)
27		elfpw 9255	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ↔ (𝑦 ⊆ (𝐴 × 𝐶) ∧ 𝑦 ∈ Fin))
28	27	simplbi 497	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) → 𝑦 ⊆ (𝐴 × 𝐶))
29	28	ad2antrl 734	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣))) → 𝑦 ⊆ (𝐴 × 𝐶))
30		dmss 5845	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ⊆ (𝐴 × 𝐶) → dom 𝑦 ⊆ dom (𝐴 × 𝐶))
31	29, 30	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣))) → dom 𝑦 ⊆ dom (𝐴 × 𝐶))
32		dmxpss 6123	. . . . . . . . . . . . . . . . . . 19 ⊢ dom (𝐴 × 𝐶) ⊆ 𝐴
33	31, 32	sstrdi 3927	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣))) → dom 𝑦 ⊆ 𝐴)
34		elinel2 4132	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) → 𝑦 ∈ Fin)
35	34	ad2antrl 734	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣))) → 𝑦 ∈ Fin)
36		dmfi 9236	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ Fin → dom 𝑦 ∈ Fin)
37	35, 36	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣))) → dom 𝑦 ∈ Fin)
38		elfpw 9255	. . . . . . . . . . . . . . . . . 18 ⊢ (dom 𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↔ (dom 𝑦 ⊆ 𝐴 ∧ dom 𝑦 ∈ Fin))
39	33, 37, 38	sylanbrc 589	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣))) → dom 𝑦 ∈ (𝒫 𝐴 ∩ Fin))
40		eqid 2739	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (._g‘𝐺) = (._g‘𝐺)
41		simpl11 1255	. . . . . . . . . . . . . . . . . . . . . . 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 786	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏))) → 𝑏 ∈ (𝒫 𝐴 ∩ Fin))
46	45	elin2d 4135	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏))) → 𝑏 ∈ Fin)
47		simpl2r 1234	. . . . . . . . . . . . . . . . . . . . . 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 14310	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑏 ∈ Fin → (♯‘𝑏) ∈ ℕ₀)
51	46, 50	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏))) → (♯‘𝑏) ∈ ℕ₀)
52	7, 40, 16	mulgnn0z 19069	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐺 ∈ Mnd ∧ (♯‘𝑏) ∈ ℕ₀) → ((♯‘𝑏)(._g‘𝐺)(0_g‘𝐺)) = (0_g‘𝐺))
53	48, 51, 52	syl2anc 590	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏))) → ((♯‘𝑏)(._g‘𝐺)(0_g‘𝐺)) = (0_g‘𝐺))
54		simpl32 1262	. . . . . . . . . . . . . . . . . . . . . . 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 24080	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏))) → ∃𝑠 ∈ (TopOpen‘𝐺)((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡))
57		simp111 1309	. . . . . . . . . . . . . . . . . . . . . . . . 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 586	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡))) ∧ 𝑗 ∈ 𝐴) → (𝐻‘𝑗) ∈ (𝐺 tsums (𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘))))
70		eqid 2739	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (-_g‘𝐺) = (-_g‘𝐺)
71		simp3l 1208	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡))) → 𝑠 ∈ (TopOpen‘𝐺))
72		simp3rl 1253	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡))) → (0_g‘𝐺) ∈ 𝑠)
73		simp2rl 1249	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡))) → 𝑏 ∈ (𝒫 𝐴 ∩ Fin))
74		simp2rr 1250	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡))) → dom 𝑦 ⊆ 𝑏)
75		simp2ll 1247	. . . . . . . . . . . . . . . . . . . . . . . 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 24137	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡))) → ∃𝑛 ∈ (𝒫 𝐶 ∩ Fin)(ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠))
77	43	3adant3 1138	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 1188	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 1188	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝐴 ∈ 𝑉)
80	63	3adant3r 1188	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝐶 ∈ 𝑊)
81	65	3adant3r 1188	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝐹:(𝐴 × 𝐶)⟶𝐵)
82	67	3adant3r 1188	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝐻:𝐴⟶𝐵)
83	41	3adant3 1138	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 586	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) ∧ 𝑗 ∈ 𝐴) → (𝐻‘𝑗) ∈ (𝐺 tsums (𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘))))
85		simp3ll 1251	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 1188	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 1249	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝑏 ∈ (𝒫 𝐴 ∩ Fin))
88		simp133 1317	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)
89		simp3rl 1253	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝑛 ∈ (𝒫 𝐶 ∩ Fin))
90		simp2ll 1247	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin))
91		simp2rr 1250	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝑏 ((𝐻‘𝑥)(-_g‘𝐺)(𝐺 Σ_g (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → dom 𝑦 ⊆ 𝑏)
92		simp3rr 1254	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5637	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ Rel (𝐴 × 𝐶)
95		relss 5726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5634	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((dom 𝑦 ⊆ 𝑏 ∧ ran 𝑦 ⊆ 𝑛) → (dom 𝑦 × ran 𝑦) ⊆ (𝑏 × 𝑛))
100	98, 99	sylan9ss 3928	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ (dom 𝑦 ⊆ 𝑏 ∧ ran 𝑦 ⊆ 𝑛)) → 𝑦 ⊆ (𝑏 × 𝑛))
101	90, 91, 93, 100	syl12anc 842	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 3941	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑧 = (𝑏 × 𝑛) → (𝑦 ⊆ 𝑧 ↔ 𝑦 ⊆ (𝑏 × 𝑛)))
104		reseq2 5927	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑧 = (𝑏 × 𝑛) → (𝐹 ↾ 𝑧) = (𝐹 ↾ (𝑏 × 𝑛)))
105	104	oveq2d 7373	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑧 = (𝑏 × 𝑛) → (𝐺 Σ_g (𝐹 ↾ 𝑧)) = (𝐺 Σ_g (𝐹 ↾ (𝑏 × 𝑛))))
106	105	eleq1d 2824	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑧 = (𝑏 × 𝑛) → ((𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣 ↔ (𝐺 Σ_g (𝐹 ↾ (𝑏 × 𝑛))) ∈ 𝑣))
107	103, 106	imbi12d 345	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑧 = (𝑏 × 𝑛) → ((𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣) ↔ (𝑦 ⊆ (𝑏 × 𝑛) → (𝐺 Σ_g (𝐹 ↾ (𝑏 × 𝑛))) ∈ 𝑣)))
108		simp2lr 1248	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9255	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝑏 ⊆ 𝐴 ∧ 𝑏 ∈ Fin))
110		elfpw 9255	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ↔ (𝑛 ⊆ 𝐶 ∧ 𝑛 ∈ Fin))
111		xpss12 5634	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑏 ⊆ 𝐴 ∧ 𝑛 ⊆ 𝐶) → (𝑏 × 𝑛) ⊆ (𝐴 × 𝐶))
112		xpfi 9221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑏 ∈ Fin ∧ 𝑛 ∈ Fin) → (𝑏 × 𝑛) ∈ Fin)
113	111, 112	anim12i 619	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑏 ⊆ 𝐴 ∧ 𝑛 ⊆ 𝐶) ∧ (𝑏 ∈ Fin ∧ 𝑛 ∈ Fin)) → ((𝑏 × 𝑛) ⊆ (𝐴 × 𝐶) ∧ (𝑏 × 𝑛) ∈ Fin))
114	113	an4s 666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑏 ⊆ 𝐴 ∧ 𝑏 ∈ Fin) ∧ (𝑛 ⊆ 𝐶 ∧ 𝑛 ∈ Fin)) → ((𝑏 × 𝑛) ⊆ (𝐴 × 𝐶) ∧ (𝑏 × 𝑛) ∈ Fin))
115	109, 110, 114	syl2anb 604	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑛 ∈ (𝒫 𝐶 ∩ Fin)) → ((𝑏 × 𝑛) ⊆ (𝐴 × 𝐶) ∧ (𝑏 × 𝑛) ∈ Fin))
116		elfpw 9255	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑏 × 𝑛) ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ↔ ((𝑏 × 𝑛) ⊆ (𝐴 × 𝐶) ∧ (𝑏 × 𝑛) ∈ Fin))
117	115, 116	sylibr 235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑛 ∈ (𝒫 𝐶 ∩ Fin)) → (𝑏 × 𝑛) ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin))
118	87, 89, 117	syl2anc 590	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3561	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1252	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7365	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑔 = ℎ → (𝐺 Σ_g 𝑔) = (𝐺 Σ_g ℎ))
124	123	eleq1d 2824	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑔 = ℎ → ((𝐺 Σ_g 𝑔) ∈ 𝑡 ↔ (𝐺 Σ_g ℎ) ∈ 𝑡))
125	124	cbvralvw 3217	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡 ↔ ∀ℎ ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g ℎ) ∈ 𝑡)
126	122, 125	sylib 219	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 24138	. . . . . . . . . . . . . . . . . . . . . . . . . 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 1125	. . . . . . . . . . . . . . . . . . . . . . . . 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 1354	. . . . . . . . . . . . . . . . . . . . . . 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 3146	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡))) → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢)
132	131	3expa 1124	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦 ⊆ 𝑏))) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0_g‘𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠 ↑_m 𝑏)(𝐺 Σ_g 𝑔) ∈ 𝑡))) → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢)
133	56, 132	rexlimddv 3146	. . . . . . . . . . . . . . . . . . . 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 3131	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣))) → ∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(dom 𝑦 ⊆ 𝑏 → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢))
137		sseq1 3940	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = dom 𝑦 → (𝑎 ⊆ 𝑏 ↔ dom 𝑦 ⊆ 𝑏))
138	137	rspceaimv 3566	. . . . . . . . . . . . . . . . 17 ⊢ ((dom 𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ ∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(dom 𝑦 ⊆ 𝑏 → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢))
139	39, 136, 138	syl2anc 590	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥 ∈ 𝑣 ∧ (0_g‘𝐺) ∈ 𝑡 ∧ ∀𝑐 ∈ 𝑣 ∀𝑑 ∈ 𝑡 (𝑐(+_g‘𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣))) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢))
140	139	rexlimdvaa 3141	. . . . . . . . . . . . . . 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 1127	. . . . . . . . . . . . 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 3140	. . . . . . . . . . 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 3140	. . . . . . . . 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 700	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥 ∈ 𝑢) → (∀𝑣 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢)))
149	148	3expia 1127	. . . . . 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 3139	. . . 4 ⊢ (𝜑 → (∀𝑣 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)) → ∀𝑢 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑢 → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢))))
152	151	anim2d 618	. . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐵 ∧ ∀𝑣 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣))) → (𝑥 ∈ 𝐵 ∧ ∀𝑢 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑢 → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢)))))
153		eqid 2739	. . . 4 ⊢ (𝒫 (𝐴 × 𝐶) ∩ Fin) = (𝒫 (𝐴 × 𝐶) ∩ Fin)
154		tgptps 24064	. . . . 5 ⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ TopSp)
155	1, 154	syl 17	. . . 4 ⊢ (𝜑 → 𝐺 ∈ TopSp)
156	60, 62	xpexd 7695	. . . 4 ⊢ (𝜑 → (𝐴 × 𝐶) ∈ V)
157	7, 6, 153, 42, 155, 156, 64	eltsms 24117	. . 3 ⊢ (𝜑 → (𝑥 ∈ (𝐺 tsums 𝐹) ↔ (𝑥 ∈ 𝐵 ∧ ∀𝑣 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ 𝑣)))))
158		eqid 2739	. . . 4 ⊢ (𝒫 𝐴 ∩ Fin) = (𝒫 𝐴 ∩ Fin)
159	7, 6, 158, 42, 155, 60, 66	eltsms 24117	. . 3 ⊢ (𝜑 → (𝑥 ∈ (𝐺 tsums 𝐻) ↔ (𝑥 ∈ 𝐵 ∧ ∀𝑢 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑢 → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σ_g (𝐻 ↾ 𝑏)) ∈ 𝑢)))))
160	152, 157, 159	3imtr4d 295	. 2 ⊢ (𝜑 → (𝑥 ∈ (𝐺 tsums 𝐹) → 𝑥 ∈ (𝐺 tsums 𝐻)))
161	160	ssrdv 3921	1 ⊢ (𝜑 → (𝐺 tsums 𝐹) ⊆ (𝐺 tsums 𝐻))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1092 = wceq 1547 ∈ wcel 2119 ∀wral 3053 ∃wrex 3063 Vcvv 3431 ∩ cin 3882 ⊆ wss 3883 𝒫 cpw 4530 {csn 4556 ↦ cmpt 5154 × cxp 5617 dom cdm 5619 ran crn 5620 ↾ cres 5621 Rel wrel 5624 ⟶wf 6482 ‘cfv 6486 (class class class)co 7357 ↑_m cmap 8764 Fincfn 8884 ℕ₀cn0 12429 ♯chash 14284 Basecbs 17171 +_gcplusg 17212 TopOpenctopn 17376 0_gc0g 17394 Σ_g cgsu 17395 Mndcmnd 18694 -_gcsg 18903 ._gcmg 19035 CMndccmn 19747 TopOnctopon 22894 TopSpctps 22916 TopMndctmd 24054 TopGrpctgp 24055 tsums ctsu 24110

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2711 ax-rep 5200 ax-sep 5219 ax-nul 5229 ax-pow 5295 ax-pr 5363 ax-un 7679 ax-cnex 11086 ax-resscn 11087 ax-1cn 11088 ax-icn 11089 ax-addcl 11090 ax-addrcl 11091 ax-mulcl 11092 ax-mulrcl 11093 ax-mulcom 11094 ax-addass 11095 ax-mulass 11096 ax-distr 11097 ax-i2m1 11098 ax-1ne0 11099 ax-1rid 11100 ax-rnegex 11101 ax-rrecex 11102 ax-cnre 11103 ax-pre-lttri 11104 ax-pre-lttrn 11105 ax-pre-ltadd 11106 ax-pre-mulgt0 11107

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3or 1093 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2718 df-cleq 2731 df-clel 2814 df-nfc 2888 df-ne 2935 df-nel 3039 df-ral 3054 df-rex 3064 df-rmo 3344 df-reu 3345 df-rab 3392 df-v 3433 df-sbc 3724 df-csb 3832 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3903 df-nul 4263 df-if 4456 df-pw 4532 df-sn 4557 df-pr 4559 df-op 4563 df-uni 4840 df-int 4879 df-iun 4924 df-iin 4925 df-br 5074 df-opab 5136 df-mpt 5155 df-tr 5181 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-se 5573 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 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 7314 df-ov 7360 df-oprab 7361 df-mpo 7362 df-of 7621 df-om 7808 df-1st 7932 df-2nd 7933 df-supp 8102 df-frecs 8222 df-wrecs 8253 df-recs 8302 df-rdg 8340 df-1o 8396 df-2o 8397 df-er 8634 df-map 8766 df-ixp 8837 df-en 8885 df-dom 8886 df-sdom 8887 df-fin 8888 df-fsupp 9266 df-fi 9315 df-oi 9416 df-card 9855 df-pnf 11173 df-mnf 11174 df-xr 11175 df-ltxr 11176 df-le 11177 df-sub 11371 df-neg 11372 df-nn 12167 df-2 12236 df-n0 12430 df-z 12517 df-uz 12781 df-fz 13454 df-fzo 13601 df-seq 13956 df-hash 14285 df-sets 17126 df-slot 17144 df-ndx 17156 df-base 17172 df-ress 17193 df-plusg 17225 df-rest 17377 df-0g 17396 df-gsum 17397 df-topgen 17398 df-pt 17399 df-mre 17540 df-mrc 17541 df-acs 17543 df-plusf 18599 df-mgm 18600 df-sgrp 18679 df-mnd 18695 df-mhm 18743 df-submnd 18744 df-grp 18904 df-minusg 18905 df-sbg 18906 df-mulg 19036 df-ghm 19180 df-cntz 19284 df-cmn 19749 df-abl 19750 df-fbas 21345 df-fg 21346 df-top 22878 df-topon 22895 df-topsp 22917 df-bases 22930 df-ntr 23004 df-nei 23082 df-cn 23211 df-cnp 23212 df-cmp 23371 df-tx 23546 df-xko 23547 df-hmeo 23739 df-fil 23830 df-fm 23922 df-flim 23923 df-flf 23924 df-tmd 24056 df-tgp 24057 df-tsms 24111

This theorem is referenced by: (None)

W3C validator