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

Theorem tsmsxp 22168
Description: Write a sum over a two-dimensional region as a double sum. This infinite group sum version of gsumxp 18572 is also known as Fubini's theorem. The converse is not necessarily true without additional assumptions. See tsmsxplem1 22166 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.
StepHypRef Expression
1 tsmsxp.2 . . . . . . . . . . 11 (𝜑𝐺 ∈ TopGrp)
2 tgptmd 22093 . . . . . . . . . . 11 (𝐺 ∈ TopGrp → 𝐺 ∈ TopMnd)
31, 2syl 17 . . . . . . . . . 10 (𝜑𝐺 ∈ TopMnd)
433ad2ant1 1156 . . . . . . . . 9 ((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) → 𝐺 ∈ TopMnd)
5 simp2 1160 . . . . . . . . 9 ((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) → 𝑢 ∈ (TopOpen‘𝐺))
6 eqid 2806 . . . . . . . . . . . . 13 (TopOpen‘𝐺) = (TopOpen‘𝐺)
7 tsmsxp.b . . . . . . . . . . . . 13 𝐵 = (Base‘𝐺)
86, 7tmdtopon 22095 . . . . . . . . . . . 12 (𝐺 ∈ TopMnd → (TopOpen‘𝐺) ∈ (TopOn‘𝐵))
94, 8syl 17 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) → (TopOpen‘𝐺) ∈ (TopOn‘𝐵))
10 toponss 20942 . . . . . . . . . . 11 (((TopOpen‘𝐺) ∈ (TopOn‘𝐵) ∧ 𝑢 ∈ (TopOpen‘𝐺)) → 𝑢𝐵)
119, 5, 10syl2anc 575 . . . . . . . . . 10 ((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) → 𝑢𝐵)
12 simp3 1161 . . . . . . . . . 10 ((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) → 𝑥𝑢)
1311, 12sseldd 3799 . . . . . . . . 9 ((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) → 𝑥𝐵)
14 tmdmnd 22089 . . . . . . . . . . 11 (𝐺 ∈ TopMnd → 𝐺 ∈ Mnd)
154, 14syl 17 . . . . . . . . . 10 ((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) → 𝐺 ∈ Mnd)
16 eqid 2806 . . . . . . . . . . 11 (0g𝐺) = (0g𝐺)
177, 16mndidcl 17509 . . . . . . . . . 10 (𝐺 ∈ Mnd → (0g𝐺) ∈ 𝐵)
1815, 17syl 17 . . . . . . . . 9 ((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) → (0g𝐺) ∈ 𝐵)
19 eqid 2806 . . . . . . . . . . . 12 (+g𝐺) = (+g𝐺)
207, 19, 16mndrid 17513 . . . . . . . . . . 11 ((𝐺 ∈ Mnd ∧ 𝑥𝐵) → (𝑥(+g𝐺)(0g𝐺)) = 𝑥)
2115, 13, 20syl2anc 575 . . . . . . . . . 10 ((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) → (𝑥(+g𝐺)(0g𝐺)) = 𝑥)
2221, 12eqeltrd 2885 . . . . . . . . 9 ((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) → (𝑥(+g𝐺)(0g𝐺)) ∈ 𝑢)
237, 6, 19tmdcn2 22103 . . . . . . . . 9 (((𝐺 ∈ TopMnd ∧ 𝑢 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝐵 ∧ (0g𝐺) ∈ 𝐵 ∧ (𝑥(+g𝐺)(0g𝐺)) ∈ 𝑢)) → ∃𝑣 ∈ (TopOpen‘𝐺)∃𝑡 ∈ (TopOpen‘𝐺)(𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢))
244, 5, 13, 18, 22, 23syl23anc 1489 . . . . . . . 8 ((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) → ∃𝑣 ∈ (TopOpen‘𝐺)∃𝑡 ∈ (TopOpen‘𝐺)(𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢))
25 r19.29 3260 . . . . . . . . 9 ((∀𝑣 ∈ (TopOpen‘𝐺)(𝑥𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ ∃𝑣 ∈ (TopOpen‘𝐺)∃𝑡 ∈ (TopOpen‘𝐺)(𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) → ∃𝑣 ∈ (TopOpen‘𝐺)((𝑥𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ ∃𝑡 ∈ (TopOpen‘𝐺)(𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)))
26 simp31 1259 . . . . . . . . . . . . . . . 16 (((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) → 𝑥𝑣)
27 elfpw 8503 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ↔ (𝑦 ⊆ (𝐴 × 𝐶) ∧ 𝑦 ∈ Fin))
2827simplbi 487 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) → 𝑦 ⊆ (𝐴 × 𝐶))
2928ad2antrl 710 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣))) → 𝑦 ⊆ (𝐴 × 𝐶))
30 dmss 5524 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ⊆ (𝐴 × 𝐶) → dom 𝑦 ⊆ dom (𝐴 × 𝐶))
3129, 30syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣))) → dom 𝑦 ⊆ dom (𝐴 × 𝐶))
32 dmxpss 5776 . . . . . . . . . . . . . . . . . . . 20 dom (𝐴 × 𝐶) ⊆ 𝐴
3331, 32syl6ss 3810 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣))) → dom 𝑦𝐴)
3427simprbi 486 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) → 𝑦 ∈ Fin)
3534ad2antrl 710 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣))) → 𝑦 ∈ Fin)
36 dmfi 8479 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ Fin → dom 𝑦 ∈ Fin)
3735, 36syl 17 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣))) → dom 𝑦 ∈ Fin)
38 elfpw 8503 . . . . . . . . . . . . . . . . . . 19 (dom 𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↔ (dom 𝑦𝐴 ∧ dom 𝑦 ∈ Fin))
3933, 37, 38sylanbrc 574 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣))) → dom 𝑦 ∈ (𝒫 𝐴 ∩ Fin))
40 eqid 2806 . . . . . . . . . . . . . . . . . . . . . . 23 (.g𝐺) = (.g𝐺)
41 simpl11 1322 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏))) → 𝜑)
42 tsmsxp.g . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐺 ∈ CMnd)
4341, 42syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏))) → 𝐺 ∈ CMnd)
4441, 3syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏))) → 𝐺 ∈ TopMnd)
45 simprrl 790 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏))) → 𝑏 ∈ (𝒫 𝐴 ∩ Fin))
46 elfpw 8503 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝑏𝐴𝑏 ∈ Fin))
4746simprbi 486 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑏 ∈ (𝒫 𝐴 ∩ Fin) → 𝑏 ∈ Fin)
4845, 47syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏))) → 𝑏 ∈ Fin)
49 simpl2r 1292 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏))) → 𝑡 ∈ (TopOpen‘𝐺))
5044, 14syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏))) → 𝐺 ∈ Mnd)
5150, 17syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏))) → (0g𝐺) ∈ 𝐵)
52 hashcl 13361 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑏 ∈ Fin → (♯‘𝑏) ∈ ℕ0)
5348, 52syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏))) → (♯‘𝑏) ∈ ℕ0)
547, 40, 16mulgnn0z 17767 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐺 ∈ Mnd ∧ (♯‘𝑏) ∈ ℕ0) → ((♯‘𝑏)(.g𝐺)(0g𝐺)) = (0g𝐺))
5550, 53, 54syl2anc 575 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏))) → ((♯‘𝑏)(.g𝐺)(0g𝐺)) = (0g𝐺))
56 simpl32 1336 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏))) → (0g𝐺) ∈ 𝑡)
5755, 56eqeltrd 2885 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏))) → ((♯‘𝑏)(.g𝐺)(0g𝐺)) ∈ 𝑡)
586, 7, 40, 43, 44, 48, 49, 51, 57tmdgsum2 22110 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏))) → ∃𝑠 ∈ (TopOpen‘𝐺)((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡))
59 simp111 1394 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡))) → 𝜑)
6059, 42syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡))) → 𝐺 ∈ CMnd)
6159, 1syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡))) → 𝐺 ∈ TopGrp)
62 tsmsxp.a . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝐴𝑉)
6359, 62syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡))) → 𝐴𝑉)
64 tsmsxp.c . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝐶𝑊)
6559, 64syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡))) → 𝐶𝑊)
66 tsmsxp.f . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝐹:(𝐴 × 𝐶)⟶𝐵)
6759, 66syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡))) → 𝐹:(𝐴 × 𝐶)⟶𝐵)
68 tsmsxp.h . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝐻:𝐴𝐵)
6959, 68syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡))) → 𝐻:𝐴𝐵)
70 tsmsxp.1 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗𝐴) → (𝐻𝑗) ∈ (𝐺 tsums (𝑘𝐶 ↦ (𝑗𝐹𝑘))))
7159, 70sylan 571 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡))) ∧ 𝑗𝐴) → (𝐻𝑗) ∈ (𝐺 tsums (𝑘𝐶 ↦ (𝑗𝐹𝑘))))
72 eqid 2806 . . . . . . . . . . . . . . . . . . . . . . . . 25 (-g𝐺) = (-g𝐺)
73 simp3l 1251 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡))) → 𝑠 ∈ (TopOpen‘𝐺))
74 simp3rl 1320 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡))) → (0g𝐺) ∈ 𝑠)
75 simp2rl 1316 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡))) → 𝑏 ∈ (𝒫 𝐴 ∩ Fin))
76 simp2rr 1317 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡))) → dom 𝑦𝑏)
77 simp2ll 1314 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡))) → 𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin))
787, 60, 61, 63, 65, 67, 69, 71, 6, 16, 19, 72, 73, 74, 75, 76, 77tsmsxplem1 22166 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡))) → ∃𝑛 ∈ (𝒫 𝐶 ∩ Fin)(ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠))
79433adant3 1155 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝐺 ∈ CMnd)
80613adant3r 1224 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝐺 ∈ TopGrp)
81633adant3r 1224 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝐴𝑉)
82653adant3r 1224 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝐶𝑊)
83673adant3r 1224 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝐹:(𝐴 × 𝐶)⟶𝐵)
84693adant3r 1224 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝐻:𝐴𝐵)
85413adant3 1155 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝜑)
8685, 70sylan 571 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) ∧ 𝑗𝐴) → (𝐻𝑗) ∈ (𝐺 tsums (𝑘𝐶 ↦ (𝑗𝐹𝑘))))
87 simp3ll 1318 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝑠 ∈ (TopOpen‘𝐺))
88743adant3r 1224 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → (0g𝐺) ∈ 𝑠)
89 simp2rl 1316 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝑏 ∈ (𝒫 𝐴 ∩ Fin))
90 simp133 1402 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)
91 simp3rl 1320 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝑛 ∈ (𝒫 𝐶 ∩ Fin))
92 simp2ll 1314 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin))
93 simp2rr 1317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → dom 𝑦𝑏)
94 simp3rr 1321 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠))
9594simpld 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → ran 𝑦𝑛)
96 relxp 5328 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Rel (𝐴 × 𝐶)
97 relss 5408 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑦 ⊆ (𝐴 × 𝐶) → (Rel (𝐴 × 𝐶) → Rel 𝑦))
9828, 96, 97mpisyl 21 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) → Rel 𝑦)
99 relssdmrn 5870 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (Rel 𝑦𝑦 ⊆ (dom 𝑦 × ran 𝑦))
10098, 99syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) → 𝑦 ⊆ (dom 𝑦 × ran 𝑦))
101 xpss12 5326 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((dom 𝑦𝑏 ∧ ran 𝑦𝑛) → (dom 𝑦 × ran 𝑦) ⊆ (𝑏 × 𝑛))
102100, 101sylan9ss 3811 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ (dom 𝑦𝑏 ∧ ran 𝑦𝑛)) → 𝑦 ⊆ (𝑏 × 𝑛))
10392, 93, 95, 102syl12anc 856 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝑦 ⊆ (𝑏 × 𝑛))
10494simprd 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)
105 sseq2 3824 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑧 = (𝑏 × 𝑛) → (𝑦𝑧𝑦 ⊆ (𝑏 × 𝑛)))
106 reseq2 5592 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧 = (𝑏 × 𝑛) → (𝐹𝑧) = (𝐹 ↾ (𝑏 × 𝑛)))
107106oveq2d 6886 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑧 = (𝑏 × 𝑛) → (𝐺 Σg (𝐹𝑧)) = (𝐺 Σg (𝐹 ↾ (𝑏 × 𝑛))))
108107eleq1d 2870 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑧 = (𝑏 × 𝑛) → ((𝐺 Σg (𝐹𝑧)) ∈ 𝑣 ↔ (𝐺 Σg (𝐹 ↾ (𝑏 × 𝑛))) ∈ 𝑣))
109105, 108imbi12d 335 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑧 = (𝑏 × 𝑛) → ((𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣) ↔ (𝑦 ⊆ (𝑏 × 𝑛) → (𝐺 Σg (𝐹 ↾ (𝑏 × 𝑛))) ∈ 𝑣)))
110 simp2lr 1315 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣))
111 elfpw 8503 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ↔ (𝑛𝐶𝑛 ∈ Fin))
112 xpss12 5326 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑏𝐴𝑛𝐶) → (𝑏 × 𝑛) ⊆ (𝐴 × 𝐶))
113 xpfi 8466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑏 ∈ Fin ∧ 𝑛 ∈ Fin) → (𝑏 × 𝑛) ∈ Fin)
114112, 113anim12i 602 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑏𝐴𝑛𝐶) ∧ (𝑏 ∈ Fin ∧ 𝑛 ∈ Fin)) → ((𝑏 × 𝑛) ⊆ (𝐴 × 𝐶) ∧ (𝑏 × 𝑛) ∈ Fin))
115114an4s 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑏𝐴𝑏 ∈ Fin) ∧ (𝑛𝐶𝑛 ∈ Fin)) → ((𝑏 × 𝑛) ⊆ (𝐴 × 𝐶) ∧ (𝑏 × 𝑛) ∈ Fin))
11646, 111, 115syl2anb 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑛 ∈ (𝒫 𝐶 ∩ Fin)) → ((𝑏 × 𝑛) ⊆ (𝐴 × 𝐶) ∧ (𝑏 × 𝑛) ∈ Fin))
117 elfpw 8503 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑏 × 𝑛) ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ↔ ((𝑏 × 𝑛) ⊆ (𝐴 × 𝐶) ∧ (𝑏 × 𝑛) ∈ Fin))
118116, 117sylibr 225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑛 ∈ (𝒫 𝐶 ∩ Fin)) → (𝑏 × 𝑛) ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin))
11989, 91, 118syl2anc 575 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → (𝑏 × 𝑛) ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin))
120109, 110, 119rspcdva 3508 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → (𝑦 ⊆ (𝑏 × 𝑛) → (𝐺 Σg (𝐹 ↾ (𝑏 × 𝑛))) ∈ 𝑣))
121103, 120mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → (𝐺 Σg (𝐹 ↾ (𝑏 × 𝑛))) ∈ 𝑣)
122 simp3lr 1319 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡))
123122simprd 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)
124 oveq2 6878 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑔 = → (𝐺 Σg 𝑔) = (𝐺 Σg ))
125124eleq1d 2870 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑔 = → ((𝐺 Σg 𝑔) ∈ 𝑡 ↔ (𝐺 Σg ) ∈ 𝑡))
126125cbvralv 3360 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡 ↔ ∀ ∈ (𝑠𝑚 𝑏)(𝐺 Σg ) ∈ 𝑡)
127123, 126sylib 209 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → ∀ ∈ (𝑠𝑚 𝑏)(𝐺 Σg ) ∈ 𝑡)
1287, 79, 80, 81, 82, 83, 84, 86, 6, 16, 19, 72, 87, 88, 89, 90, 91, 103, 104, 121, 127tsmsxplem2 22167 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢)
1291283exp 1141 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) → (((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) → (((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠))) → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢)))
130129exp4a 420 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) → (((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) → ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) → ((𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)) → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢))))
1311303imp1 1449 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡))) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠))) → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢)
13278, 131rexlimddv 3223 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡))) → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢)
1331323expa 1140 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏))) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡))) → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢)
13458, 133rexlimddv 3223 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏))) → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢)
135134anassrs 455 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣))) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢)
136135expr 446 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣))) ∧ 𝑏 ∈ (𝒫 𝐴 ∩ Fin)) → (dom 𝑦𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢))
137136ralrimiva 3154 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣))) → ∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(dom 𝑦𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢))
138 sseq1 3823 . . . . . . . . . . . . . . . . . . 19 (𝑎 = dom 𝑦 → (𝑎𝑏 ↔ dom 𝑦𝑏))
139138rspceaimv 3510 . . . . . . . . . . . . . . . . . 18 ((dom 𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ ∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(dom 𝑦𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢))
14039, 137, 139syl2anc 575 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣))) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢))
141140rexlimdvaa 3220 . . . . . . . . . . . . . . . 16 (((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) → (∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢)))
14226, 141embantd 59 . . . . . . . . . . . . . . 15 (((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) → ((𝑥𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢)))
1431423expia 1143 . . . . . . . . . . . . . 14 (((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺))) → ((𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢) → ((𝑥𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢))))
144143anassrs 455 . . . . . . . . . . . . 13 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ 𝑣 ∈ (TopOpen‘𝐺)) ∧ 𝑡 ∈ (TopOpen‘𝐺)) → ((𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢) → ((𝑥𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢))))
145144rexlimdva 3219 . . . . . . . . . . . 12 (((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ 𝑣 ∈ (TopOpen‘𝐺)) → (∃𝑡 ∈ (TopOpen‘𝐺)(𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢) → ((𝑥𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢))))
146145com23 86 . . . . . . . . . . 11 (((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ 𝑣 ∈ (TopOpen‘𝐺)) → ((𝑥𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) → (∃𝑡 ∈ (TopOpen‘𝐺)(𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢))))
147146impd 398 . . . . . . . . . 10 (((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ 𝑣 ∈ (TopOpen‘𝐺)) → (((𝑥𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ ∃𝑡 ∈ (TopOpen‘𝐺)(𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢)))
148147rexlimdva 3219 . . . . . . . . 9 ((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) → (∃𝑣 ∈ (TopOpen‘𝐺)((𝑥𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ ∃𝑡 ∈ (TopOpen‘𝐺)(𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢)))
14925, 148syl5 34 . . . . . . . 8 ((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) → ((∀𝑣 ∈ (TopOpen‘𝐺)(𝑥𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ ∃𝑣 ∈ (TopOpen‘𝐺)∃𝑡 ∈ (TopOpen‘𝐺)(𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢)))
15024, 149mpan2d 677 . . . . . . 7 ((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) → (∀𝑣 ∈ (TopOpen‘𝐺)(𝑥𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢)))
1511503expia 1143 . . . . . 6 ((𝜑𝑢 ∈ (TopOpen‘𝐺)) → (𝑥𝑢 → (∀𝑣 ∈ (TopOpen‘𝐺)(𝑥𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢))))
152151com23 86 . . . . 5 ((𝜑𝑢 ∈ (TopOpen‘𝐺)) → (∀𝑣 ∈ (TopOpen‘𝐺)(𝑥𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) → (𝑥𝑢 → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢))))
153152ralrimdva 3157 . . . 4 (𝜑 → (∀𝑣 ∈ (TopOpen‘𝐺)(𝑥𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) → ∀𝑢 ∈ (TopOpen‘𝐺)(𝑥𝑢 → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢))))
154153anim2d 601 . . 3 (𝜑 → ((𝑥𝐵 ∧ ∀𝑣 ∈ (TopOpen‘𝐺)(𝑥𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣))) → (𝑥𝐵 ∧ ∀𝑢 ∈ (TopOpen‘𝐺)(𝑥𝑢 → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢)))))
155 eqid 2806 . . . 4 (𝒫 (𝐴 × 𝐶) ∩ Fin) = (𝒫 (𝐴 × 𝐶) ∩ Fin)
156 tgptps 22094 . . . . 5 (𝐺 ∈ TopGrp → 𝐺 ∈ TopSp)
1571, 156syl 17 . . . 4 (𝜑𝐺 ∈ TopSp)
158 xpexg 7186 . . . . 5 ((𝐴𝑉𝐶𝑊) → (𝐴 × 𝐶) ∈ V)
15962, 64, 158syl2anc 575 . . . 4 (𝜑 → (𝐴 × 𝐶) ∈ V)
1607, 6, 155, 42, 157, 159, 66eltsms 22146 . . 3 (𝜑 → (𝑥 ∈ (𝐺 tsums 𝐹) ↔ (𝑥𝐵 ∧ ∀𝑣 ∈ (TopOpen‘𝐺)(𝑥𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)))))
161 eqid 2806 . . . 4 (𝒫 𝐴 ∩ Fin) = (𝒫 𝐴 ∩ Fin)
1627, 6, 161, 42, 157, 62, 68eltsms 22146 . . 3 (𝜑 → (𝑥 ∈ (𝐺 tsums 𝐻) ↔ (𝑥𝐵 ∧ ∀𝑢 ∈ (TopOpen‘𝐺)(𝑥𝑢 → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢)))))
163154, 160, 1623imtr4d 285 . 2 (𝜑 → (𝑥 ∈ (𝐺 tsums 𝐹) → 𝑥 ∈ (𝐺 tsums 𝐻)))
164163ssrdv 3804 1 (𝜑 → (𝐺 tsums 𝐹) ⊆ (𝐺 tsums 𝐻))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100   = wceq 1637  wcel 2156  wral 3096  wrex 3097  Vcvv 3391  cin 3768  wss 3769  𝒫 cpw 4351  {csn 4370  cmpt 4923   × cxp 5309  dom cdm 5311  ran crn 5312  cres 5313  Rel wrel 5316  wf 6093  cfv 6097  (class class class)co 6870  𝑚 cmap 8088  Fincfn 8188  0cn0 11555  chash 13333  Basecbs 16064  +gcplusg 16149  TopOpenctopn 16283  0gc0g 16301   Σg cgsu 16302  Mndcmnd 17495  -gcsg 17625  .gcmg 17741  CMndccmn 18390  TopOnctopon 20925  TopSpctps 20947  TopMndctmd 22084  TopGrpctgp 22085   tsums ctsu 22139
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-rep 4964  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7175  ax-inf2 8781  ax-cnex 10273  ax-resscn 10274  ax-1cn 10275  ax-icn 10276  ax-addcl 10277  ax-addrcl 10278  ax-mulcl 10279  ax-mulrcl 10280  ax-mulcom 10281  ax-addass 10282  ax-mulass 10283  ax-distr 10284  ax-i2m1 10285  ax-1ne0 10286  ax-1rid 10287  ax-rnegex 10288  ax-rrecex 10289  ax-cnre 10290  ax-pre-lttri 10291  ax-pre-lttrn 10292  ax-pre-ltadd 10293  ax-pre-mulgt0 10294
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-nel 3082  df-ral 3101  df-rex 3102  df-reu 3103  df-rmo 3104  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-int 4670  df-iun 4714  df-iin 4715  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-se 5271  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942  df-iota 6060  df-fun 6099  df-fn 6100  df-f 6101  df-f1 6102  df-fo 6103  df-f1o 6104  df-fv 6105  df-isom 6106  df-riota 6831  df-ov 6873  df-oprab 6874  df-mpt2 6875  df-of 7123  df-om 7292  df-1st 7394  df-2nd 7395  df-supp 7526  df-wrecs 7638  df-recs 7700  df-rdg 7738  df-1o 7792  df-2o 7793  df-oadd 7796  df-er 7975  df-map 8090  df-ixp 8142  df-en 8189  df-dom 8190  df-sdom 8191  df-fin 8192  df-fsupp 8511  df-fi 8552  df-oi 8650  df-card 9044  df-pnf 10357  df-mnf 10358  df-xr 10359  df-ltxr 10360  df-le 10361  df-sub 10549  df-neg 10550  df-nn 11302  df-2 11360  df-n0 11556  df-z 11640  df-uz 11901  df-fz 12546  df-fzo 12686  df-seq 13021  df-hash 13334  df-ndx 16067  df-slot 16068  df-base 16070  df-sets 16071  df-ress 16072  df-plusg 16162  df-rest 16284  df-0g 16303  df-gsum 16304  df-topgen 16305  df-pt 16306  df-mre 16447  df-mrc 16448  df-acs 16450  df-plusf 17442  df-mgm 17443  df-sgrp 17485  df-mnd 17496  df-mhm 17536  df-submnd 17537  df-grp 17626  df-minusg 17627  df-sbg 17628  df-mulg 17742  df-ghm 17856  df-cntz 17947  df-cmn 18392  df-abl 18393  df-fbas 19947  df-fg 19948  df-top 20909  df-topon 20926  df-topsp 20948  df-bases 20961  df-ntr 21035  df-nei 21113  df-cn 21242  df-cnp 21243  df-cmp 21401  df-tx 21576  df-xko 21577  df-hmeo 21769  df-fil 21860  df-fm 21952  df-flim 21953  df-flf 21954  df-tmd 22086  df-tgp 22087  df-tsms 22140
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator