This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem tsmssubm

Description: Evaluate an infinite group sum in a submonoid. (Contributed by Mario Carneiro, 18-Sep-2015)

Ref Expression
Hypotheses tsmssubm.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
tsmssubm.1 ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
tsmssubm.2 ⊢ ( 𝜑 → 𝐺 ∈ TopSp )
tsmssubm.s ⊢ ( 𝜑 → 𝑆 ∈ ( SubMnd ‘ 𝐺 ) )
tsmssubm.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝑆 )
tsmssubm.h ⊢ 𝐻 = ( 𝐺 ↾s 𝑆 )
Assertion tsmssubm ( 𝜑 → ( 𝐻 tsums 𝐹 ) = ( ( 𝐺 tsums 𝐹 ) ∩ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 tsmssubm.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 tsmssubm.1 ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
3 tsmssubm.2 ⊢ ( 𝜑 → 𝐺 ∈ TopSp )
4 tsmssubm.s ⊢ ( 𝜑 → 𝑆 ∈ ( SubMnd ‘ 𝐺 ) )
5 tsmssubm.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝑆 )
6 tsmssubm.h ⊢ 𝐻 = ( 𝐺 ↾s 𝑆 )
7 6 submbas ⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) → 𝑆 = ( Base ‘ 𝐻 ) )
8 4 7 syl ⊢ ( 𝜑 → 𝑆 = ( Base ‘ 𝐻 ) )
9 8 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑆 ↔ 𝑥 ∈ ( Base ‘ 𝐻 ) ) )
10 9 anbi1d ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑆 ∧ ∀ 𝑣 ∈ ( TopOpen ‘ 𝐻 ) ( 𝑥 ∈ 𝑣 → ∃ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑧 ⊆ 𝑦 → ( 𝐻 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑣 ) ) ) ↔ ( 𝑥 ∈ ( Base ‘ 𝐻 ) ∧ ∀ 𝑣 ∈ ( TopOpen ‘ 𝐻 ) ( 𝑥 ∈ 𝑣 → ∃ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑧 ⊆ 𝑦 → ( 𝐻 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑣 ) ) ) ) )
11 elin ⊢ ( 𝑥 ∈ ( ( 𝐺 tsums 𝐹 ) ∩ 𝑆 ) ↔ ( 𝑥 ∈ ( 𝐺 tsums 𝐹 ) ∧ 𝑥 ∈ 𝑆 ) )
12 11 biancomi ⊢ ( 𝑥 ∈ ( ( 𝐺 tsums 𝐹 ) ∩ 𝑆 ) ↔ ( 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ ( 𝐺 tsums 𝐹 ) ) )
13 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
14 13 submss ⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
15 4 14 syl ⊢ ( 𝜑 → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
16 15 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ ( Base ‘ 𝐺 ) )
17 eqid ⊢ ( TopOpen ‘ 𝐺 ) = ( TopOpen ‘ 𝐺 )
18 eqid ⊢ ( 𝒫 𝐴 ∩ Fin ) = ( 𝒫 𝐴 ∩ Fin )
19 5 15 fssd ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ( Base ‘ 𝐺 ) )
20 13 17 18 2 3 1 19 eltsms ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐺 tsums 𝐹 ) ↔ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ ∀ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ( 𝑥 ∈ 𝑢 → ∃ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑧 ⊆ 𝑦 → ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑢 ) ) ) ) )
21 20 baibd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑥 ∈ ( 𝐺 tsums 𝐹 ) ↔ ∀ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ( 𝑥 ∈ 𝑢 → ∃ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑧 ⊆ 𝑦 → ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑢 ) ) ) )
22 16 21 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑥 ∈ ( 𝐺 tsums 𝐹 ) ↔ ∀ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ( 𝑥 ∈ 𝑢 → ∃ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑧 ⊆ 𝑦 → ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑢 ) ) ) )
23 vex ⊢ 𝑢 ∈ V
24 23 inex1 ⊢ ( 𝑢 ∩ 𝑆 ) ∈ V
25 24 a1i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ) → ( 𝑢 ∩ 𝑆 ) ∈ V )
26 6 17 resstopn ⊢ ( ( TopOpen ‘ 𝐺 ) ↾t 𝑆 ) = ( TopOpen ‘ 𝐻 )
27 26 eleq2i ⊢ ( 𝑣 ∈ ( ( TopOpen ‘ 𝐺 ) ↾t 𝑆 ) ↔ 𝑣 ∈ ( TopOpen ‘ 𝐻 ) )
28 fvex ⊢ ( TopOpen ‘ 𝐺 ) ∈ V
29 elrest ⊢ ( ( ( TopOpen ‘ 𝐺 ) ∈ V ∧ 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ) → ( 𝑣 ∈ ( ( TopOpen ‘ 𝐺 ) ↾t 𝑆 ) ↔ ∃ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) 𝑣 = ( 𝑢 ∩ 𝑆 ) ) )
30 28 4 29 sylancr ⊢ ( 𝜑 → ( 𝑣 ∈ ( ( TopOpen ‘ 𝐺 ) ↾t 𝑆 ) ↔ ∃ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) 𝑣 = ( 𝑢 ∩ 𝑆 ) ) )
31 30 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑣 ∈ ( ( TopOpen ‘ 𝐺 ) ↾t 𝑆 ) ↔ ∃ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) 𝑣 = ( 𝑢 ∩ 𝑆 ) ) )
32 27 31 bitr3id ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑣 ∈ ( TopOpen ‘ 𝐻 ) ↔ ∃ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) 𝑣 = ( 𝑢 ∩ 𝑆 ) ) )
33 eleq2 ⊢ ( 𝑣 = ( 𝑢 ∩ 𝑆 ) → ( 𝑥 ∈ 𝑣 ↔ 𝑥 ∈ ( 𝑢 ∩ 𝑆 ) ) )
34 elin ⊢ ( 𝑥 ∈ ( 𝑢 ∩ 𝑆 ) ↔ ( 𝑥 ∈ 𝑢 ∧ 𝑥 ∈ 𝑆 ) )
35 34 rbaib ⊢ ( 𝑥 ∈ 𝑆 → ( 𝑥 ∈ ( 𝑢 ∩ 𝑆 ) ↔ 𝑥 ∈ 𝑢 ) )
36 35 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑥 ∈ ( 𝑢 ∩ 𝑆 ) ↔ 𝑥 ∈ 𝑢 ) )
37 33 36 sylan9bbr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑣 = ( 𝑢 ∩ 𝑆 ) ) → ( 𝑥 ∈ 𝑣 ↔ 𝑥 ∈ 𝑢 ) )
38 eleq2 ⊢ ( 𝑣 = ( 𝑢 ∩ 𝑆 ) → ( ( 𝐻 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑣 ↔ ( 𝐻 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ ( 𝑢 ∩ 𝑆 ) ) )
39 eqid ⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
40 eqid ⊢ ( 0g ‘ 𝐻 ) = ( 0g ‘ 𝐻 )
41 6 submmnd ⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) → 𝐻 ∈ Mnd )
42 4 41 syl ⊢ ( 𝜑 → 𝐻 ∈ Mnd )
43 6 subcmn ⊢ ( ( 𝐺 ∈ CMnd ∧ 𝐻 ∈ Mnd ) → 𝐻 ∈ CMnd )
44 2 42 43 syl2anc ⊢ ( 𝜑 → 𝐻 ∈ CMnd )
45 44 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝐻 ∈ CMnd )
46 elinel2 ⊢ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑦 ∈ Fin )
47 46 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑦 ∈ Fin )
48 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝐹 : 𝐴 ⟶ 𝑆 )
49 elfpw ⊢ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↔ ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ∈ Fin ) )
50 49 simplbi ⊢ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑦 ⊆ 𝐴 )
51 50 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑦 ⊆ 𝐴 )
52 48 51 fssresd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ 𝑆 )
53 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑆 = ( Base ‘ 𝐻 ) )
54 53 feq3d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ 𝑆 ↔ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ ( Base ‘ 𝐻 ) ) )
55 52 54 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ ( Base ‘ 𝐻 ) )
56 fvex ⊢ ( 0g ‘ 𝐻 ) ∈ V
57 56 a1i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 0g ‘ 𝐻 ) ∈ V )
58 52 47 57 fdmfifsupp ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐹 ↾ 𝑦 ) finSupp ( 0g ‘ 𝐻 ) )
59 39 40 45 47 55 58 gsumcl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐻 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ ( Base ‘ 𝐻 ) )
60 59 53 eleqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐻 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑆 )
61 elin ⊢ ( ( 𝐻 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ ( 𝑢 ∩ 𝑆 ) ↔ ( ( 𝐻 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑢 ∧ ( 𝐻 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑆 ) )
62 61 rbaib ⊢ ( ( 𝐻 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑆 → ( ( 𝐻 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ ( 𝑢 ∩ 𝑆 ) ↔ ( 𝐻 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑢 ) )
63 60 62 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( 𝐻 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ ( 𝑢 ∩ 𝑆 ) ↔ ( 𝐻 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑢 ) )
64 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑆 ∈ ( SubMnd ‘ 𝐺 ) )
65 47 64 52 6 gsumsubm ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) = ( 𝐻 Σg ( 𝐹 ↾ 𝑦 ) ) )
66 65 eleq1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑢 ↔ ( 𝐻 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑢 ) )
67 63 66 bitr4d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( 𝐻 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ ( 𝑢 ∩ 𝑆 ) ↔ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑢 ) )
68 38 67 sylan9bbr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑣 = ( 𝑢 ∩ 𝑆 ) ) → ( ( 𝐻 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑣 ↔ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑢 ) )
69 68 an32s ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑣 = ( 𝑢 ∩ 𝑆 ) ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( 𝐻 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑣 ↔ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑢 ) )
70 69 imbi2d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑣 = ( 𝑢 ∩ 𝑆 ) ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( 𝑧 ⊆ 𝑦 → ( 𝐻 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑣 ) ↔ ( 𝑧 ⊆ 𝑦 → ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑢 ) ) )
71 70 ralbidva ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑣 = ( 𝑢 ∩ 𝑆 ) ) → ( ∀ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑧 ⊆ 𝑦 → ( 𝐻 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑣 ) ↔ ∀ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑧 ⊆ 𝑦 → ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑢 ) ) )
72 71 rexbidv ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑣 = ( 𝑢 ∩ 𝑆 ) ) → ( ∃ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑧 ⊆ 𝑦 → ( 𝐻 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑣 ) ↔ ∃ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑧 ⊆ 𝑦 → ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑢 ) ) )
73 37 72 imbi12d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑣 = ( 𝑢 ∩ 𝑆 ) ) → ( ( 𝑥 ∈ 𝑣 → ∃ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑧 ⊆ 𝑦 → ( 𝐻 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑣 ) ) ↔ ( 𝑥 ∈ 𝑢 → ∃ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑧 ⊆ 𝑦 → ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑢 ) ) ) )
74 25 32 73 ralxfr2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ∀ 𝑣 ∈ ( TopOpen ‘ 𝐻 ) ( 𝑥 ∈ 𝑣 → ∃ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑧 ⊆ 𝑦 → ( 𝐻 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑣 ) ) ↔ ∀ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ( 𝑥 ∈ 𝑢 → ∃ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑧 ⊆ 𝑦 → ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑢 ) ) ) )
75 22 74 bitr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑥 ∈ ( 𝐺 tsums 𝐹 ) ↔ ∀ 𝑣 ∈ ( TopOpen ‘ 𝐻 ) ( 𝑥 ∈ 𝑣 → ∃ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑧 ⊆ 𝑦 → ( 𝐻 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑣 ) ) ) )
76 75 pm5.32da ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ ( 𝐺 tsums 𝐹 ) ) ↔ ( 𝑥 ∈ 𝑆 ∧ ∀ 𝑣 ∈ ( TopOpen ‘ 𝐻 ) ( 𝑥 ∈ 𝑣 → ∃ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑧 ⊆ 𝑦 → ( 𝐻 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑣 ) ) ) ) )
77 12 76 bitrid ⊢ ( 𝜑 → ( 𝑥 ∈ ( ( 𝐺 tsums 𝐹 ) ∩ 𝑆 ) ↔ ( 𝑥 ∈ 𝑆 ∧ ∀ 𝑣 ∈ ( TopOpen ‘ 𝐻 ) ( 𝑥 ∈ 𝑣 → ∃ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑧 ⊆ 𝑦 → ( 𝐻 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑣 ) ) ) ) )
78 eqid ⊢ ( TopOpen ‘ 𝐻 ) = ( TopOpen ‘ 𝐻 )
79 resstps ⊢ ( ( 𝐺 ∈ TopSp ∧ 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ) → ( 𝐺 ↾s 𝑆 ) ∈ TopSp )
80 3 4 79 syl2anc ⊢ ( 𝜑 → ( 𝐺 ↾s 𝑆 ) ∈ TopSp )
81 6 80 eqeltrid ⊢ ( 𝜑 → 𝐻 ∈ TopSp )
82 8 feq3d ⊢ ( 𝜑 → ( 𝐹 : 𝐴 ⟶ 𝑆 ↔ 𝐹 : 𝐴 ⟶ ( Base ‘ 𝐻 ) ) )
83 5 82 mpbid ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ( Base ‘ 𝐻 ) )
84 39 78 18 44 81 1 83 eltsms ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐻 tsums 𝐹 ) ↔ ( 𝑥 ∈ ( Base ‘ 𝐻 ) ∧ ∀ 𝑣 ∈ ( TopOpen ‘ 𝐻 ) ( 𝑥 ∈ 𝑣 → ∃ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑧 ⊆ 𝑦 → ( 𝐻 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑣 ) ) ) ) )
85 10 77 84 3bitr4rd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐻 tsums 𝐹 ) ↔ 𝑥 ∈ ( ( 𝐺 tsums 𝐹 ) ∩ 𝑆 ) ) )
86 85 eqrdv ⊢ ( 𝜑 → ( 𝐻 tsums 𝐹 ) = ( ( 𝐺 tsums 𝐹 ) ∩ 𝑆 ) )