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

Theorem tsmsxp 24103
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 24101 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 24027 . . . . . . . . . . 11 (𝐺 ∈ TopGrp → 𝐺 ∈ TopMnd)
31, 2syl 17 . . . . . . . . . 10 (𝜑𝐺 ∈ TopMnd)
433ad2ant1 1130 . . . . . . . . 9 ((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) → 𝐺 ∈ TopMnd)
5 simp2 1134 . . . . . . . . 9 ((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) → 𝑢 ∈ (TopOpen‘𝐺))
6 eqid 2725 . . . . . . . . . . . . 13 (TopOpen‘𝐺) = (TopOpen‘𝐺)
7 tsmsxp.b . . . . . . . . . . . . 13 𝐵 = (Base‘𝐺)
86, 7tmdtopon 24029 . . . . . . . . . . . 12 (𝐺 ∈ TopMnd → (TopOpen‘𝐺) ∈ (TopOn‘𝐵))
94, 8syl 17 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) → (TopOpen‘𝐺) ∈ (TopOn‘𝐵))
10 toponss 22873 . . . . . . . . . . 11 (((TopOpen‘𝐺) ∈ (TopOn‘𝐵) ∧ 𝑢 ∈ (TopOpen‘𝐺)) → 𝑢𝐵)
119, 5, 10syl2anc 582 . . . . . . . . . 10 ((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) → 𝑢𝐵)
12 simp3 1135 . . . . . . . . . 10 ((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) → 𝑥𝑢)
1311, 12sseldd 3977 . . . . . . . . 9 ((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) → 𝑥𝐵)
14 tmdmnd 24023 . . . . . . . . . . 11 (𝐺 ∈ TopMnd → 𝐺 ∈ Mnd)
154, 14syl 17 . . . . . . . . . 10 ((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) → 𝐺 ∈ Mnd)
16 eqid 2725 . . . . . . . . . . 11 (0g𝐺) = (0g𝐺)
177, 16mndidcl 18712 . . . . . . . . . 10 (𝐺 ∈ Mnd → (0g𝐺) ∈ 𝐵)
1815, 17syl 17 . . . . . . . . 9 ((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) → (0g𝐺) ∈ 𝐵)
19 eqid 2725 . . . . . . . . . . . 12 (+g𝐺) = (+g𝐺)
207, 19, 16mndrid 18718 . . . . . . . . . . 11 ((𝐺 ∈ Mnd ∧ 𝑥𝐵) → (𝑥(+g𝐺)(0g𝐺)) = 𝑥)
2115, 13, 20syl2anc 582 . . . . . . . . . 10 ((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) → (𝑥(+g𝐺)(0g𝐺)) = 𝑥)
2221, 12eqeltrd 2825 . . . . . . . . 9 ((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) → (𝑥(+g𝐺)(0g𝐺)) ∈ 𝑢)
237, 6, 19tmdcn2 24037 . . . . . . . . 9 (((𝐺 ∈ TopMnd ∧ 𝑢 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝐵 ∧ (0g𝐺) ∈ 𝐵 ∧ (𝑥(+g𝐺)(0g𝐺)) ∈ 𝑢)) → ∃𝑣 ∈ (TopOpen‘𝐺)∃𝑡 ∈ (TopOpen‘𝐺)(𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢))
244, 5, 13, 18, 22, 23syl23anc 1374 . . . . . . . 8 ((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) → ∃𝑣 ∈ (TopOpen‘𝐺)∃𝑡 ∈ (TopOpen‘𝐺)(𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢))
25 r19.29 3103 . . . . . . . . 9 ((∀𝑣 ∈ (TopOpen‘𝐺)(𝑥𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ ∃𝑣 ∈ (TopOpen‘𝐺)∃𝑡 ∈ (TopOpen‘𝐺)(𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) → ∃𝑣 ∈ (TopOpen‘𝐺)((𝑥𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ ∃𝑡 ∈ (TopOpen‘𝐺)(𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)))
26 simp31 1206 . . . . . . . . . . . . . . 15 (((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) → 𝑥𝑣)
27 elfpw 9380 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ↔ (𝑦 ⊆ (𝐴 × 𝐶) ∧ 𝑦 ∈ Fin))
2827simplbi 496 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) → 𝑦 ⊆ (𝐴 × 𝐶))
2928ad2antrl 726 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣))) → 𝑦 ⊆ (𝐴 × 𝐶))
30 dmss 5905 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ⊆ (𝐴 × 𝐶) → dom 𝑦 ⊆ dom (𝐴 × 𝐶))
3129, 30syl 17 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣))) → dom 𝑦 ⊆ dom (𝐴 × 𝐶))
32 dmxpss 6177 . . . . . . . . . . . . . . . . . . 19 dom (𝐴 × 𝐶) ⊆ 𝐴
3331, 32sstrdi 3989 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣))) → dom 𝑦𝐴)
34 elinel2 4194 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) → 𝑦 ∈ Fin)
3534ad2antrl 726 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣))) → 𝑦 ∈ Fin)
36 dmfi 9356 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ Fin → dom 𝑦 ∈ Fin)
3735, 36syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣))) → dom 𝑦 ∈ Fin)
38 elfpw 9380 . . . . . . . . . . . . . . . . . 18 (dom 𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↔ (dom 𝑦𝐴 ∧ dom 𝑦 ∈ Fin))
3933, 37, 38sylanbrc 581 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣))) → dom 𝑦 ∈ (𝒫 𝐴 ∩ Fin))
40 eqid 2725 . . . . . . . . . . . . . . . . . . . . . 22 (.g𝐺) = (.g𝐺)
41 simpl11 1245 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏))) → 𝜑)
42 tsmsxp.g . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐺 ∈ CMnd)
4341, 42syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏))) → 𝐺 ∈ CMnd)
4441, 3syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏))) → 𝐺 ∈ TopMnd)
45 simprrl 779 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏))) → 𝑏 ∈ (𝒫 𝐴 ∩ Fin))
4645elin2d 4197 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏))) → 𝑏 ∈ Fin)
47 simpl2r 1224 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏))) → 𝑡 ∈ (TopOpen‘𝐺))
4844, 14syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏))) → 𝐺 ∈ Mnd)
4948, 17syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏))) → (0g𝐺) ∈ 𝐵)
50 hashcl 14351 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑏 ∈ Fin → (♯‘𝑏) ∈ ℕ0)
5146, 50syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏))) → (♯‘𝑏) ∈ ℕ0)
527, 40, 16mulgnn0z 19064 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐺 ∈ Mnd ∧ (♯‘𝑏) ∈ ℕ0) → ((♯‘𝑏)(.g𝐺)(0g𝐺)) = (0g𝐺))
5348, 51, 52syl2anc 582 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏))) → ((♯‘𝑏)(.g𝐺)(0g𝐺)) = (0g𝐺))
54 simpl32 1252 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏))) → (0g𝐺) ∈ 𝑡)
5553, 54eqeltrd 2825 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏))) → ((♯‘𝑏)(.g𝐺)(0g𝐺)) ∈ 𝑡)
566, 7, 40, 43, 44, 46, 47, 49, 55tmdgsum2 24044 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏))) → ∃𝑠 ∈ (TopOpen‘𝐺)((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠m 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡))
57 simp111 1299 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠m 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡))) → 𝜑)
5857, 42syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠m 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡))) → 𝐺 ∈ CMnd)
5957, 1syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠m 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡))) → 𝐺 ∈ TopGrp)
60 tsmsxp.a . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐴𝑉)
6157, 60syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠m 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡))) → 𝐴𝑉)
62 tsmsxp.c . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐶𝑊)
6357, 62syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠m 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡))) → 𝐶𝑊)
64 tsmsxp.f . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐹:(𝐴 × 𝐶)⟶𝐵)
6557, 64syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠m 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡))) → 𝐹:(𝐴 × 𝐶)⟶𝐵)
66 tsmsxp.h . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐻:𝐴𝐵)
6757, 66syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠m 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡))) → 𝐻:𝐴𝐵)
68 tsmsxp.1 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗𝐴) → (𝐻𝑗) ∈ (𝐺 tsums (𝑘𝐶 ↦ (𝑗𝐹𝑘))))
6957, 68sylan 578 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠m 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡))) ∧ 𝑗𝐴) → (𝐻𝑗) ∈ (𝐺 tsums (𝑘𝐶 ↦ (𝑗𝐹𝑘))))
70 eqid 2725 . . . . . . . . . . . . . . . . . . . . . . . 24 (-g𝐺) = (-g𝐺)
71 simp3l 1198 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠m 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡))) → 𝑠 ∈ (TopOpen‘𝐺))
72 simp3rl 1243 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠m 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡))) → (0g𝐺) ∈ 𝑠)
73 simp2rl 1239 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠m 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡))) → 𝑏 ∈ (𝒫 𝐴 ∩ Fin))
74 simp2rr 1240 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠m 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡))) → dom 𝑦𝑏)
75 simp2ll 1237 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠m 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡))) → 𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin))
767, 58, 59, 61, 63, 65, 67, 69, 6, 16, 19, 70, 71, 72, 73, 74, 75tsmsxplem1 24101 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠m 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡))) → ∃𝑛 ∈ (𝒫 𝐶 ∩ Fin)(ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠))
77433adant3 1129 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠m 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝐺 ∈ CMnd)
78593adant3r 1178 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠m 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝐺 ∈ TopGrp)
79613adant3r 1178 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠m 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝐴𝑉)
80633adant3r 1178 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠m 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝐶𝑊)
81653adant3r 1178 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠m 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝐹:(𝐴 × 𝐶)⟶𝐵)
82673adant3r 1178 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠m 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝐻:𝐴𝐵)
83413adant3 1129 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠m 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝜑)
8483, 68sylan 578 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠m 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) ∧ 𝑗𝐴) → (𝐻𝑗) ∈ (𝐺 tsums (𝑘𝐶 ↦ (𝑗𝐹𝑘))))
85 simp3ll 1241 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠m 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝑠 ∈ (TopOpen‘𝐺))
86723adant3r 1178 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠m 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → (0g𝐺) ∈ 𝑠)
87 simp2rl 1239 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠m 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝑏 ∈ (𝒫 𝐴 ∩ Fin))
88 simp133 1307 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠m 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)
89 simp3rl 1243 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠m 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝑛 ∈ (𝒫 𝐶 ∩ Fin))
90 simp2ll 1237 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠m 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin))
91 simp2rr 1240 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠m 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → dom 𝑦𝑏)
92 simp3rr 1244 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠m 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠))
9392simpld 493 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠m 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → ran 𝑦𝑛)
94 relxp 5696 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Rel (𝐴 × 𝐶)
95 relss 5783 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 ⊆ (𝐴 × 𝐶) → (Rel (𝐴 × 𝐶) → Rel 𝑦))
9628, 94, 95mpisyl 21 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) → Rel 𝑦)
97 relssdmrn 6274 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (Rel 𝑦𝑦 ⊆ (dom 𝑦 × ran 𝑦))
9896, 97syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) → 𝑦 ⊆ (dom 𝑦 × ran 𝑦))
99 xpss12 5693 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((dom 𝑦𝑏 ∧ ran 𝑦𝑛) → (dom 𝑦 × ran 𝑦) ⊆ (𝑏 × 𝑛))
10098, 99sylan9ss 3990 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ (dom 𝑦𝑏 ∧ ran 𝑦𝑛)) → 𝑦 ⊆ (𝑏 × 𝑛))
10190, 91, 93, 100syl12anc 835 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠m 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝑦 ⊆ (𝑏 × 𝑛))
10292simprd 494 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠m 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)
103 sseq2 4003 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑧 = (𝑏 × 𝑛) → (𝑦𝑧𝑦 ⊆ (𝑏 × 𝑛)))
104 reseq2 5980 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑧 = (𝑏 × 𝑛) → (𝐹𝑧) = (𝐹 ↾ (𝑏 × 𝑛)))
105104oveq2d 7435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑧 = (𝑏 × 𝑛) → (𝐺 Σg (𝐹𝑧)) = (𝐺 Σg (𝐹 ↾ (𝑏 × 𝑛))))
106105eleq1d 2810 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑧 = (𝑏 × 𝑛) → ((𝐺 Σg (𝐹𝑧)) ∈ 𝑣 ↔ (𝐺 Σg (𝐹 ↾ (𝑏 × 𝑛))) ∈ 𝑣))
107103, 106imbi12d 343 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧 = (𝑏 × 𝑛) → ((𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣) ↔ (𝑦 ⊆ (𝑏 × 𝑛) → (𝐺 Σg (𝐹 ↾ (𝑏 × 𝑛))) ∈ 𝑣)))
108 simp2lr 1238 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠m 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣))
109 elfpw 9380 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝑏𝐴𝑏 ∈ Fin))
110 elfpw 9380 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ↔ (𝑛𝐶𝑛 ∈ Fin))
111 xpss12 5693 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑏𝐴𝑛𝐶) → (𝑏 × 𝑛) ⊆ (𝐴 × 𝐶))
112 xpfi 9343 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑏 ∈ Fin ∧ 𝑛 ∈ Fin) → (𝑏 × 𝑛) ∈ Fin)
113111, 112anim12i 611 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑏𝐴𝑛𝐶) ∧ (𝑏 ∈ Fin ∧ 𝑛 ∈ Fin)) → ((𝑏 × 𝑛) ⊆ (𝐴 × 𝐶) ∧ (𝑏 × 𝑛) ∈ Fin))
114113an4s 658 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑏𝐴𝑏 ∈ Fin) ∧ (𝑛𝐶𝑛 ∈ Fin)) → ((𝑏 × 𝑛) ⊆ (𝐴 × 𝐶) ∧ (𝑏 × 𝑛) ∈ Fin))
115109, 110, 114syl2anb 596 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑛 ∈ (𝒫 𝐶 ∩ Fin)) → ((𝑏 × 𝑛) ⊆ (𝐴 × 𝐶) ∧ (𝑏 × 𝑛) ∈ Fin))
116 elfpw 9380 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑏 × 𝑛) ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ↔ ((𝑏 × 𝑛) ⊆ (𝐴 × 𝐶) ∧ (𝑏 × 𝑛) ∈ Fin))
117115, 116sylibr 233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑛 ∈ (𝒫 𝐶 ∩ Fin)) → (𝑏 × 𝑛) ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin))
11887, 89, 117syl2anc 582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠m 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → (𝑏 × 𝑛) ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin))
119107, 108, 118rspcdva 3607 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠m 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → (𝑦 ⊆ (𝑏 × 𝑛) → (𝐺 Σg (𝐹 ↾ (𝑏 × 𝑛))) ∈ 𝑣))
120101, 119mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠m 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → (𝐺 Σg (𝐹 ↾ (𝑏 × 𝑛))) ∈ 𝑣)
121 simp3lr 1242 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠m 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠m 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡))
122121simprd 494 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠m 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → ∀𝑔 ∈ (𝑠m 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)
123 oveq2 7427 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑔 = → (𝐺 Σg 𝑔) = (𝐺 Σg ))
124123eleq1d 2810 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑔 = → ((𝐺 Σg 𝑔) ∈ 𝑡 ↔ (𝐺 Σg ) ∈ 𝑡))
125124cbvralvw 3224 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∀𝑔 ∈ (𝑠m 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡 ↔ ∀ ∈ (𝑠m 𝑏)(𝐺 Σg ) ∈ 𝑡)
126122, 125sylib 217 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠m 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → ∀ ∈ (𝑠m 𝑏)(𝐺 Σg ) ∈ 𝑡)
1277, 77, 78, 79, 80, 81, 82, 84, 6, 16, 19, 70, 85, 86, 87, 88, 89, 101, 102, 120, 126tsmsxplem2 24102 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠m 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢)
1281273exp 1116 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) → (((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) → (((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠m 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠))) → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢)))
129128exp4a 430 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) → (((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) → ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠m 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) → ((𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)) → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢))))
1301293imp1 1344 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠m 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡))) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠))) → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢)
13176, 130rexlimddv 3150 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠m 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡))) → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢)
1321313expa 1115 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏))) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠m 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡))) → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢)
13356, 132rexlimddv 3150 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏))) → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢)
134133anassrs 466 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣))) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢)
135134expr 455 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣))) ∧ 𝑏 ∈ (𝒫 𝐴 ∩ Fin)) → (dom 𝑦𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢))
136135ralrimiva 3135 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣))) → ∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(dom 𝑦𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢))
137 sseq1 4002 . . . . . . . . . . . . . . . . . 18 (𝑎 = dom 𝑦 → (𝑎𝑏 ↔ dom 𝑦𝑏))
138137rspceaimv 3612 . . . . . . . . . . . . . . . . 17 ((dom 𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ ∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(dom 𝑦𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢))
13939, 136, 138syl2anc 582 . . . . . . . . . . . . . . . 16 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣))) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢))
140139rexlimdvaa 3145 . . . . . . . . . . . . . . 15 (((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) → (∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢)))
14126, 140embantd 59 . . . . . . . . . . . . . 14 (((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) → ((𝑥𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢)))
1421413expia 1118 . . . . . . . . . . . . 13 (((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺))) → ((𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢) → ((𝑥𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢))))
143142anassrs 466 . . . . . . . . . . . 12 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ 𝑣 ∈ (TopOpen‘𝐺)) ∧ 𝑡 ∈ (TopOpen‘𝐺)) → ((𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢) → ((𝑥𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢))))
144143rexlimdva 3144 . . . . . . . . . . 11 (((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ 𝑣 ∈ (TopOpen‘𝐺)) → (∃𝑡 ∈ (TopOpen‘𝐺)(𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢) → ((𝑥𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢))))
145144impcomd 410 . . . . . . . . . 10 (((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ 𝑣 ∈ (TopOpen‘𝐺)) → (((𝑥𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ ∃𝑡 ∈ (TopOpen‘𝐺)(𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢)))
146145rexlimdva 3144 . . . . . . . . 9 ((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) → (∃𝑣 ∈ (TopOpen‘𝐺)((𝑥𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ ∃𝑡 ∈ (TopOpen‘𝐺)(𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢)))
14725, 146syl5 34 . . . . . . . 8 ((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) → ((∀𝑣 ∈ (TopOpen‘𝐺)(𝑥𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ ∃𝑣 ∈ (TopOpen‘𝐺)∃𝑡 ∈ (TopOpen‘𝐺)(𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢)))
14824, 147mpan2d 692 . . . . . . 7 ((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) → (∀𝑣 ∈ (TopOpen‘𝐺)(𝑥𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢)))
1491483expia 1118 . . . . . 6 ((𝜑𝑢 ∈ (TopOpen‘𝐺)) → (𝑥𝑢 → (∀𝑣 ∈ (TopOpen‘𝐺)(𝑥𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢))))
150149com23 86 . . . . 5 ((𝜑𝑢 ∈ (TopOpen‘𝐺)) → (∀𝑣 ∈ (TopOpen‘𝐺)(𝑥𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) → (𝑥𝑢 → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢))))
151150ralrimdva 3143 . . . 4 (𝜑 → (∀𝑣 ∈ (TopOpen‘𝐺)(𝑥𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) → ∀𝑢 ∈ (TopOpen‘𝐺)(𝑥𝑢 → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢))))
152151anim2d 610 . . 3 (𝜑 → ((𝑥𝐵 ∧ ∀𝑣 ∈ (TopOpen‘𝐺)(𝑥𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣))) → (𝑥𝐵 ∧ ∀𝑢 ∈ (TopOpen‘𝐺)(𝑥𝑢 → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢)))))
153 eqid 2725 . . . 4 (𝒫 (𝐴 × 𝐶) ∩ Fin) = (𝒫 (𝐴 × 𝐶) ∩ Fin)
154 tgptps 24028 . . . . 5 (𝐺 ∈ TopGrp → 𝐺 ∈ TopSp)
1551, 154syl 17 . . . 4 (𝜑𝐺 ∈ TopSp)
15660, 62xpexd 7754 . . . 4 (𝜑 → (𝐴 × 𝐶) ∈ V)
1577, 6, 153, 42, 155, 156, 64eltsms 24081 . . 3 (𝜑 → (𝑥 ∈ (𝐺 tsums 𝐹) ↔ (𝑥𝐵 ∧ ∀𝑣 ∈ (TopOpen‘𝐺)(𝑥𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)))))
158 eqid 2725 . . . 4 (𝒫 𝐴 ∩ Fin) = (𝒫 𝐴 ∩ Fin)
1597, 6, 158, 42, 155, 60, 66eltsms 24081 . . 3 (𝜑 → (𝑥 ∈ (𝐺 tsums 𝐻) ↔ (𝑥𝐵 ∧ ∀𝑢 ∈ (TopOpen‘𝐺)(𝑥𝑢 → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢)))))
160152, 157, 1593imtr4d 293 . 2 (𝜑 → (𝑥 ∈ (𝐺 tsums 𝐹) → 𝑥 ∈ (𝐺 tsums 𝐻)))
161160ssrdv 3982 1 (𝜑 → (𝐺 tsums 𝐹) ⊆ (𝐺 tsums 𝐻))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  w3a 1084   = wceq 1533  wcel 2098  wral 3050  wrex 3059  Vcvv 3461  cin 3943  wss 3944  𝒫 cpw 4604  {csn 4630  cmpt 5232   × cxp 5676  dom cdm 5678  ran crn 5679  cres 5680  Rel wrel 5683  wf 6545  cfv 6549  (class class class)co 7419  m cmap 8845  Fincfn 8964  0cn0 12505  chash 14325  Basecbs 17183  +gcplusg 17236  TopOpenctopn 17406  0gc0g 17424   Σg cgsu 17425  Mndcmnd 18697  -gcsg 18900  .gcmg 19031  CMndccmn 19747  TopOnctopon 22856  TopSpctps 22878  TopMndctmd 24018  TopGrpctgp 24019   tsums ctsu 24074
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741  ax-cnex 11196  ax-resscn 11197  ax-1cn 11198  ax-icn 11199  ax-addcl 11200  ax-addrcl 11201  ax-mulcl 11202  ax-mulrcl 11203  ax-mulcom 11204  ax-addass 11205  ax-mulass 11206  ax-distr 11207  ax-i2m1 11208  ax-1ne0 11209  ax-1rid 11210  ax-rnegex 11211  ax-rrecex 11212  ax-cnre 11213  ax-pre-lttri 11214  ax-pre-lttrn 11215  ax-pre-ltadd 11216  ax-pre-mulgt0 11217
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3363  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3964  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-int 4951  df-iun 4999  df-iin 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-se 5634  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6307  df-ord 6374  df-on 6375  df-lim 6376  df-suc 6377  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-isom 6558  df-riota 7375  df-ov 7422  df-oprab 7423  df-mpo 7424  df-of 7685  df-om 7872  df-1st 7994  df-2nd 7995  df-supp 8166  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-1o 8487  df-er 8725  df-map 8847  df-ixp 8917  df-en 8965  df-dom 8966  df-sdom 8967  df-fin 8968  df-fsupp 9388  df-fi 9436  df-oi 9535  df-card 9964  df-pnf 11282  df-mnf 11283  df-xr 11284  df-ltxr 11285  df-le 11286  df-sub 11478  df-neg 11479  df-nn 12246  df-2 12308  df-n0 12506  df-z 12592  df-uz 12856  df-fz 13520  df-fzo 13663  df-seq 14003  df-hash 14326  df-sets 17136  df-slot 17154  df-ndx 17166  df-base 17184  df-ress 17213  df-plusg 17249  df-rest 17407  df-0g 17426  df-gsum 17427  df-topgen 17428  df-pt 17429  df-mre 17569  df-mrc 17570  df-acs 17572  df-plusf 18602  df-mgm 18603  df-sgrp 18682  df-mnd 18698  df-mhm 18743  df-submnd 18744  df-grp 18901  df-minusg 18902  df-sbg 18903  df-mulg 19032  df-ghm 19176  df-cntz 19280  df-cmn 19749  df-abl 19750  df-fbas 21293  df-fg 21294  df-top 22840  df-topon 22857  df-topsp 22879  df-bases 22893  df-ntr 22968  df-nei 23046  df-cn 23175  df-cnp 23176  df-cmp 23335  df-tx 23510  df-xko 23511  df-hmeo 23703  df-fil 23794  df-fm 23886  df-flim 23887  df-flf 23888  df-tmd 24020  df-tgp 24021  df-tsms 24075
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator