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

Theorem tsmsxp 21868
Description: Write a sum over a two-dimensional region as a double sum. This infinite group sum version of gsumxp 18296 is also known as Fubini's theorem. The converse is not necessarily true without additional assumptions. See tsmsxplem1 21866 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 21793 . . . . . . . . . . 11 (𝐺 ∈ TopGrp → 𝐺 ∈ TopMnd)
31, 2syl 17 . . . . . . . . . 10 (𝜑𝐺 ∈ TopMnd)
433ad2ant1 1080 . . . . . . . . 9 ((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) → 𝐺 ∈ TopMnd)
5 simp2 1060 . . . . . . . . 9 ((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) → 𝑢 ∈ (TopOpen‘𝐺))
6 eqid 2621 . . . . . . . . . . . . 13 (TopOpen‘𝐺) = (TopOpen‘𝐺)
7 tsmsxp.b . . . . . . . . . . . . 13 𝐵 = (Base‘𝐺)
86, 7tmdtopon 21795 . . . . . . . . . . . 12 (𝐺 ∈ TopMnd → (TopOpen‘𝐺) ∈ (TopOn‘𝐵))
94, 8syl 17 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) → (TopOpen‘𝐺) ∈ (TopOn‘𝐵))
10 toponss 20644 . . . . . . . . . . 11 (((TopOpen‘𝐺) ∈ (TopOn‘𝐵) ∧ 𝑢 ∈ (TopOpen‘𝐺)) → 𝑢𝐵)
119, 5, 10syl2anc 692 . . . . . . . . . 10 ((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) → 𝑢𝐵)
12 simp3 1061 . . . . . . . . . 10 ((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) → 𝑥𝑢)
1311, 12sseldd 3584 . . . . . . . . 9 ((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) → 𝑥𝐵)
14 tmdmnd 21789 . . . . . . . . . . 11 (𝐺 ∈ TopMnd → 𝐺 ∈ Mnd)
154, 14syl 17 . . . . . . . . . 10 ((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) → 𝐺 ∈ Mnd)
16 eqid 2621 . . . . . . . . . . 11 (0g𝐺) = (0g𝐺)
177, 16mndidcl 17229 . . . . . . . . . 10 (𝐺 ∈ Mnd → (0g𝐺) ∈ 𝐵)
1815, 17syl 17 . . . . . . . . 9 ((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) → (0g𝐺) ∈ 𝐵)
19 eqid 2621 . . . . . . . . . . . 12 (+g𝐺) = (+g𝐺)
207, 19, 16mndrid 17233 . . . . . . . . . . 11 ((𝐺 ∈ Mnd ∧ 𝑥𝐵) → (𝑥(+g𝐺)(0g𝐺)) = 𝑥)
2115, 13, 20syl2anc 692 . . . . . . . . . 10 ((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) → (𝑥(+g𝐺)(0g𝐺)) = 𝑥)
2221, 12eqeltrd 2698 . . . . . . . . 9 ((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) → (𝑥(+g𝐺)(0g𝐺)) ∈ 𝑢)
237, 6, 19tmdcn2 21803 . . . . . . . . 9 (((𝐺 ∈ TopMnd ∧ 𝑢 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝐵 ∧ (0g𝐺) ∈ 𝐵 ∧ (𝑥(+g𝐺)(0g𝐺)) ∈ 𝑢)) → ∃𝑣 ∈ (TopOpen‘𝐺)∃𝑡 ∈ (TopOpen‘𝐺)(𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢))
244, 5, 13, 18, 22, 23syl23anc 1330 . . . . . . . 8 ((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) → ∃𝑣 ∈ (TopOpen‘𝐺)∃𝑡 ∈ (TopOpen‘𝐺)(𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢))
25 r19.29 3065 . . . . . . . . 9 ((∀𝑣 ∈ (TopOpen‘𝐺)(𝑥𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ ∃𝑣 ∈ (TopOpen‘𝐺)∃𝑡 ∈ (TopOpen‘𝐺)(𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) → ∃𝑣 ∈ (TopOpen‘𝐺)((𝑥𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ ∃𝑡 ∈ (TopOpen‘𝐺)(𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)))
26 simp31 1095 . . . . . . . . . . . . . . . 16 (((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) → 𝑥𝑣)
27 elfpw 8212 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ↔ (𝑦 ⊆ (𝐴 × 𝐶) ∧ 𝑦 ∈ Fin))
2827simplbi 476 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) → 𝑦 ⊆ (𝐴 × 𝐶))
2928ad2antrl 763 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣))) → 𝑦 ⊆ (𝐴 × 𝐶))
30 dmss 5283 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ⊆ (𝐴 × 𝐶) → dom 𝑦 ⊆ dom (𝐴 × 𝐶))
3129, 30syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣))) → dom 𝑦 ⊆ dom (𝐴 × 𝐶))
32 dmxpss 5524 . . . . . . . . . . . . . . . . . . . 20 dom (𝐴 × 𝐶) ⊆ 𝐴
3331, 32syl6ss 3595 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣))) → dom 𝑦𝐴)
3427simprbi 480 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) → 𝑦 ∈ Fin)
3534ad2antrl 763 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣))) → 𝑦 ∈ Fin)
36 dmfi 8188 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ Fin → dom 𝑦 ∈ Fin)
3735, 36syl 17 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣))) → dom 𝑦 ∈ Fin)
38 elfpw 8212 . . . . . . . . . . . . . . . . . . 19 (dom 𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↔ (dom 𝑦𝐴 ∧ dom 𝑦 ∈ Fin))
3933, 37, 38sylanbrc 697 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣))) → dom 𝑦 ∈ (𝒫 𝐴 ∩ Fin))
40 eqid 2621 . . . . . . . . . . . . . . . . . . . . . . 23 (.g𝐺) = (.g𝐺)
41 simpl11 1134 . . . . . . . . . . . . . . . . . . . . . . . 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 803 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏))) → 𝑏 ∈ (𝒫 𝐴 ∩ Fin))
46 elfpw 8212 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝑏𝐴𝑏 ∈ Fin))
4746simprbi 480 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑏 ∈ (𝒫 𝐴 ∩ Fin) → 𝑏 ∈ Fin)
4845, 47syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏))) → 𝑏 ∈ Fin)
49 simpl2r 1113 . . . . . . . . . . . . . . . . . . . . . . 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 13087 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑏 ∈ Fin → (#‘𝑏) ∈ ℕ0)
5348, 52syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏))) → (#‘𝑏) ∈ ℕ0)
547, 40, 16mulgnn0z 17488 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐺 ∈ Mnd ∧ (#‘𝑏) ∈ ℕ0) → ((#‘𝑏)(.g𝐺)(0g𝐺)) = (0g𝐺))
5550, 53, 54syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏))) → ((#‘𝑏)(.g𝐺)(0g𝐺)) = (0g𝐺))
56 simpl32 1141 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏))) → (0g𝐺) ∈ 𝑡)
5755, 56eqeltrd 2698 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏))) → ((#‘𝑏)(.g𝐺)(0g𝐺)) ∈ 𝑡)
586, 7, 40, 43, 44, 48, 49, 51, 57tmdgsum2 21810 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏))) → ∃𝑠 ∈ (TopOpen‘𝐺)((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡))
59 simp111 1188 . . . . . . . . . . . . . . . . . . . . . . . . . 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 488 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡))) ∧ 𝑗𝐴) → (𝐻𝑗) ∈ (𝐺 tsums (𝑘𝐶 ↦ (𝑗𝐹𝑘))))
72 eqid 2621 . . . . . . . . . . . . . . . . . . . . . . . . 25 (-g𝐺) = (-g𝐺)
73 simp3l 1087 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡))) → 𝑠 ∈ (TopOpen‘𝐺))
74 simp3rl 1132 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡))) → (0g𝐺) ∈ 𝑠)
75 simp2rl 1128 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡))) → 𝑏 ∈ (𝒫 𝐴 ∩ Fin))
76 simp2rr 1129 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡))) → dom 𝑦𝑏)
77 simp2ll 1126 . . . . . . . . . . . . . . . . . . . . . . . . 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 21866 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡))) → ∃𝑛 ∈ (𝒫 𝐶 ∩ Fin)(ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠))
79433adant3 1079 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝐺 ∈ CMnd)
80613adant3r 1320 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝐺 ∈ TopGrp)
81633adant3r 1320 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝐴𝑉)
82653adant3r 1320 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝐶𝑊)
83673adant3r 1320 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝐹:(𝐴 × 𝐶)⟶𝐵)
84693adant3r 1320 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝐻:𝐴𝐵)
85413adant3 1079 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝜑)
8685, 70sylan 488 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) ∧ 𝑗𝐴) → (𝐻𝑗) ∈ (𝐺 tsums (𝑘𝐶 ↦ (𝑗𝐹𝑘))))
87 simp3ll 1130 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝑠 ∈ (TopOpen‘𝐺))
88743adant3r 1320 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → (0g𝐺) ∈ 𝑠)
89 simp2rl 1128 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝑏 ∈ (𝒫 𝐴 ∩ Fin))
90 simp133 1196 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)
91 simp3rl 1132 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝑛 ∈ (𝒫 𝐶 ∩ Fin))
92 simp2ll 1126 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin))
93 simp2rr 1129 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → dom 𝑦𝑏)
94 simp3rr 1133 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠))
9594simpld 475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → ran 𝑦𝑛)
96 relxp 5188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Rel (𝐴 × 𝐶)
97 relss 5167 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑦 ⊆ (𝐴 × 𝐶) → (Rel (𝐴 × 𝐶) → Rel 𝑦))
9828, 96, 97mpisyl 21 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) → Rel 𝑦)
99 relssdmrn 5615 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (Rel 𝑦𝑦 ⊆ (dom 𝑦 × ran 𝑦))
10098, 99syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) → 𝑦 ⊆ (dom 𝑦 × ran 𝑦))
101 xpss12 5186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((dom 𝑦𝑏 ∧ ran 𝑦𝑛) → (dom 𝑦 × ran 𝑦) ⊆ (𝑏 × 𝑛))
102100, 101sylan9ss 3596 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ (dom 𝑦𝑏 ∧ ran 𝑦𝑛)) → 𝑦 ⊆ (𝑏 × 𝑛))
10392, 93, 95, 102syl12anc 1321 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → 𝑦 ⊆ (𝑏 × 𝑛))
10494simprd 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)
105 elfpw 8212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ↔ (𝑛𝐶𝑛 ∈ Fin))
106 xpss12 5186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑏𝐴𝑛𝐶) → (𝑏 × 𝑛) ⊆ (𝐴 × 𝐶))
107 xpfi 8175 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑏 ∈ Fin ∧ 𝑛 ∈ Fin) → (𝑏 × 𝑛) ∈ Fin)
108106, 107anim12i 589 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑏𝐴𝑛𝐶) ∧ (𝑏 ∈ Fin ∧ 𝑛 ∈ Fin)) → ((𝑏 × 𝑛) ⊆ (𝐴 × 𝐶) ∧ (𝑏 × 𝑛) ∈ Fin))
109108an4s 868 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑏𝐴𝑏 ∈ Fin) ∧ (𝑛𝐶𝑛 ∈ Fin)) → ((𝑏 × 𝑛) ⊆ (𝐴 × 𝐶) ∧ (𝑏 × 𝑛) ∈ Fin))
11046, 105, 109syl2anb 496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑛 ∈ (𝒫 𝐶 ∩ Fin)) → ((𝑏 × 𝑛) ⊆ (𝐴 × 𝐶) ∧ (𝑏 × 𝑛) ∈ Fin))
111 elfpw 8212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑏 × 𝑛) ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ↔ ((𝑏 × 𝑛) ⊆ (𝐴 × 𝐶) ∧ (𝑏 × 𝑛) ∈ Fin))
112110, 111sylibr 224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑛 ∈ (𝒫 𝐶 ∩ Fin)) → (𝑏 × 𝑛) ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin))
11389, 91, 112syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → (𝑏 × 𝑛) ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin))
114 simp2lr 1127 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣))
115 sseq2 3606 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑧 = (𝑏 × 𝑛) → (𝑦𝑧𝑦 ⊆ (𝑏 × 𝑛)))
116 reseq2 5351 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧 = (𝑏 × 𝑛) → (𝐹𝑧) = (𝐹 ↾ (𝑏 × 𝑛)))
117116oveq2d 6620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑧 = (𝑏 × 𝑛) → (𝐺 Σg (𝐹𝑧)) = (𝐺 Σg (𝐹 ↾ (𝑏 × 𝑛))))
118117eleq1d 2683 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑧 = (𝑏 × 𝑛) → ((𝐺 Σg (𝐹𝑧)) ∈ 𝑣 ↔ (𝐺 Σg (𝐹 ↾ (𝑏 × 𝑛))) ∈ 𝑣))
119115, 118imbi12d 334 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑧 = (𝑏 × 𝑛) → ((𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣) ↔ (𝑦 ⊆ (𝑏 × 𝑛) → (𝐺 Σg (𝐹 ↾ (𝑏 × 𝑛))) ∈ 𝑣)))
120119rspcv 3291 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑏 × 𝑛) ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) → (∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣) → (𝑦 ⊆ (𝑏 × 𝑛) → (𝐺 Σg (𝐹 ↾ (𝑏 × 𝑛))) ∈ 𝑣)))
121113, 114, 103, 120syl3c 66 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → (𝐺 Σg (𝐹 ↾ (𝑏 × 𝑛))) ∈ 𝑣)
122 simp3lr 1131 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡))
123122simprd 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)
124 oveq2 6612 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑔 = → (𝐺 Σg 𝑔) = (𝐺 Σg ))
125124eleq1d 2683 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑔 = → ((𝐺 Σg 𝑔) ∈ 𝑡 ↔ (𝐺 Σg ) ∈ 𝑡))
126125cbvralv 3159 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡 ↔ ∀ ∈ (𝑠𝑚 𝑏)(𝐺 Σg ) ∈ 𝑡)
127123, 126sylib 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 21867 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)))) → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢)
1291283exp 1261 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) → (((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) → (((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠))) → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢)))
130129exp4a 632 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) → (((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) → ((𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡)) → ((𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠)) → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢))))
1311303imp1 1277 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡))) ∧ (𝑛 ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝑦𝑛 ∧ ∀𝑥𝑏 ((𝐻𝑥)(-g𝐺)(𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝑠))) → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢)
13278, 131rexlimddv 3028 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡))) → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢)
1331323expa 1262 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏))) ∧ (𝑠 ∈ (TopOpen‘𝐺) ∧ ((0g𝐺) ∈ 𝑠 ∧ ∀𝑔 ∈ (𝑠𝑚 𝑏)(𝐺 Σg 𝑔) ∈ 𝑡))) → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢)
13458, 133rexlimddv 3028 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ ((𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏))) → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢)
135134anassrs 679 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣))) ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ dom 𝑦𝑏)) → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢)
136135expr 642 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣))) ∧ 𝑏 ∈ (𝒫 𝐴 ∩ Fin)) → (dom 𝑦𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢))
137136ralrimiva 2960 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣))) → ∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(dom 𝑦𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢))
138 sseq1 3605 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = dom 𝑦 → (𝑎𝑏 ↔ dom 𝑦𝑏))
139138imbi1d 331 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = dom 𝑦 → ((𝑎𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢) ↔ (dom 𝑦𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢)))
140139ralbidv 2980 . . . . . . . . . . . . . . . . . . 19 (𝑎 = dom 𝑦 → (∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢) ↔ ∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(dom 𝑦𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢)))
141140rspcev 3295 . . . . . . . . . . . . . . . . . 18 ((dom 𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ ∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(dom 𝑦𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢))
14239, 137, 141syl2anc 692 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) ∧ (𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣))) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢))
143142rexlimdvaa 3025 . . . . . . . . . . . . . . . 16 (((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) → (∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢)))
14426, 143embantd 59 . . . . . . . . . . . . . . 15 (((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺)) ∧ (𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) → ((𝑥𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢)))
1451443expia 1264 . . . . . . . . . . . . . 14 (((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ (𝑣 ∈ (TopOpen‘𝐺) ∧ 𝑡 ∈ (TopOpen‘𝐺))) → ((𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢) → ((𝑥𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢))))
146145anassrs 679 . . . . . . . . . . . . 13 ((((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ 𝑣 ∈ (TopOpen‘𝐺)) ∧ 𝑡 ∈ (TopOpen‘𝐺)) → ((𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢) → ((𝑥𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢))))
147146rexlimdva 3024 . . . . . . . . . . . 12 (((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ 𝑣 ∈ (TopOpen‘𝐺)) → (∃𝑡 ∈ (TopOpen‘𝐺)(𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢) → ((𝑥𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢))))
148147com23 86 . . . . . . . . . . 11 (((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ 𝑣 ∈ (TopOpen‘𝐺)) → ((𝑥𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) → (∃𝑡 ∈ (TopOpen‘𝐺)(𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢))))
149148impd 447 . . . . . . . . . 10 (((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) ∧ 𝑣 ∈ (TopOpen‘𝐺)) → (((𝑥𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ ∃𝑡 ∈ (TopOpen‘𝐺)(𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢)))
150149rexlimdva 3024 . . . . . . . . 9 ((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) → (∃𝑣 ∈ (TopOpen‘𝐺)((𝑥𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ ∃𝑡 ∈ (TopOpen‘𝐺)(𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢)))
15125, 150syl5 34 . . . . . . . 8 ((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) → ((∀𝑣 ∈ (TopOpen‘𝐺)(𝑥𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) ∧ ∃𝑣 ∈ (TopOpen‘𝐺)∃𝑡 ∈ (TopOpen‘𝐺)(𝑥𝑣 ∧ (0g𝐺) ∈ 𝑡 ∧ ∀𝑐𝑣𝑑𝑡 (𝑐(+g𝐺)𝑑) ∈ 𝑢)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢)))
15224, 151mpan2d 709 . . . . . . 7 ((𝜑𝑢 ∈ (TopOpen‘𝐺) ∧ 𝑥𝑢) → (∀𝑣 ∈ (TopOpen‘𝐺)(𝑥𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢)))
1531523expia 1264 . . . . . 6 ((𝜑𝑢 ∈ (TopOpen‘𝐺)) → (𝑥𝑢 → (∀𝑣 ∈ (TopOpen‘𝐺)(𝑥𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢))))
154153com23 86 . . . . 5 ((𝜑𝑢 ∈ (TopOpen‘𝐺)) → (∀𝑣 ∈ (TopOpen‘𝐺)(𝑥𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) → (𝑥𝑢 → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢))))
155154ralrimdva 2963 . . . 4 (𝜑 → (∀𝑣 ∈ (TopOpen‘𝐺)(𝑥𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)) → ∀𝑢 ∈ (TopOpen‘𝐺)(𝑥𝑢 → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢))))
156155anim2d 588 . . 3 (𝜑 → ((𝑥𝐵 ∧ ∀𝑣 ∈ (TopOpen‘𝐺)(𝑥𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣))) → (𝑥𝐵 ∧ ∀𝑢 ∈ (TopOpen‘𝐺)(𝑥𝑢 → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢)))))
157 eqid 2621 . . . 4 (𝒫 (𝐴 × 𝐶) ∩ Fin) = (𝒫 (𝐴 × 𝐶) ∩ Fin)
158 tgptps 21794 . . . . 5 (𝐺 ∈ TopGrp → 𝐺 ∈ TopSp)
1591, 158syl 17 . . . 4 (𝜑𝐺 ∈ TopSp)
160 xpexg 6913 . . . . 5 ((𝐴𝑉𝐶𝑊) → (𝐴 × 𝐶) ∈ V)
16162, 64, 160syl2anc 692 . . . 4 (𝜑 → (𝐴 × 𝐶) ∈ V)
1627, 6, 157, 42, 159, 161, 66eltsms 21846 . . 3 (𝜑 → (𝑥 ∈ (𝐺 tsums 𝐹) ↔ (𝑥𝐵 ∧ ∀𝑣 ∈ (TopOpen‘𝐺)(𝑥𝑣 → ∃𝑦 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)∀𝑧 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin)(𝑦𝑧 → (𝐺 Σg (𝐹𝑧)) ∈ 𝑣)))))
163 eqid 2621 . . . 4 (𝒫 𝐴 ∩ Fin) = (𝒫 𝐴 ∩ Fin)
1647, 6, 163, 42, 159, 62, 68eltsms 21846 . . 3 (𝜑 → (𝑥 ∈ (𝐺 tsums 𝐻) ↔ (𝑥𝐵 ∧ ∀𝑢 ∈ (TopOpen‘𝐺)(𝑥𝑢 → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∀𝑏 ∈ (𝒫 𝐴 ∩ Fin)(𝑎𝑏 → (𝐺 Σg (𝐻𝑏)) ∈ 𝑢)))))
165156, 162, 1643imtr4d 283 . 2 (𝜑 → (𝑥 ∈ (𝐺 tsums 𝐹) → 𝑥 ∈ (𝐺 tsums 𝐻)))
166165ssrdv 3589 1 (𝜑 → (𝐺 tsums 𝐹) ⊆ (𝐺 tsums 𝐻))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036   = wceq 1480  wcel 1987  wral 2907  wrex 2908  Vcvv 3186  cin 3554  wss 3555  𝒫 cpw 4130  {csn 4148  cmpt 4673   × cxp 5072  dom cdm 5074  ran crn 5075  cres 5076  Rel wrel 5079  wf 5843  cfv 5847  (class class class)co 6604  𝑚 cmap 7802  Fincfn 7899  0cn0 11236  #chash 13057  Basecbs 15781  +gcplusg 15862  TopOpenctopn 16003  0gc0g 16021   Σg cgsu 16022  Mndcmnd 17215  -gcsg 17345  .gcmg 17461  CMndccmn 18114  TopOnctopon 20618  TopSpctps 20619  TopMndctmd 21784  TopGrpctgp 21785   tsums ctsu 21839
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902  ax-inf2 8482  ax-cnex 9936  ax-resscn 9937  ax-1cn 9938  ax-icn 9939  ax-addcl 9940  ax-addrcl 9941  ax-mulcl 9942  ax-mulrcl 9943  ax-mulcom 9944  ax-addass 9945  ax-mulass 9946  ax-distr 9947  ax-i2m1 9948  ax-1ne0 9949  ax-1rid 9950  ax-rnegex 9951  ax-rrecex 9952  ax-cnre 9953  ax-pre-lttri 9954  ax-pre-lttrn 9955  ax-pre-ltadd 9956  ax-pre-mulgt0 9957
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-int 4441  df-iun 4487  df-iin 4488  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-se 5034  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-isom 5856  df-riota 6565  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-of 6850  df-om 7013  df-1st 7113  df-2nd 7114  df-supp 7241  df-wrecs 7352  df-recs 7413  df-rdg 7451  df-1o 7505  df-2o 7506  df-oadd 7509  df-er 7687  df-map 7804  df-ixp 7853  df-en 7900  df-dom 7901  df-sdom 7902  df-fin 7903  df-fsupp 8220  df-fi 8261  df-oi 8359  df-card 8709  df-pnf 10020  df-mnf 10021  df-xr 10022  df-ltxr 10023  df-le 10024  df-sub 10212  df-neg 10213  df-nn 10965  df-2 11023  df-n0 11237  df-z 11322  df-uz 11632  df-fz 12269  df-fzo 12407  df-seq 12742  df-hash 13058  df-ndx 15784  df-slot 15785  df-base 15786  df-sets 15787  df-ress 15788  df-plusg 15875  df-rest 16004  df-0g 16023  df-gsum 16024  df-topgen 16025  df-pt 16026  df-mre 16167  df-mrc 16168  df-acs 16170  df-plusf 17162  df-mgm 17163  df-sgrp 17205  df-mnd 17216  df-mhm 17256  df-submnd 17257  df-grp 17346  df-minusg 17347  df-sbg 17348  df-mulg 17462  df-ghm 17579  df-cntz 17671  df-cmn 18116  df-abl 18117  df-fbas 19662  df-fg 19663  df-top 20621  df-bases 20622  df-topon 20623  df-topsp 20624  df-ntr 20734  df-nei 20812  df-cn 20941  df-cnp 20942  df-cmp 21100  df-tx 21275  df-xko 21276  df-hmeo 21468  df-fil 21560  df-fm 21652  df-flim 21653  df-flf 21654  df-tmd 21786  df-tgp 21787  df-tsms 21840
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator