Metamath Proof Explorer

Theorem tsmsxp

Description: Write a sum over a two-dimensional region as a double sum. This infinite group sum version of gsumxp is also known as Fubini's theorem. The converse is not necessarily true without additional assumptions. See tsmsxplem1 for the main proof; this part mostly sets up the local assumptions. (Contributed by Mario Carneiro, 21-Sep-2015)

Ref Expression
Hypotheses tsmsxp.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
tsmsxp.g ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
tsmsxp.2 ⊢ ( 𝜑 → 𝐺 ∈ TopGrp )
tsmsxp.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
tsmsxp.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑊 )
tsmsxp.f ⊢ ( 𝜑 → 𝐹 : ( 𝐴 × 𝐶 ) ⟶ 𝐵 )
tsmsxp.h ⊢ ( 𝜑 → 𝐻 : 𝐴 ⟶ 𝐵 )
tsmsxp.1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑗 ) ∈ ( 𝐺 tsums ( 𝑘 ∈ 𝐶 ↦ ( 𝑗 𝐹 𝑘 ) ) ) )
Assertion tsmsxp ( 𝜑 → ( 𝐺 tsums 𝐹 ) ⊆ ( 𝐺 tsums 𝐻 ) )

Proof

Step Hyp Ref Expression
1 tsmsxp.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 tsmsxp.g ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
3 tsmsxp.2 ⊢ ( 𝜑 → 𝐺 ∈ TopGrp )
4 tsmsxp.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
5 tsmsxp.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑊 )
6 tsmsxp.f ⊢ ( 𝜑 → 𝐹 : ( 𝐴 × 𝐶 ) ⟶ 𝐵 )
7 tsmsxp.h ⊢ ( 𝜑 → 𝐻 : 𝐴 ⟶ 𝐵 )
8 tsmsxp.1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑗 ) ∈ ( 𝐺 tsums ( 𝑘 ∈ 𝐶 ↦ ( 𝑗 𝐹 𝑘 ) ) ) )
9 tgptmd ⊢ ( 𝐺 ∈ TopGrp → 𝐺 ∈ TopMnd )
10 3 9 syl ⊢ ( 𝜑 → 𝐺 ∈ TopMnd )
11 10 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) → 𝐺 ∈ TopMnd )
12 simp2 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) → 𝑢 ∈ ( TopOpen ‘ 𝐺 ) )
13 eqid ⊢ ( TopOpen ‘ 𝐺 ) = ( TopOpen ‘ 𝐺 )
14 13 1 tmdtopon ⊢ ( 𝐺 ∈ TopMnd → ( TopOpen ‘ 𝐺 ) ∈ ( TopOn ‘ 𝐵 ) )
15 11 14 syl ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) → ( TopOpen ‘ 𝐺 ) ∈ ( TopOn ‘ 𝐵 ) )
16 toponss ⊢ ( ( ( TopOpen ‘ 𝐺 ) ∈ ( TopOn ‘ 𝐵 ) ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ) → 𝑢 ⊆ 𝐵 )
17 15 12 16 syl2anc ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) → 𝑢 ⊆ 𝐵 )
18 simp3 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) → 𝑥 ∈ 𝑢 )
19 17 18 sseldd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) → 𝑥 ∈ 𝐵 )
20 tmdmnd ⊢ ( 𝐺 ∈ TopMnd → 𝐺 ∈ Mnd )
21 11 20 syl ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) → 𝐺 ∈ Mnd )
22 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
23 1 22 mndidcl ⊢ ( 𝐺 ∈ Mnd → ( 0g ‘ 𝐺 ) ∈ 𝐵 )
24 21 23 syl ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) → ( 0g ‘ 𝐺 ) ∈ 𝐵 )
25 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
26 1 25 22 mndrid ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ( +g ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) = 𝑥 )
27 21 19 26 syl2anc ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) → ( 𝑥 ( +g ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) = 𝑥 )
28 27 18 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) → ( 𝑥 ( +g ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) ∈ 𝑢 )
29 1 13 25 tmdcn2 ⊢ ( ( ( 𝐺 ∈ TopMnd ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ ( 0g ‘ 𝐺 ) ∈ 𝐵 ∧ ( 𝑥 ( +g ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) ∈ 𝑢 ) ) → ∃ 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∃ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) )
30 11 12 19 24 28 29 syl23anc ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) → ∃ 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∃ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) )
31 r19.29 ⊢ ( ( ∀ 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ( 𝑥 ∈ 𝑣 → ∃ 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ∃ 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∃ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) → ∃ 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ( ( 𝑥 ∈ 𝑣 → ∃ 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ∃ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) )
32 simp31 ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) → 𝑥 ∈ 𝑣 )
33 elfpw ⊢ ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ↔ ( 𝑦 ⊆ ( 𝐴 × 𝐶 ) ∧ 𝑦 ∈ Fin ) )
34 33 simplbi ⊢ ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) → 𝑦 ⊆ ( 𝐴 × 𝐶 ) )
35 34 ad2antrl ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ) → 𝑦 ⊆ ( 𝐴 × 𝐶 ) )
36 dmss ⊢ ( 𝑦 ⊆ ( 𝐴 × 𝐶 ) → dom 𝑦 ⊆ dom ( 𝐴 × 𝐶 ) )
37 35 36 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ) → dom 𝑦 ⊆ dom ( 𝐴 × 𝐶 ) )
38 dmxpss ⊢ dom ( 𝐴 × 𝐶 ) ⊆ 𝐴
39 37 38 sstrdi ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ) → dom 𝑦 ⊆ 𝐴 )
40 elinel2 ⊢ ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) → 𝑦 ∈ Fin )
41 40 ad2antrl ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ) → 𝑦 ∈ Fin )
42 dmfi ⊢ ( 𝑦 ∈ Fin → dom 𝑦 ∈ Fin )
43 41 42 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ) → dom 𝑦 ∈ Fin )
44 elfpw ⊢ ( dom 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↔ ( dom 𝑦 ⊆ 𝐴 ∧ dom 𝑦 ∈ Fin ) )
45 39 43 44 sylanbrc ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ) → dom 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) )
46 eqid ⊢ ( .g ‘ 𝐺 ) = ( .g ‘ 𝐺 )
47 simpl11 ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ) → 𝜑 )
48 47 2 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ) → 𝐺 ∈ CMnd )
49 47 10 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ) → 𝐺 ∈ TopMnd )
50 simprrl ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ) → 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) )
51 50 elin2d ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ) → 𝑏 ∈ Fin )
52 simpl2r ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ) → 𝑡 ∈ ( TopOpen ‘ 𝐺 ) )
53 49 20 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ) → 𝐺 ∈ Mnd )
54 53 23 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ) → ( 0g ‘ 𝐺 ) ∈ 𝐵 )
55 hashcl ⊢ ( 𝑏 ∈ Fin → ( ♯ ‘ 𝑏 ) ∈ ℕ0 )
56 51 55 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ) → ( ♯ ‘ 𝑏 ) ∈ ℕ0 )
57 1 46 22 mulgnn0z ⊢ ( ( 𝐺 ∈ Mnd ∧ ( ♯ ‘ 𝑏 ) ∈ ℕ0 ) → ( ( ♯ ‘ 𝑏 ) ( .g ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) = ( 0g ‘ 𝐺 ) )
58 53 56 57 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ) → ( ( ♯ ‘ 𝑏 ) ( .g ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) = ( 0g ‘ 𝐺 ) )
59 simpl32 ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ) → ( 0g ‘ 𝐺 ) ∈ 𝑡 )
60 58 59 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ) → ( ( ♯ ‘ 𝑏 ) ( .g ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) ∈ 𝑡 )
61 13 1 46 48 49 51 52 54 60 tmdgsum2 ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ) → ∃ 𝑠 ∈ ( TopOpen ‘ 𝐺 ) ( ( 0g ‘ 𝐺 ) ∈ 𝑠 ∧ ∀ 𝑔 ∈ ( 𝑠 ↑m 𝑏 ) ( 𝐺 Σg 𝑔 ) ∈ 𝑡 ) )
62 simp111 ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ∧ ( 𝑠 ∈ ( TopOpen ‘ 𝐺 ) ∧ ( ( 0g ‘ 𝐺 ) ∈ 𝑠 ∧ ∀ 𝑔 ∈ ( 𝑠 ↑m 𝑏 ) ( 𝐺 Σg 𝑔 ) ∈ 𝑡 ) ) ) → 𝜑 )
63 62 2 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ∧ ( 𝑠 ∈ ( TopOpen ‘ 𝐺 ) ∧ ( ( 0g ‘ 𝐺 ) ∈ 𝑠 ∧ ∀ 𝑔 ∈ ( 𝑠 ↑m 𝑏 ) ( 𝐺 Σg 𝑔 ) ∈ 𝑡 ) ) ) → 𝐺 ∈ CMnd )
64 62 3 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ∧ ( 𝑠 ∈ ( TopOpen ‘ 𝐺 ) ∧ ( ( 0g ‘ 𝐺 ) ∈ 𝑠 ∧ ∀ 𝑔 ∈ ( 𝑠 ↑m 𝑏 ) ( 𝐺 Σg 𝑔 ) ∈ 𝑡 ) ) ) → 𝐺 ∈ TopGrp )
65 62 4 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ∧ ( 𝑠 ∈ ( TopOpen ‘ 𝐺 ) ∧ ( ( 0g ‘ 𝐺 ) ∈ 𝑠 ∧ ∀ 𝑔 ∈ ( 𝑠 ↑m 𝑏 ) ( 𝐺 Σg 𝑔 ) ∈ 𝑡 ) ) ) → 𝐴 ∈ 𝑉 )
66 62 5 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ∧ ( 𝑠 ∈ ( TopOpen ‘ 𝐺 ) ∧ ( ( 0g ‘ 𝐺 ) ∈ 𝑠 ∧ ∀ 𝑔 ∈ ( 𝑠 ↑m 𝑏 ) ( 𝐺 Σg 𝑔 ) ∈ 𝑡 ) ) ) → 𝐶 ∈ 𝑊 )
67 62 6 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ∧ ( 𝑠 ∈ ( TopOpen ‘ 𝐺 ) ∧ ( ( 0g ‘ 𝐺 ) ∈ 𝑠 ∧ ∀ 𝑔 ∈ ( 𝑠 ↑m 𝑏 ) ( 𝐺 Σg 𝑔 ) ∈ 𝑡 ) ) ) → 𝐹 : ( 𝐴 × 𝐶 ) ⟶ 𝐵 )
68 62 7 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ∧ ( 𝑠 ∈ ( TopOpen ‘ 𝐺 ) ∧ ( ( 0g ‘ 𝐺 ) ∈ 𝑠 ∧ ∀ 𝑔 ∈ ( 𝑠 ↑m 𝑏 ) ( 𝐺 Σg 𝑔 ) ∈ 𝑡 ) ) ) → 𝐻 : 𝐴 ⟶ 𝐵 )
69 62 8 sylan ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ∧ ( 𝑠 ∈ ( TopOpen ‘ 𝐺 ) ∧ ( ( 0g ‘ 𝐺 ) ∈ 𝑠 ∧ ∀ 𝑔 ∈ ( 𝑠 ↑m 𝑏 ) ( 𝐺 Σg 𝑔 ) ∈ 𝑡 ) ) ) ∧ 𝑗 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑗 ) ∈ ( 𝐺 tsums ( 𝑘 ∈ 𝐶 ↦ ( 𝑗 𝐹 𝑘 ) ) ) )
70 eqid ⊢ ( -g ‘ 𝐺 ) = ( -g ‘ 𝐺 )
71 simp3l ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ∧ ( 𝑠 ∈ ( TopOpen ‘ 𝐺 ) ∧ ( ( 0g ‘ 𝐺 ) ∈ 𝑠 ∧ ∀ 𝑔 ∈ ( 𝑠 ↑m 𝑏 ) ( 𝐺 Σg 𝑔 ) ∈ 𝑡 ) ) ) → 𝑠 ∈ ( TopOpen ‘ 𝐺 ) )
72 simp3rl ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ∧ ( 𝑠 ∈ ( TopOpen ‘ 𝐺 ) ∧ ( ( 0g ‘ 𝐺 ) ∈ 𝑠 ∧ ∀ 𝑔 ∈ ( 𝑠 ↑m 𝑏 ) ( 𝐺 Σg 𝑔 ) ∈ 𝑡 ) ) ) → ( 0g ‘ 𝐺 ) ∈ 𝑠 )
73 simp2rl ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ∧ ( 𝑠 ∈ ( TopOpen ‘ 𝐺 ) ∧ ( ( 0g ‘ 𝐺 ) ∈ 𝑠 ∧ ∀ 𝑔 ∈ ( 𝑠 ↑m 𝑏 ) ( 𝐺 Σg 𝑔 ) ∈ 𝑡 ) ) ) → 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) )
74 simp2rr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ∧ ( 𝑠 ∈ ( TopOpen ‘ 𝐺 ) ∧ ( ( 0g ‘ 𝐺 ) ∈ 𝑠 ∧ ∀ 𝑔 ∈ ( 𝑠 ↑m 𝑏 ) ( 𝐺 Σg 𝑔 ) ∈ 𝑡 ) ) ) → dom 𝑦 ⊆ 𝑏 )
75 simp2ll ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ∧ ( 𝑠 ∈ ( TopOpen ‘ 𝐺 ) ∧ ( ( 0g ‘ 𝐺 ) ∈ 𝑠 ∧ ∀ 𝑔 ∈ ( 𝑠 ↑m 𝑏 ) ( 𝐺 Σg 𝑔 ) ∈ 𝑡 ) ) ) → 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) )
76 1 63 64 65 66 67 68 69 13 22 25 70 71 72 73 74 75 tsmsxplem1 ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ∧ ( 𝑠 ∈ ( TopOpen ‘ 𝐺 ) ∧ ( ( 0g ‘ 𝐺 ) ∈ 𝑠 ∧ ∀ 𝑔 ∈ ( 𝑠 ↑m 𝑏 ) ( 𝐺 Σg 𝑔 ) ∈ 𝑡 ) ) ) → ∃ 𝑛 ∈ ( 𝒫 𝐶 ∩ Fin ) ( ran 𝑦 ⊆ 𝑛 ∧ ∀ 𝑥 ∈ 𝑏 ( ( 𝐻 ‘ 𝑥 ) ( -g ‘ 𝐺 ) ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × 𝑛 ) ) ) ) ∈ 𝑠 ) )
77 48 3adant3 ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ∧ ( ( 𝑠 ∈ ( TopOpen ‘ 𝐺 ) ∧ ( ( 0g ‘ 𝐺 ) ∈ 𝑠 ∧ ∀ 𝑔 ∈ ( 𝑠 ↑m 𝑏 ) ( 𝐺 Σg 𝑔 ) ∈ 𝑡 ) ) ∧ ( 𝑛 ∈ ( 𝒫 𝐶 ∩ Fin ) ∧ ( ran 𝑦 ⊆ 𝑛 ∧ ∀ 𝑥 ∈ 𝑏 ( ( 𝐻 ‘ 𝑥 ) ( -g ‘ 𝐺 ) ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × 𝑛 ) ) ) ) ∈ 𝑠 ) ) ) ) → 𝐺 ∈ CMnd )
78 64 3adant3r ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ∧ ( ( 𝑠 ∈ ( TopOpen ‘ 𝐺 ) ∧ ( ( 0g ‘ 𝐺 ) ∈ 𝑠 ∧ ∀ 𝑔 ∈ ( 𝑠 ↑m 𝑏 ) ( 𝐺 Σg 𝑔 ) ∈ 𝑡 ) ) ∧ ( 𝑛 ∈ ( 𝒫 𝐶 ∩ Fin ) ∧ ( ran 𝑦 ⊆ 𝑛 ∧ ∀ 𝑥 ∈ 𝑏 ( ( 𝐻 ‘ 𝑥 ) ( -g ‘ 𝐺 ) ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × 𝑛 ) ) ) ) ∈ 𝑠 ) ) ) ) → 𝐺 ∈ TopGrp )
79 65 3adant3r ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ∧ ( ( 𝑠 ∈ ( TopOpen ‘ 𝐺 ) ∧ ( ( 0g ‘ 𝐺 ) ∈ 𝑠 ∧ ∀ 𝑔 ∈ ( 𝑠 ↑m 𝑏 ) ( 𝐺 Σg 𝑔 ) ∈ 𝑡 ) ) ∧ ( 𝑛 ∈ ( 𝒫 𝐶 ∩ Fin ) ∧ ( ran 𝑦 ⊆ 𝑛 ∧ ∀ 𝑥 ∈ 𝑏 ( ( 𝐻 ‘ 𝑥 ) ( -g ‘ 𝐺 ) ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × 𝑛 ) ) ) ) ∈ 𝑠 ) ) ) ) → 𝐴 ∈ 𝑉 )
80 66 3adant3r ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ∧ ( ( 𝑠 ∈ ( TopOpen ‘ 𝐺 ) ∧ ( ( 0g ‘ 𝐺 ) ∈ 𝑠 ∧ ∀ 𝑔 ∈ ( 𝑠 ↑m 𝑏 ) ( 𝐺 Σg 𝑔 ) ∈ 𝑡 ) ) ∧ ( 𝑛 ∈ ( 𝒫 𝐶 ∩ Fin ) ∧ ( ran 𝑦 ⊆ 𝑛 ∧ ∀ 𝑥 ∈ 𝑏 ( ( 𝐻 ‘ 𝑥 ) ( -g ‘ 𝐺 ) ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × 𝑛 ) ) ) ) ∈ 𝑠 ) ) ) ) → 𝐶 ∈ 𝑊 )
81 67 3adant3r ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ∧ ( ( 𝑠 ∈ ( TopOpen ‘ 𝐺 ) ∧ ( ( 0g ‘ 𝐺 ) ∈ 𝑠 ∧ ∀ 𝑔 ∈ ( 𝑠 ↑m 𝑏 ) ( 𝐺 Σg 𝑔 ) ∈ 𝑡 ) ) ∧ ( 𝑛 ∈ ( 𝒫 𝐶 ∩ Fin ) ∧ ( ran 𝑦 ⊆ 𝑛 ∧ ∀ 𝑥 ∈ 𝑏 ( ( 𝐻 ‘ 𝑥 ) ( -g ‘ 𝐺 ) ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × 𝑛 ) ) ) ) ∈ 𝑠 ) ) ) ) → 𝐹 : ( 𝐴 × 𝐶 ) ⟶ 𝐵 )
82 68 3adant3r ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ∧ ( ( 𝑠 ∈ ( TopOpen ‘ 𝐺 ) ∧ ( ( 0g ‘ 𝐺 ) ∈ 𝑠 ∧ ∀ 𝑔 ∈ ( 𝑠 ↑m 𝑏 ) ( 𝐺 Σg 𝑔 ) ∈ 𝑡 ) ) ∧ ( 𝑛 ∈ ( 𝒫 𝐶 ∩ Fin ) ∧ ( ran 𝑦 ⊆ 𝑛 ∧ ∀ 𝑥 ∈ 𝑏 ( ( 𝐻 ‘ 𝑥 ) ( -g ‘ 𝐺 ) ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × 𝑛 ) ) ) ) ∈ 𝑠 ) ) ) ) → 𝐻 : 𝐴 ⟶ 𝐵 )
83 47 3adant3 ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ∧ ( ( 𝑠 ∈ ( TopOpen ‘ 𝐺 ) ∧ ( ( 0g ‘ 𝐺 ) ∈ 𝑠 ∧ ∀ 𝑔 ∈ ( 𝑠 ↑m 𝑏 ) ( 𝐺 Σg 𝑔 ) ∈ 𝑡 ) ) ∧ ( 𝑛 ∈ ( 𝒫 𝐶 ∩ Fin ) ∧ ( ran 𝑦 ⊆ 𝑛 ∧ ∀ 𝑥 ∈ 𝑏 ( ( 𝐻 ‘ 𝑥 ) ( -g ‘ 𝐺 ) ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × 𝑛 ) ) ) ) ∈ 𝑠 ) ) ) ) → 𝜑 )
84 83 8 sylan ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ∧ ( ( 𝑠 ∈ ( TopOpen ‘ 𝐺 ) ∧ ( ( 0g ‘ 𝐺 ) ∈ 𝑠 ∧ ∀ 𝑔 ∈ ( 𝑠 ↑m 𝑏 ) ( 𝐺 Σg 𝑔 ) ∈ 𝑡 ) ) ∧ ( 𝑛 ∈ ( 𝒫 𝐶 ∩ Fin ) ∧ ( ran 𝑦 ⊆ 𝑛 ∧ ∀ 𝑥 ∈ 𝑏 ( ( 𝐻 ‘ 𝑥 ) ( -g ‘ 𝐺 ) ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × 𝑛 ) ) ) ) ∈ 𝑠 ) ) ) ) ∧ 𝑗 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑗 ) ∈ ( 𝐺 tsums ( 𝑘 ∈ 𝐶 ↦ ( 𝑗 𝐹 𝑘 ) ) ) )
85 simp3ll ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ∧ ( ( 𝑠 ∈ ( TopOpen ‘ 𝐺 ) ∧ ( ( 0g ‘ 𝐺 ) ∈ 𝑠 ∧ ∀ 𝑔 ∈ ( 𝑠 ↑m 𝑏 ) ( 𝐺 Σg 𝑔 ) ∈ 𝑡 ) ) ∧ ( 𝑛 ∈ ( 𝒫 𝐶 ∩ Fin ) ∧ ( ran 𝑦 ⊆ 𝑛 ∧ ∀ 𝑥 ∈ 𝑏 ( ( 𝐻 ‘ 𝑥 ) ( -g ‘ 𝐺 ) ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × 𝑛 ) ) ) ) ∈ 𝑠 ) ) ) ) → 𝑠 ∈ ( TopOpen ‘ 𝐺 ) )
86 72 3adant3r ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ∧ ( ( 𝑠 ∈ ( TopOpen ‘ 𝐺 ) ∧ ( ( 0g ‘ 𝐺 ) ∈ 𝑠 ∧ ∀ 𝑔 ∈ ( 𝑠 ↑m 𝑏 ) ( 𝐺 Σg 𝑔 ) ∈ 𝑡 ) ) ∧ ( 𝑛 ∈ ( 𝒫 𝐶 ∩ Fin ) ∧ ( ran 𝑦 ⊆ 𝑛 ∧ ∀ 𝑥 ∈ 𝑏 ( ( 𝐻 ‘ 𝑥 ) ( -g ‘ 𝐺 ) ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × 𝑛 ) ) ) ) ∈ 𝑠 ) ) ) ) → ( 0g ‘ 𝐺 ) ∈ 𝑠 )
87 simp2rl ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ∧ ( ( 𝑠 ∈ ( TopOpen ‘ 𝐺 ) ∧ ( ( 0g ‘ 𝐺 ) ∈ 𝑠 ∧ ∀ 𝑔 ∈ ( 𝑠 ↑m 𝑏 ) ( 𝐺 Σg 𝑔 ) ∈ 𝑡 ) ) ∧ ( 𝑛 ∈ ( 𝒫 𝐶 ∩ Fin ) ∧ ( ran 𝑦 ⊆ 𝑛 ∧ ∀ 𝑥 ∈ 𝑏 ( ( 𝐻 ‘ 𝑥 ) ( -g ‘ 𝐺 ) ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × 𝑛 ) ) ) ) ∈ 𝑠 ) ) ) ) → 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) )
88 simp133 ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ∧ ( ( 𝑠 ∈ ( TopOpen ‘ 𝐺 ) ∧ ( ( 0g ‘ 𝐺 ) ∈ 𝑠 ∧ ∀ 𝑔 ∈ ( 𝑠 ↑m 𝑏 ) ( 𝐺 Σg 𝑔 ) ∈ 𝑡 ) ) ∧ ( 𝑛 ∈ ( 𝒫 𝐶 ∩ Fin ) ∧ ( ran 𝑦 ⊆ 𝑛 ∧ ∀ 𝑥 ∈ 𝑏 ( ( 𝐻 ‘ 𝑥 ) ( -g ‘ 𝐺 ) ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × 𝑛 ) ) ) ) ∈ 𝑠 ) ) ) ) → ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 )
89 simp3rl ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ∧ ( ( 𝑠 ∈ ( TopOpen ‘ 𝐺 ) ∧ ( ( 0g ‘ 𝐺 ) ∈ 𝑠 ∧ ∀ 𝑔 ∈ ( 𝑠 ↑m 𝑏 ) ( 𝐺 Σg 𝑔 ) ∈ 𝑡 ) ) ∧ ( 𝑛 ∈ ( 𝒫 𝐶 ∩ Fin ) ∧ ( ran 𝑦 ⊆ 𝑛 ∧ ∀ 𝑥 ∈ 𝑏 ( ( 𝐻 ‘ 𝑥 ) ( -g ‘ 𝐺 ) ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × 𝑛 ) ) ) ) ∈ 𝑠 ) ) ) ) → 𝑛 ∈ ( 𝒫 𝐶 ∩ Fin ) )
90 simp2ll ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ∧ ( ( 𝑠 ∈ ( TopOpen ‘ 𝐺 ) ∧ ( ( 0g ‘ 𝐺 ) ∈ 𝑠 ∧ ∀ 𝑔 ∈ ( 𝑠 ↑m 𝑏 ) ( 𝐺 Σg 𝑔 ) ∈ 𝑡 ) ) ∧ ( 𝑛 ∈ ( 𝒫 𝐶 ∩ Fin ) ∧ ( ran 𝑦 ⊆ 𝑛 ∧ ∀ 𝑥 ∈ 𝑏 ( ( 𝐻 ‘ 𝑥 ) ( -g ‘ 𝐺 ) ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × 𝑛 ) ) ) ) ∈ 𝑠 ) ) ) ) → 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) )
91 simp2rr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ∧ ( ( 𝑠 ∈ ( TopOpen ‘ 𝐺 ) ∧ ( ( 0g ‘ 𝐺 ) ∈ 𝑠 ∧ ∀ 𝑔 ∈ ( 𝑠 ↑m 𝑏 ) ( 𝐺 Σg 𝑔 ) ∈ 𝑡 ) ) ∧ ( 𝑛 ∈ ( 𝒫 𝐶 ∩ Fin ) ∧ ( ran 𝑦 ⊆ 𝑛 ∧ ∀ 𝑥 ∈ 𝑏 ( ( 𝐻 ‘ 𝑥 ) ( -g ‘ 𝐺 ) ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × 𝑛 ) ) ) ) ∈ 𝑠 ) ) ) ) → dom 𝑦 ⊆ 𝑏 )
92 simp3rr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ∧ ( ( 𝑠 ∈ ( TopOpen ‘ 𝐺 ) ∧ ( ( 0g ‘ 𝐺 ) ∈ 𝑠 ∧ ∀ 𝑔 ∈ ( 𝑠 ↑m 𝑏 ) ( 𝐺 Σg 𝑔 ) ∈ 𝑡 ) ) ∧ ( 𝑛 ∈ ( 𝒫 𝐶 ∩ Fin ) ∧ ( ran 𝑦 ⊆ 𝑛 ∧ ∀ 𝑥 ∈ 𝑏 ( ( 𝐻 ‘ 𝑥 ) ( -g ‘ 𝐺 ) ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × 𝑛 ) ) ) ) ∈ 𝑠 ) ) ) ) → ( ran 𝑦 ⊆ 𝑛 ∧ ∀ 𝑥 ∈ 𝑏 ( ( 𝐻 ‘ 𝑥 ) ( -g ‘ 𝐺 ) ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × 𝑛 ) ) ) ) ∈ 𝑠 ) )
93 92 simpld ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ∧ ( ( 𝑠 ∈ ( TopOpen ‘ 𝐺 ) ∧ ( ( 0g ‘ 𝐺 ) ∈ 𝑠 ∧ ∀ 𝑔 ∈ ( 𝑠 ↑m 𝑏 ) ( 𝐺 Σg 𝑔 ) ∈ 𝑡 ) ) ∧ ( 𝑛 ∈ ( 𝒫 𝐶 ∩ Fin ) ∧ ( ran 𝑦 ⊆ 𝑛 ∧ ∀ 𝑥 ∈ 𝑏 ( ( 𝐻 ‘ 𝑥 ) ( -g ‘ 𝐺 ) ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × 𝑛 ) ) ) ) ∈ 𝑠 ) ) ) ) → ran 𝑦 ⊆ 𝑛 )
94 relxp ⊢ Rel ( 𝐴 × 𝐶 )
95 relss ⊢ ( 𝑦 ⊆ ( 𝐴 × 𝐶 ) → ( Rel ( 𝐴 × 𝐶 ) → Rel 𝑦 ) )
96 34 94 95 mpisyl ⊢ ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) → Rel 𝑦 )
97 relssdmrn ⊢ ( Rel 𝑦 → 𝑦 ⊆ ( dom 𝑦 × ran 𝑦 ) )
98 96 97 syl ⊢ ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) → 𝑦 ⊆ ( dom 𝑦 × ran 𝑦 ) )
99 xpss12 ⊢ ( ( dom 𝑦 ⊆ 𝑏 ∧ ran 𝑦 ⊆ 𝑛 ) → ( dom 𝑦 × ran 𝑦 ) ⊆ ( 𝑏 × 𝑛 ) )
100 98 99 sylan9ss ⊢ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ( dom 𝑦 ⊆ 𝑏 ∧ ran 𝑦 ⊆ 𝑛 ) ) → 𝑦 ⊆ ( 𝑏 × 𝑛 ) )
101 90 91 93 100 syl12anc ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ∧ ( ( 𝑠 ∈ ( TopOpen ‘ 𝐺 ) ∧ ( ( 0g ‘ 𝐺 ) ∈ 𝑠 ∧ ∀ 𝑔 ∈ ( 𝑠 ↑m 𝑏 ) ( 𝐺 Σg 𝑔 ) ∈ 𝑡 ) ) ∧ ( 𝑛 ∈ ( 𝒫 𝐶 ∩ Fin ) ∧ ( ran 𝑦 ⊆ 𝑛 ∧ ∀ 𝑥 ∈ 𝑏 ( ( 𝐻 ‘ 𝑥 ) ( -g ‘ 𝐺 ) ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × 𝑛 ) ) ) ) ∈ 𝑠 ) ) ) ) → 𝑦 ⊆ ( 𝑏 × 𝑛 ) )
102 92 simprd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ∧ ( ( 𝑠 ∈ ( TopOpen ‘ 𝐺 ) ∧ ( ( 0g ‘ 𝐺 ) ∈ 𝑠 ∧ ∀ 𝑔 ∈ ( 𝑠 ↑m 𝑏 ) ( 𝐺 Σg 𝑔 ) ∈ 𝑡 ) ) ∧ ( 𝑛 ∈ ( 𝒫 𝐶 ∩ Fin ) ∧ ( ran 𝑦 ⊆ 𝑛 ∧ ∀ 𝑥 ∈ 𝑏 ( ( 𝐻 ‘ 𝑥 ) ( -g ‘ 𝐺 ) ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × 𝑛 ) ) ) ) ∈ 𝑠 ) ) ) ) → ∀ 𝑥 ∈ 𝑏 ( ( 𝐻 ‘ 𝑥 ) ( -g ‘ 𝐺 ) ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × 𝑛 ) ) ) ) ∈ 𝑠 )
103 sseq2 ⊢ ( 𝑧 = ( 𝑏 × 𝑛 ) → ( 𝑦 ⊆ 𝑧 ↔ 𝑦 ⊆ ( 𝑏 × 𝑛 ) ) )
104 reseq2 ⊢ ( 𝑧 = ( 𝑏 × 𝑛 ) → ( 𝐹 ↾ 𝑧 ) = ( 𝐹 ↾ ( 𝑏 × 𝑛 ) ) )
105 104 oveq2d ⊢ ( 𝑧 = ( 𝑏 × 𝑛 ) → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) = ( 𝐺 Σg ( 𝐹 ↾ ( 𝑏 × 𝑛 ) ) ) )
106 105 eleq1d ⊢ ( 𝑧 = ( 𝑏 × 𝑛 ) → ( ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ↔ ( 𝐺 Σg ( 𝐹 ↾ ( 𝑏 × 𝑛 ) ) ) ∈ 𝑣 ) )
107 103 106 imbi12d ⊢ ( 𝑧 = ( 𝑏 × 𝑛 ) → ( ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ↔ ( 𝑦 ⊆ ( 𝑏 × 𝑛 ) → ( 𝐺 Σg ( 𝐹 ↾ ( 𝑏 × 𝑛 ) ) ) ∈ 𝑣 ) ) )
108 simp2lr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ∧ ( ( 𝑠 ∈ ( TopOpen ‘ 𝐺 ) ∧ ( ( 0g ‘ 𝐺 ) ∈ 𝑠 ∧ ∀ 𝑔 ∈ ( 𝑠 ↑m 𝑏 ) ( 𝐺 Σg 𝑔 ) ∈ 𝑡 ) ) ∧ ( 𝑛 ∈ ( 𝒫 𝐶 ∩ Fin ) ∧ ( ran 𝑦 ⊆ 𝑛 ∧ ∀ 𝑥 ∈ 𝑏 ( ( 𝐻 ‘ 𝑥 ) ( -g ‘ 𝐺 ) ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × 𝑛 ) ) ) ) ∈ 𝑠 ) ) ) ) → ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) )
109 elfpw ⊢ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ↔ ( 𝑏 ⊆ 𝐴 ∧ 𝑏 ∈ Fin ) )
110 elfpw ⊢ ( 𝑛 ∈ ( 𝒫 𝐶 ∩ Fin ) ↔ ( 𝑛 ⊆ 𝐶 ∧ 𝑛 ∈ Fin ) )
111 xpss12 ⊢ ( ( 𝑏 ⊆ 𝐴 ∧ 𝑛 ⊆ 𝐶 ) → ( 𝑏 × 𝑛 ) ⊆ ( 𝐴 × 𝐶 ) )
112 xpfi ⊢ ( ( 𝑏 ∈ Fin ∧ 𝑛 ∈ Fin ) → ( 𝑏 × 𝑛 ) ∈ Fin )
113 111 112 anim12i ⊢ ( ( ( 𝑏 ⊆ 𝐴 ∧ 𝑛 ⊆ 𝐶 ) ∧ ( 𝑏 ∈ Fin ∧ 𝑛 ∈ Fin ) ) → ( ( 𝑏 × 𝑛 ) ⊆ ( 𝐴 × 𝐶 ) ∧ ( 𝑏 × 𝑛 ) ∈ Fin ) )
114 113 an4s ⊢ ( ( ( 𝑏 ⊆ 𝐴 ∧ 𝑏 ∈ Fin ) ∧ ( 𝑛 ⊆ 𝐶 ∧ 𝑛 ∈ Fin ) ) → ( ( 𝑏 × 𝑛 ) ⊆ ( 𝐴 × 𝐶 ) ∧ ( 𝑏 × 𝑛 ) ∈ Fin ) )
115 109 110 114 syl2anb ⊢ ( ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑛 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → ( ( 𝑏 × 𝑛 ) ⊆ ( 𝐴 × 𝐶 ) ∧ ( 𝑏 × 𝑛 ) ∈ Fin ) )
116 elfpw ⊢ ( ( 𝑏 × 𝑛 ) ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ↔ ( ( 𝑏 × 𝑛 ) ⊆ ( 𝐴 × 𝐶 ) ∧ ( 𝑏 × 𝑛 ) ∈ Fin ) )
117 115 116 sylibr ⊢ ( ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑛 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → ( 𝑏 × 𝑛 ) ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) )
118 87 89 117 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ∧ ( ( 𝑠 ∈ ( TopOpen ‘ 𝐺 ) ∧ ( ( 0g ‘ 𝐺 ) ∈ 𝑠 ∧ ∀ 𝑔 ∈ ( 𝑠 ↑m 𝑏 ) ( 𝐺 Σg 𝑔 ) ∈ 𝑡 ) ) ∧ ( 𝑛 ∈ ( 𝒫 𝐶 ∩ Fin ) ∧ ( ran 𝑦 ⊆ 𝑛 ∧ ∀ 𝑥 ∈ 𝑏 ( ( 𝐻 ‘ 𝑥 ) ( -g ‘ 𝐺 ) ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × 𝑛 ) ) ) ) ∈ 𝑠 ) ) ) ) → ( 𝑏 × 𝑛 ) ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) )
119 107 108 118 rspcdva ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ∧ ( ( 𝑠 ∈ ( TopOpen ‘ 𝐺 ) ∧ ( ( 0g ‘ 𝐺 ) ∈ 𝑠 ∧ ∀ 𝑔 ∈ ( 𝑠 ↑m 𝑏 ) ( 𝐺 Σg 𝑔 ) ∈ 𝑡 ) ) ∧ ( 𝑛 ∈ ( 𝒫 𝐶 ∩ Fin ) ∧ ( ran 𝑦 ⊆ 𝑛 ∧ ∀ 𝑥 ∈ 𝑏 ( ( 𝐻 ‘ 𝑥 ) ( -g ‘ 𝐺 ) ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × 𝑛 ) ) ) ) ∈ 𝑠 ) ) ) ) → ( 𝑦 ⊆ ( 𝑏 × 𝑛 ) → ( 𝐺 Σg ( 𝐹 ↾ ( 𝑏 × 𝑛 ) ) ) ∈ 𝑣 ) )
120 101 119 mpd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ∧ ( ( 𝑠 ∈ ( TopOpen ‘ 𝐺 ) ∧ ( ( 0g ‘ 𝐺 ) ∈ 𝑠 ∧ ∀ 𝑔 ∈ ( 𝑠 ↑m 𝑏 ) ( 𝐺 Σg 𝑔 ) ∈ 𝑡 ) ) ∧ ( 𝑛 ∈ ( 𝒫 𝐶 ∩ Fin ) ∧ ( ran 𝑦 ⊆ 𝑛 ∧ ∀ 𝑥 ∈ 𝑏 ( ( 𝐻 ‘ 𝑥 ) ( -g ‘ 𝐺 ) ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × 𝑛 ) ) ) ) ∈ 𝑠 ) ) ) ) → ( 𝐺 Σg ( 𝐹 ↾ ( 𝑏 × 𝑛 ) ) ) ∈ 𝑣 )
121 simp3lr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ∧ ( ( 𝑠 ∈ ( TopOpen ‘ 𝐺 ) ∧ ( ( 0g ‘ 𝐺 ) ∈ 𝑠 ∧ ∀ 𝑔 ∈ ( 𝑠 ↑m 𝑏 ) ( 𝐺 Σg 𝑔 ) ∈ 𝑡 ) ) ∧ ( 𝑛 ∈ ( 𝒫 𝐶 ∩ Fin ) ∧ ( ran 𝑦 ⊆ 𝑛 ∧ ∀ 𝑥 ∈ 𝑏 ( ( 𝐻 ‘ 𝑥 ) ( -g ‘ 𝐺 ) ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × 𝑛 ) ) ) ) ∈ 𝑠 ) ) ) ) → ( ( 0g ‘ 𝐺 ) ∈ 𝑠 ∧ ∀ 𝑔 ∈ ( 𝑠 ↑m 𝑏 ) ( 𝐺 Σg 𝑔 ) ∈ 𝑡 ) )
122 121 simprd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ∧ ( ( 𝑠 ∈ ( TopOpen ‘ 𝐺 ) ∧ ( ( 0g ‘ 𝐺 ) ∈ 𝑠 ∧ ∀ 𝑔 ∈ ( 𝑠 ↑m 𝑏 ) ( 𝐺 Σg 𝑔 ) ∈ 𝑡 ) ) ∧ ( 𝑛 ∈ ( 𝒫 𝐶 ∩ Fin ) ∧ ( ran 𝑦 ⊆ 𝑛 ∧ ∀ 𝑥 ∈ 𝑏 ( ( 𝐻 ‘ 𝑥 ) ( -g ‘ 𝐺 ) ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × 𝑛 ) ) ) ) ∈ 𝑠 ) ) ) ) → ∀ 𝑔 ∈ ( 𝑠 ↑m 𝑏 ) ( 𝐺 Σg 𝑔 ) ∈ 𝑡 )
123 oveq2 ⊢ ( 𝑔 = ℎ → ( 𝐺 Σg 𝑔 ) = ( 𝐺 Σg ℎ ) )
124 123 eleq1d ⊢ ( 𝑔 = ℎ → ( ( 𝐺 Σg 𝑔 ) ∈ 𝑡 ↔ ( 𝐺 Σg ℎ ) ∈ 𝑡 ) )
125 124 cbvralvw ⊢ ( ∀ 𝑔 ∈ ( 𝑠 ↑m 𝑏 ) ( 𝐺 Σg 𝑔 ) ∈ 𝑡 ↔ ∀ ℎ ∈ ( 𝑠 ↑m 𝑏 ) ( 𝐺 Σg ℎ ) ∈ 𝑡 )
126 122 125 sylib ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ∧ ( ( 𝑠 ∈ ( TopOpen ‘ 𝐺 ) ∧ ( ( 0g ‘ 𝐺 ) ∈ 𝑠 ∧ ∀ 𝑔 ∈ ( 𝑠 ↑m 𝑏 ) ( 𝐺 Σg 𝑔 ) ∈ 𝑡 ) ) ∧ ( 𝑛 ∈ ( 𝒫 𝐶 ∩ Fin ) ∧ ( ran 𝑦 ⊆ 𝑛 ∧ ∀ 𝑥 ∈ 𝑏 ( ( 𝐻 ‘ 𝑥 ) ( -g ‘ 𝐺 ) ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × 𝑛 ) ) ) ) ∈ 𝑠 ) ) ) ) → ∀ ℎ ∈ ( 𝑠 ↑m 𝑏 ) ( 𝐺 Σg ℎ ) ∈ 𝑡 )
127 1 77 78 79 80 81 82 84 13 22 25 70 85 86 87 88 89 101 102 120 126 tsmsxplem2 ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ∧ ( ( 𝑠 ∈ ( TopOpen ‘ 𝐺 ) ∧ ( ( 0g ‘ 𝐺 ) ∈ 𝑠 ∧ ∀ 𝑔 ∈ ( 𝑠 ↑m 𝑏 ) ( 𝐺 Σg 𝑔 ) ∈ 𝑡 ) ) ∧ ( 𝑛 ∈ ( 𝒫 𝐶 ∩ Fin ) ∧ ( ran 𝑦 ⊆ 𝑛 ∧ ∀ 𝑥 ∈ 𝑏 ( ( 𝐻 ‘ 𝑥 ) ( -g ‘ 𝐺 ) ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × 𝑛 ) ) ) ) ∈ 𝑠 ) ) ) ) → ( 𝐺 Σg ( 𝐻 ↾ 𝑏 ) ) ∈ 𝑢 )
128 127 3exp ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) → ( ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) → ( ( ( 𝑠 ∈ ( TopOpen ‘ 𝐺 ) ∧ ( ( 0g ‘ 𝐺 ) ∈ 𝑠 ∧ ∀ 𝑔 ∈ ( 𝑠 ↑m 𝑏 ) ( 𝐺 Σg 𝑔 ) ∈ 𝑡 ) ) ∧ ( 𝑛 ∈ ( 𝒫 𝐶 ∩ Fin ) ∧ ( ran 𝑦 ⊆ 𝑛 ∧ ∀ 𝑥 ∈ 𝑏 ( ( 𝐻 ‘ 𝑥 ) ( -g ‘ 𝐺 ) ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × 𝑛 ) ) ) ) ∈ 𝑠 ) ) ) → ( 𝐺 Σg ( 𝐻 ↾ 𝑏 ) ) ∈ 𝑢 ) ) )
129 128 exp4a ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) → ( ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) → ( ( 𝑠 ∈ ( TopOpen ‘ 𝐺 ) ∧ ( ( 0g ‘ 𝐺 ) ∈ 𝑠 ∧ ∀ 𝑔 ∈ ( 𝑠 ↑m 𝑏 ) ( 𝐺 Σg 𝑔 ) ∈ 𝑡 ) ) → ( ( 𝑛 ∈ ( 𝒫 𝐶 ∩ Fin ) ∧ ( ran 𝑦 ⊆ 𝑛 ∧ ∀ 𝑥 ∈ 𝑏 ( ( 𝐻 ‘ 𝑥 ) ( -g ‘ 𝐺 ) ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × 𝑛 ) ) ) ) ∈ 𝑠 ) ) → ( 𝐺 Σg ( 𝐻 ↾ 𝑏 ) ) ∈ 𝑢 ) ) ) )
130 129 3imp1 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ∧ ( 𝑠 ∈ ( TopOpen ‘ 𝐺 ) ∧ ( ( 0g ‘ 𝐺 ) ∈ 𝑠 ∧ ∀ 𝑔 ∈ ( 𝑠 ↑m 𝑏 ) ( 𝐺 Σg 𝑔 ) ∈ 𝑡 ) ) ) ∧ ( 𝑛 ∈ ( 𝒫 𝐶 ∩ Fin ) ∧ ( ran 𝑦 ⊆ 𝑛 ∧ ∀ 𝑥 ∈ 𝑏 ( ( 𝐻 ‘ 𝑥 ) ( -g ‘ 𝐺 ) ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × 𝑛 ) ) ) ) ∈ 𝑠 ) ) ) → ( 𝐺 Σg ( 𝐻 ↾ 𝑏 ) ) ∈ 𝑢 )
131 76 130 rexlimddv ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ∧ ( 𝑠 ∈ ( TopOpen ‘ 𝐺 ) ∧ ( ( 0g ‘ 𝐺 ) ∈ 𝑠 ∧ ∀ 𝑔 ∈ ( 𝑠 ↑m 𝑏 ) ( 𝐺 Σg 𝑔 ) ∈ 𝑡 ) ) ) → ( 𝐺 Σg ( 𝐻 ↾ 𝑏 ) ) ∈ 𝑢 )
132 131 3expa ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ) ∧ ( 𝑠 ∈ ( TopOpen ‘ 𝐺 ) ∧ ( ( 0g ‘ 𝐺 ) ∈ 𝑠 ∧ ∀ 𝑔 ∈ ( 𝑠 ↑m 𝑏 ) ( 𝐺 Σg 𝑔 ) ∈ 𝑡 ) ) ) → ( 𝐺 Σg ( 𝐻 ↾ 𝑏 ) ) ∈ 𝑢 )
133 61 132 rexlimddv ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) ) → ( 𝐺 Σg ( 𝐻 ↾ 𝑏 ) ) ∈ 𝑢 )
134 133 anassrs ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ) ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ dom 𝑦 ⊆ 𝑏 ) ) → ( 𝐺 Σg ( 𝐻 ↾ 𝑏 ) ) ∈ 𝑢 )
135 134 expr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ) ∧ 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( dom 𝑦 ⊆ 𝑏 → ( 𝐺 Σg ( 𝐻 ↾ 𝑏 ) ) ∈ 𝑢 ) )
136 135 ralrimiva ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ) → ∀ 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ( dom 𝑦 ⊆ 𝑏 → ( 𝐺 Σg ( 𝐻 ↾ 𝑏 ) ) ∈ 𝑢 ) )
137 sseq1 ⊢ ( 𝑎 = dom 𝑦 → ( 𝑎 ⊆ 𝑏 ↔ dom 𝑦 ⊆ 𝑏 ) )
138 137 rspceaimv ⊢ ( ( dom 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ( dom 𝑦 ⊆ 𝑏 → ( 𝐺 Σg ( 𝐻 ↾ 𝑏 ) ) ∈ 𝑢 ) ) → ∃ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( 𝐻 ↾ 𝑏 ) ) ∈ 𝑢 ) )
139 45 136 138 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) ∧ ( 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ) → ∃ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( 𝐻 ↾ 𝑏 ) ) ∈ 𝑢 ) )
140 139 rexlimdvaa ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) → ( ∃ 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) → ∃ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( 𝐻 ↾ 𝑏 ) ) ∈ 𝑢 ) ) )
141 32 140 embantd ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) → ( ( 𝑥 ∈ 𝑣 → ∃ 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) → ∃ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( 𝐻 ↾ 𝑏 ) ) ∈ 𝑢 ) ) )
142 141 3expia ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ ( 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) ) → ( ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) → ( ( 𝑥 ∈ 𝑣 → ∃ 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) → ∃ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( 𝐻 ↾ 𝑏 ) ) ∈ 𝑢 ) ) ) )
143 142 anassrs ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ) ∧ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ) → ( ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) → ( ( 𝑥 ∈ 𝑣 → ∃ 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) → ∃ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( 𝐻 ↾ 𝑏 ) ) ∈ 𝑢 ) ) ) )
144 143 rexlimdva ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ) → ( ∃ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) → ( ( 𝑥 ∈ 𝑣 → ∃ 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) → ∃ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( 𝐻 ↾ 𝑏 ) ) ∈ 𝑢 ) ) ) )
145 144 impcomd ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) ∧ 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ) → ( ( ( 𝑥 ∈ 𝑣 → ∃ 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ∃ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) → ∃ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( 𝐻 ↾ 𝑏 ) ) ∈ 𝑢 ) ) )
146 145 rexlimdva ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) → ( ∃ 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ( ( 𝑥 ∈ 𝑣 → ∃ 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ∃ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) → ∃ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( 𝐻 ↾ 𝑏 ) ) ∈ 𝑢 ) ) )
147 31 146 syl5 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) → ( ( ∀ 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ( 𝑥 ∈ 𝑣 → ∃ 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ∧ ∃ 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ∃ 𝑡 ∈ ( TopOpen ‘ 𝐺 ) ( 𝑥 ∈ 𝑣 ∧ ( 0g ‘ 𝐺 ) ∈ 𝑡 ∧ ∀ 𝑐 ∈ 𝑣 ∀ 𝑑 ∈ 𝑡 ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑢 ) ) → ∃ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( 𝐻 ↾ 𝑏 ) ) ∈ 𝑢 ) ) )
148 30 147 mpan2d ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑢 ) → ( ∀ 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ( 𝑥 ∈ 𝑣 → ∃ 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) → ∃ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( 𝐻 ↾ 𝑏 ) ) ∈ 𝑢 ) ) )
149 148 3expia ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ) → ( 𝑥 ∈ 𝑢 → ( ∀ 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ( 𝑥 ∈ 𝑣 → ∃ 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) → ∃ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( 𝐻 ↾ 𝑏 ) ) ∈ 𝑢 ) ) ) )
150 149 com23 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ) → ( ∀ 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ( 𝑥 ∈ 𝑣 → ∃ 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) → ( 𝑥 ∈ 𝑢 → ∃ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( 𝐻 ↾ 𝑏 ) ) ∈ 𝑢 ) ) ) )
151 150 ralrimdva ⊢ ( 𝜑 → ( ∀ 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ( 𝑥 ∈ 𝑣 → ∃ 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) → ∀ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ( 𝑥 ∈ 𝑢 → ∃ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( 𝐻 ↾ 𝑏 ) ) ∈ 𝑢 ) ) ) )
152 151 anim2d ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ( 𝑥 ∈ 𝑣 → ∃ 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ) → ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ( 𝑥 ∈ 𝑢 → ∃ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( 𝐻 ↾ 𝑏 ) ) ∈ 𝑢 ) ) ) ) )
153 eqid ⊢ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) = ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin )
154 tgptps ⊢ ( 𝐺 ∈ TopGrp → 𝐺 ∈ TopSp )
155 3 154 syl ⊢ ( 𝜑 → 𝐺 ∈ TopSp )
156 4 5 xpexd ⊢ ( 𝜑 → ( 𝐴 × 𝐶 ) ∈ V )
157 1 13 153 2 155 156 6 eltsms ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐺 tsums 𝐹 ) ↔ ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑣 ∈ ( TopOpen ‘ 𝐺 ) ( 𝑥 ∈ 𝑣 → ∃ 𝑦 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑣 ) ) ) ) )
158 eqid ⊢ ( 𝒫 𝐴 ∩ Fin ) = ( 𝒫 𝐴 ∩ Fin )
159 1 13 158 2 155 4 7 eltsms ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐺 tsums 𝐻 ) ↔ ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ( 𝑥 ∈ 𝑢 → ∃ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( 𝐻 ↾ 𝑏 ) ) ∈ 𝑢 ) ) ) ) )
160 152 157 159 3imtr4d ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐺 tsums 𝐹 ) → 𝑥 ∈ ( 𝐺 tsums 𝐻 ) ) )
161 160 ssrdv ⊢ ( 𝜑 → ( 𝐺 tsums 𝐹 ) ⊆ ( 𝐺 tsums 𝐻 ) )