Metamath Proof Explorer

Theorem tsmsadd

Description: The sum of two infinite group sums. (Contributed by Mario Carneiro, 19-Sep-2015) (Proof shortened by AV, 24-Jul-2019)

Ref Expression
Hypotheses tsmsadd.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
tsmsadd.p ⊢ + = ( +g ‘ 𝐺 )
tsmsadd.1 ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
tsmsadd.2 ⊢ ( 𝜑 → 𝐺 ∈ TopMnd )
tsmsadd.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
tsmsadd.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
tsmsadd.h ⊢ ( 𝜑 → 𝐻 : 𝐴 ⟶ 𝐵 )
tsmsadd.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐺 tsums 𝐹 ) )
tsmsadd.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐺 tsums 𝐻 ) )
Assertion tsmsadd ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ ( 𝐺 tsums ( 𝐹 ∘f + 𝐻 ) ) )

Proof

Step Hyp Ref Expression
1 tsmsadd.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 tsmsadd.p ⊢ + = ( +g ‘ 𝐺 )
3 tsmsadd.1 ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
4 tsmsadd.2 ⊢ ( 𝜑 → 𝐺 ∈ TopMnd )
5 tsmsadd.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
6 tsmsadd.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
7 tsmsadd.h ⊢ ( 𝜑 → 𝐻 : 𝐴 ⟶ 𝐵 )
8 tsmsadd.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐺 tsums 𝐹 ) )
9 tsmsadd.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐺 tsums 𝐻 ) )
10 tmdtps ⊢ ( 𝐺 ∈ TopMnd → 𝐺 ∈ TopSp )
11 4 10 syl ⊢ ( 𝜑 → 𝐺 ∈ TopSp )
12 1 3 11 5 6 tsmscl ⊢ ( 𝜑 → ( 𝐺 tsums 𝐹 ) ⊆ 𝐵 )
13 12 8 sseldd ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
14 1 3 11 5 7 tsmscl ⊢ ( 𝜑 → ( 𝐺 tsums 𝐻 ) ⊆ 𝐵 )
15 14 9 sseldd ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
16 eqid ⊢ ( +𝑓 ‘ 𝐺 ) = ( +𝑓 ‘ 𝐺 )
17 1 2 16 plusfval ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ( +𝑓 ‘ 𝐺 ) 𝑌 ) = ( 𝑋 + 𝑌 ) )
18 13 15 17 syl2anc ⊢ ( 𝜑 → ( 𝑋 ( +𝑓 ‘ 𝐺 ) 𝑌 ) = ( 𝑋 + 𝑌 ) )
19 eqid ⊢ ( TopOpen ‘ 𝐺 ) = ( TopOpen ‘ 𝐺 )
20 1 19 istps ⊢ ( 𝐺 ∈ TopSp ↔ ( TopOpen ‘ 𝐺 ) ∈ ( TopOn ‘ 𝐵 ) )
21 11 20 sylib ⊢ ( 𝜑 → ( TopOpen ‘ 𝐺 ) ∈ ( TopOn ‘ 𝐵 ) )
22 eqid ⊢ ( 𝒫 𝐴 ∩ Fin ) = ( 𝒫 𝐴 ∩ Fin )
23 eqid ⊢ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦 ⊆ 𝑧 } ) = ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦 ⊆ 𝑧 } )
24 eqid ⊢ ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦 ⊆ 𝑧 } ) = ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦 ⊆ 𝑧 } )
25 22 23 24 5 tsmsfbas ⊢ ( 𝜑 → ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦 ⊆ 𝑧 } ) ∈ ( fBas ‘ ( 𝒫 𝐴 ∩ Fin ) ) )
26 fgcl ⊢ ( ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦 ⊆ 𝑧 } ) ∈ ( fBas ‘ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦 ⊆ 𝑧 } ) ) ∈ ( Fil ‘ ( 𝒫 𝐴 ∩ Fin ) ) )
27 25 26 syl ⊢ ( 𝜑 → ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦 ⊆ 𝑧 } ) ) ∈ ( Fil ‘ ( 𝒫 𝐴 ∩ Fin ) ) )
28 1 22 3 5 6 tsmslem1 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝐵 )
29 1 22 3 5 7 tsmslem1 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐺 Σg ( 𝐻 ↾ 𝑧 ) ) ∈ 𝐵 )
30 1 19 22 24 3 5 6 tsmsval ⊢ ( 𝜑 → ( 𝐺 tsums 𝐹 ) = ( ( ( TopOpen ‘ 𝐺 ) fLimf ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦 ⊆ 𝑧 } ) ) ) ‘ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ) ) )
31 8 30 eleqtrd ⊢ ( 𝜑 → 𝑋 ∈ ( ( ( TopOpen ‘ 𝐺 ) fLimf ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦 ⊆ 𝑧 } ) ) ) ‘ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ) ) )
32 1 19 22 24 3 5 7 tsmsval ⊢ ( 𝜑 → ( 𝐺 tsums 𝐻 ) = ( ( ( TopOpen ‘ 𝐺 ) fLimf ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦 ⊆ 𝑧 } ) ) ) ‘ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐻 ↾ 𝑧 ) ) ) ) )
33 9 32 eleqtrd ⊢ ( 𝜑 → 𝑌 ∈ ( ( ( TopOpen ‘ 𝐺 ) fLimf ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦 ⊆ 𝑧 } ) ) ) ‘ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐻 ↾ 𝑧 ) ) ) ) )
34 19 16 tmdcn ⊢ ( 𝐺 ∈ TopMnd → ( +𝑓 ‘ 𝐺 ) ∈ ( ( ( TopOpen ‘ 𝐺 ) ×t ( TopOpen ‘ 𝐺 ) ) Cn ( TopOpen ‘ 𝐺 ) ) )
35 4 34 syl ⊢ ( 𝜑 → ( +𝑓 ‘ 𝐺 ) ∈ ( ( ( TopOpen ‘ 𝐺 ) ×t ( TopOpen ‘ 𝐺 ) ) Cn ( TopOpen ‘ 𝐺 ) ) )
36 13 15 opelxpd ⊢ ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝐵 × 𝐵 ) )
37 txtopon ⊢ ( ( ( TopOpen ‘ 𝐺 ) ∈ ( TopOn ‘ 𝐵 ) ∧ ( TopOpen ‘ 𝐺 ) ∈ ( TopOn ‘ 𝐵 ) ) → ( ( TopOpen ‘ 𝐺 ) ×t ( TopOpen ‘ 𝐺 ) ) ∈ ( TopOn ‘ ( 𝐵 × 𝐵 ) ) )
38 21 21 37 syl2anc ⊢ ( 𝜑 → ( ( TopOpen ‘ 𝐺 ) ×t ( TopOpen ‘ 𝐺 ) ) ∈ ( TopOn ‘ ( 𝐵 × 𝐵 ) ) )
39 toponuni ⊢ ( ( ( TopOpen ‘ 𝐺 ) ×t ( TopOpen ‘ 𝐺 ) ) ∈ ( TopOn ‘ ( 𝐵 × 𝐵 ) ) → ( 𝐵 × 𝐵 ) = ∪ ( ( TopOpen ‘ 𝐺 ) ×t ( TopOpen ‘ 𝐺 ) ) )
40 38 39 syl ⊢ ( 𝜑 → ( 𝐵 × 𝐵 ) = ∪ ( ( TopOpen ‘ 𝐺 ) ×t ( TopOpen ‘ 𝐺 ) ) )
41 36 40 eleqtrd ⊢ ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ ∈ ∪ ( ( TopOpen ‘ 𝐺 ) ×t ( TopOpen ‘ 𝐺 ) ) )
42 eqid ⊢ ∪ ( ( TopOpen ‘ 𝐺 ) ×t ( TopOpen ‘ 𝐺 ) ) = ∪ ( ( TopOpen ‘ 𝐺 ) ×t ( TopOpen ‘ 𝐺 ) )
43 42 cncnpi ⊢ ( ( ( +𝑓 ‘ 𝐺 ) ∈ ( ( ( TopOpen ‘ 𝐺 ) ×t ( TopOpen ‘ 𝐺 ) ) Cn ( TopOpen ‘ 𝐺 ) ) ∧ ⟨ 𝑋 , 𝑌 ⟩ ∈ ∪ ( ( TopOpen ‘ 𝐺 ) ×t ( TopOpen ‘ 𝐺 ) ) ) → ( +𝑓 ‘ 𝐺 ) ∈ ( ( ( ( TopOpen ‘ 𝐺 ) ×t ( TopOpen ‘ 𝐺 ) ) CnP ( TopOpen ‘ 𝐺 ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
44 35 41 43 syl2anc ⊢ ( 𝜑 → ( +𝑓 ‘ 𝐺 ) ∈ ( ( ( ( TopOpen ‘ 𝐺 ) ×t ( TopOpen ‘ 𝐺 ) ) CnP ( TopOpen ‘ 𝐺 ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
45 21 21 27 28 29 31 33 44 flfcnp2 ⊢ ( 𝜑 → ( 𝑋 ( +𝑓 ‘ 𝐺 ) 𝑌 ) ∈ ( ( ( TopOpen ‘ 𝐺 ) fLimf ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦 ⊆ 𝑧 } ) ) ) ‘ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ( +𝑓 ‘ 𝐺 ) ( 𝐺 Σg ( 𝐻 ↾ 𝑧 ) ) ) ) ) )
46 18 45 eqeltrrd ⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ ( ( ( TopOpen ‘ 𝐺 ) fLimf ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦 ⊆ 𝑧 } ) ) ) ‘ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ( +𝑓 ‘ 𝐺 ) ( 𝐺 Σg ( 𝐻 ↾ 𝑧 ) ) ) ) ) )
47 cmnmnd ⊢ ( 𝐺 ∈ CMnd → 𝐺 ∈ Mnd )
48 3 47 syl ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
49 1 2 mndcl ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
50 49 3expb ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
51 48 50 sylan ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
52 inidm ⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴
53 51 6 7 5 5 52 off ⊢ ( 𝜑 → ( 𝐹 ∘f + 𝐻 ) : 𝐴 ⟶ 𝐵 )
54 1 19 22 24 3 5 53 tsmsval ⊢ ( 𝜑 → ( 𝐺 tsums ( 𝐹 ∘f + 𝐻 ) ) = ( ( ( TopOpen ‘ 𝐺 ) fLimf ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦 ⊆ 𝑧 } ) ) ) ‘ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( ( 𝐹 ∘f + 𝐻 ) ↾ 𝑧 ) ) ) ) )
55 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
56 3 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝐺 ∈ CMnd )
57 elinel2 ⊢ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑧 ∈ Fin )
58 57 adantl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑧 ∈ Fin )
59 elfpw ⊢ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↔ ( 𝑧 ⊆ 𝐴 ∧ 𝑧 ∈ Fin ) )
60 59 simplbi ⊢ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑧 ⊆ 𝐴 )
61 fssres ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑧 ⊆ 𝐴 ) → ( 𝐹 ↾ 𝑧 ) : 𝑧 ⟶ 𝐵 )
62 6 60 61 syl2an ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐹 ↾ 𝑧 ) : 𝑧 ⟶ 𝐵 )
63 fssres ⊢ ( ( 𝐻 : 𝐴 ⟶ 𝐵 ∧ 𝑧 ⊆ 𝐴 ) → ( 𝐻 ↾ 𝑧 ) : 𝑧 ⟶ 𝐵 )
64 7 60 63 syl2an ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐻 ↾ 𝑧 ) : 𝑧 ⟶ 𝐵 )
65 fvexd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 0g ‘ 𝐺 ) ∈ V )
66 62 58 65 fdmfifsupp ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐹 ↾ 𝑧 ) finSupp ( 0g ‘ 𝐺 ) )
67 64 58 65 fdmfifsupp ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐻 ↾ 𝑧 ) finSupp ( 0g ‘ 𝐺 ) )
68 1 55 2 56 58 62 64 66 67 gsumadd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑧 ) ∘f + ( 𝐻 ↾ 𝑧 ) ) ) = ( ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) + ( 𝐺 Σg ( 𝐻 ↾ 𝑧 ) ) ) )
69 1 fvexi ⊢ 𝐵 ∈ V
70 69 a1i ⊢ ( 𝜑 → 𝐵 ∈ V )
71 fex2 ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ V ) → 𝐹 ∈ V )
72 6 5 70 71 syl3anc ⊢ ( 𝜑 → 𝐹 ∈ V )
73 fex2 ⊢ ( ( 𝐻 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ V ) → 𝐻 ∈ V )
74 7 5 70 73 syl3anc ⊢ ( 𝜑 → 𝐻 ∈ V )
75 offres ⊢ ( ( 𝐹 ∈ V ∧ 𝐻 ∈ V ) → ( ( 𝐹 ∘f + 𝐻 ) ↾ 𝑧 ) = ( ( 𝐹 ↾ 𝑧 ) ∘f + ( 𝐻 ↾ 𝑧 ) ) )
76 72 74 75 syl2anc ⊢ ( 𝜑 → ( ( 𝐹 ∘f + 𝐻 ) ↾ 𝑧 ) = ( ( 𝐹 ↾ 𝑧 ) ∘f + ( 𝐻 ↾ 𝑧 ) ) )
77 76 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( 𝐹 ∘f + 𝐻 ) ↾ 𝑧 ) = ( ( 𝐹 ↾ 𝑧 ) ∘f + ( 𝐻 ↾ 𝑧 ) ) )
78 77 oveq2d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐺 Σg ( ( 𝐹 ∘f + 𝐻 ) ↾ 𝑧 ) ) = ( 𝐺 Σg ( ( 𝐹 ↾ 𝑧 ) ∘f + ( 𝐻 ↾ 𝑧 ) ) ) )
79 1 2 16 plusfval ⊢ ( ( ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝐵 ∧ ( 𝐺 Σg ( 𝐻 ↾ 𝑧 ) ) ∈ 𝐵 ) → ( ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ( +𝑓 ‘ 𝐺 ) ( 𝐺 Σg ( 𝐻 ↾ 𝑧 ) ) ) = ( ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) + ( 𝐺 Σg ( 𝐻 ↾ 𝑧 ) ) ) )
80 28 29 79 syl2anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ( +𝑓 ‘ 𝐺 ) ( 𝐺 Σg ( 𝐻 ↾ 𝑧 ) ) ) = ( ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) + ( 𝐺 Σg ( 𝐻 ↾ 𝑧 ) ) ) )
81 68 78 80 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐺 Σg ( ( 𝐹 ∘f + 𝐻 ) ↾ 𝑧 ) ) = ( ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ( +𝑓 ‘ 𝐺 ) ( 𝐺 Σg ( 𝐻 ↾ 𝑧 ) ) ) )
82 81 mpteq2dva ⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( ( 𝐹 ∘f + 𝐻 ) ↾ 𝑧 ) ) ) = ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ( +𝑓 ‘ 𝐺 ) ( 𝐺 Σg ( 𝐻 ↾ 𝑧 ) ) ) ) )
83 82 fveq2d ⊢ ( 𝜑 → ( ( ( TopOpen ‘ 𝐺 ) fLimf ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦 ⊆ 𝑧 } ) ) ) ‘ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( ( 𝐹 ∘f + 𝐻 ) ↾ 𝑧 ) ) ) ) = ( ( ( TopOpen ‘ 𝐺 ) fLimf ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦 ⊆ 𝑧 } ) ) ) ‘ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ( +𝑓 ‘ 𝐺 ) ( 𝐺 Σg ( 𝐻 ↾ 𝑧 ) ) ) ) ) )
84 54 83 eqtrd ⊢ ( 𝜑 → ( 𝐺 tsums ( 𝐹 ∘f + 𝐻 ) ) = ( ( ( TopOpen ‘ 𝐺 ) fLimf ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦 ⊆ 𝑧 } ) ) ) ‘ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ( +𝑓 ‘ 𝐺 ) ( 𝐺 Σg ( 𝐻 ↾ 𝑧 ) ) ) ) ) )
85 46 84 eleqtrrd ⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ ( 𝐺 tsums ( 𝐹 ∘f + 𝐻 ) ) )