| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | tsmsadd.b | . . . . . 6
⊢ 𝐵 = (Base‘𝐺) | 
| 2 |  | tsmsadd.1 | . . . . . 6
⊢ (𝜑 → 𝐺 ∈ CMnd) | 
| 3 |  | tsmsadd.2 | . . . . . . 7
⊢ (𝜑 → 𝐺 ∈ TopMnd) | 
| 4 |  | tmdtps 24084 | . . . . . . 7
⊢ (𝐺 ∈ TopMnd → 𝐺 ∈ TopSp) | 
| 5 | 3, 4 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝐺 ∈ TopSp) | 
| 6 |  | tsmsadd.a | . . . . . 6
⊢ (𝜑 → 𝐴 ∈ 𝑉) | 
| 7 |  | tsmsadd.f | . . . . . 6
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) | 
| 8 | 1, 2, 5, 6, 7 | tsmscl 24143 | . . . . 5
⊢ (𝜑 → (𝐺 tsums 𝐹) ⊆ 𝐵) | 
| 9 |  | tsmsadd.x | . . . . 5
⊢ (𝜑 → 𝑋 ∈ (𝐺 tsums 𝐹)) | 
| 10 | 8, 9 | sseldd 3984 | . . . 4
⊢ (𝜑 → 𝑋 ∈ 𝐵) | 
| 11 |  | tsmsadd.h | . . . . . 6
⊢ (𝜑 → 𝐻:𝐴⟶𝐵) | 
| 12 | 1, 2, 5, 6, 11 | tsmscl 24143 | . . . . 5
⊢ (𝜑 → (𝐺 tsums 𝐻) ⊆ 𝐵) | 
| 13 |  | tsmsadd.y | . . . . 5
⊢ (𝜑 → 𝑌 ∈ (𝐺 tsums 𝐻)) | 
| 14 | 12, 13 | sseldd 3984 | . . . 4
⊢ (𝜑 → 𝑌 ∈ 𝐵) | 
| 15 |  | tsmsadd.p | . . . . 5
⊢  + =
(+g‘𝐺) | 
| 16 |  | eqid 2737 | . . . . 5
⊢
(+𝑓‘𝐺) = (+𝑓‘𝐺) | 
| 17 | 1, 15, 16 | plusfval 18660 | . . . 4
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋(+𝑓‘𝐺)𝑌) = (𝑋 + 𝑌)) | 
| 18 | 10, 14, 17 | syl2anc 584 | . . 3
⊢ (𝜑 → (𝑋(+𝑓‘𝐺)𝑌) = (𝑋 + 𝑌)) | 
| 19 |  | eqid 2737 | . . . . . 6
⊢
(TopOpen‘𝐺) =
(TopOpen‘𝐺) | 
| 20 | 1, 19 | istps 22940 | . . . . 5
⊢ (𝐺 ∈ TopSp ↔
(TopOpen‘𝐺) ∈
(TopOn‘𝐵)) | 
| 21 | 5, 20 | sylib 218 | . . . 4
⊢ (𝜑 → (TopOpen‘𝐺) ∈ (TopOn‘𝐵)) | 
| 22 |  | eqid 2737 | . . . . . 6
⊢
(𝒫 𝐴 ∩
Fin) = (𝒫 𝐴 ∩
Fin) | 
| 23 |  | eqid 2737 | . . . . . 6
⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦 ⊆ 𝑧}) = (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦 ⊆ 𝑧}) | 
| 24 |  | eqid 2737 | . . . . . 6
⊢ ran
(𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦 ⊆ 𝑧}) = ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦 ⊆ 𝑧}) | 
| 25 | 22, 23, 24, 6 | tsmsfbas 24136 | . . . . 5
⊢ (𝜑 → ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦 ⊆ 𝑧}) ∈ (fBas‘(𝒫 𝐴 ∩ Fin))) | 
| 26 |  | fgcl 23886 | . . . . 5
⊢ (ran
(𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦 ⊆ 𝑧}) ∈ (fBas‘(𝒫 𝐴 ∩ Fin)) → ((𝒫
𝐴 ∩ Fin)filGenran
(𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦 ⊆ 𝑧})) ∈ (Fil‘(𝒫 𝐴 ∩ Fin))) | 
| 27 | 25, 26 | syl 17 | . . . 4
⊢ (𝜑 → ((𝒫 𝐴 ∩ Fin)filGenran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦 ⊆ 𝑧})) ∈ (Fil‘(𝒫 𝐴 ∩ Fin))) | 
| 28 | 1, 22, 2, 6, 7 | tsmslem1 24137 | . . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝐵) | 
| 29 | 1, 22, 2, 6, 11 | tsmslem1 24137 | . . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐺 Σg (𝐻 ↾ 𝑧)) ∈ 𝐵) | 
| 30 | 1, 19, 22, 24, 2, 6, 7 | tsmsval 24139 | . . . . 5
⊢ (𝜑 → (𝐺 tsums 𝐹) = (((TopOpen‘𝐺) fLimf ((𝒫 𝐴 ∩ Fin)filGenran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦 ⊆ 𝑧})))‘(𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑧))))) | 
| 31 | 9, 30 | eleqtrd 2843 | . . . 4
⊢ (𝜑 → 𝑋 ∈ (((TopOpen‘𝐺) fLimf ((𝒫 𝐴 ∩ Fin)filGenran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦 ⊆ 𝑧})))‘(𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑧))))) | 
| 32 | 1, 19, 22, 24, 2, 6, 11 | tsmsval 24139 | . . . . 5
⊢ (𝜑 → (𝐺 tsums 𝐻) = (((TopOpen‘𝐺) fLimf ((𝒫 𝐴 ∩ Fin)filGenran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦 ⊆ 𝑧})))‘(𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐻 ↾ 𝑧))))) | 
| 33 | 13, 32 | eleqtrd 2843 | . . . 4
⊢ (𝜑 → 𝑌 ∈ (((TopOpen‘𝐺) fLimf ((𝒫 𝐴 ∩ Fin)filGenran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦 ⊆ 𝑧})))‘(𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐻 ↾ 𝑧))))) | 
| 34 | 19, 16 | tmdcn 24091 | . . . . . 6
⊢ (𝐺 ∈ TopMnd →
(+𝑓‘𝐺) ∈ (((TopOpen‘𝐺) ×t (TopOpen‘𝐺)) Cn (TopOpen‘𝐺))) | 
| 35 | 3, 34 | syl 17 | . . . . 5
⊢ (𝜑 →
(+𝑓‘𝐺) ∈ (((TopOpen‘𝐺) ×t (TopOpen‘𝐺)) Cn (TopOpen‘𝐺))) | 
| 36 | 10, 14 | opelxpd 5724 | . . . . . 6
⊢ (𝜑 → 〈𝑋, 𝑌〉 ∈ (𝐵 × 𝐵)) | 
| 37 |  | txtopon 23599 | . . . . . . . 8
⊢
(((TopOpen‘𝐺)
∈ (TopOn‘𝐵)
∧ (TopOpen‘𝐺)
∈ (TopOn‘𝐵))
→ ((TopOpen‘𝐺)
×t (TopOpen‘𝐺)) ∈ (TopOn‘(𝐵 × 𝐵))) | 
| 38 | 21, 21, 37 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 → ((TopOpen‘𝐺) ×t
(TopOpen‘𝐺)) ∈
(TopOn‘(𝐵 ×
𝐵))) | 
| 39 |  | toponuni 22920 | . . . . . . 7
⊢
(((TopOpen‘𝐺)
×t (TopOpen‘𝐺)) ∈ (TopOn‘(𝐵 × 𝐵)) → (𝐵 × 𝐵) = ∪
((TopOpen‘𝐺)
×t (TopOpen‘𝐺))) | 
| 40 | 38, 39 | syl 17 | . . . . . 6
⊢ (𝜑 → (𝐵 × 𝐵) = ∪
((TopOpen‘𝐺)
×t (TopOpen‘𝐺))) | 
| 41 | 36, 40 | eleqtrd 2843 | . . . . 5
⊢ (𝜑 → 〈𝑋, 𝑌〉 ∈ ∪
((TopOpen‘𝐺)
×t (TopOpen‘𝐺))) | 
| 42 |  | eqid 2737 | . . . . . 6
⊢ ∪ ((TopOpen‘𝐺) ×t (TopOpen‘𝐺)) = ∪ ((TopOpen‘𝐺) ×t (TopOpen‘𝐺)) | 
| 43 | 42 | cncnpi 23286 | . . . . 5
⊢
(((+𝑓‘𝐺) ∈ (((TopOpen‘𝐺) ×t (TopOpen‘𝐺)) Cn (TopOpen‘𝐺)) ∧ 〈𝑋, 𝑌〉 ∈ ∪
((TopOpen‘𝐺)
×t (TopOpen‘𝐺))) →
(+𝑓‘𝐺) ∈ ((((TopOpen‘𝐺) ×t (TopOpen‘𝐺)) CnP (TopOpen‘𝐺))‘〈𝑋, 𝑌〉)) | 
| 44 | 35, 41, 43 | syl2anc 584 | . . . 4
⊢ (𝜑 →
(+𝑓‘𝐺) ∈ ((((TopOpen‘𝐺) ×t (TopOpen‘𝐺)) CnP (TopOpen‘𝐺))‘〈𝑋, 𝑌〉)) | 
| 45 | 21, 21, 27, 28, 29, 31, 33, 44 | flfcnp2 24015 | . . 3
⊢ (𝜑 → (𝑋(+𝑓‘𝐺)𝑌) ∈ (((TopOpen‘𝐺) fLimf ((𝒫 𝐴 ∩ Fin)filGenran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦 ⊆ 𝑧})))‘(𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((𝐺 Σg (𝐹 ↾ 𝑧))(+𝑓‘𝐺)(𝐺 Σg (𝐻 ↾ 𝑧)))))) | 
| 46 | 18, 45 | eqeltrrd 2842 | . 2
⊢ (𝜑 → (𝑋 + 𝑌) ∈ (((TopOpen‘𝐺) fLimf ((𝒫 𝐴 ∩ Fin)filGenran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦 ⊆ 𝑧})))‘(𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((𝐺 Σg (𝐹 ↾ 𝑧))(+𝑓‘𝐺)(𝐺 Σg (𝐻 ↾ 𝑧)))))) | 
| 47 |  | cmnmnd 19815 | . . . . . . 7
⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd) | 
| 48 | 2, 47 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝐺 ∈ Mnd) | 
| 49 | 1, 15 | mndcl 18755 | . . . . . . 7
⊢ ((𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵) | 
| 50 | 49 | 3expb 1121 | . . . . . 6
⊢ ((𝐺 ∈ Mnd ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) ∈ 𝐵) | 
| 51 | 48, 50 | sylan 580 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) ∈ 𝐵) | 
| 52 |  | inidm 4227 | . . . . 5
⊢ (𝐴 ∩ 𝐴) = 𝐴 | 
| 53 | 51, 7, 11, 6, 6, 52 | off 7715 | . . . 4
⊢ (𝜑 → (𝐹 ∘f + 𝐻):𝐴⟶𝐵) | 
| 54 | 1, 19, 22, 24, 2, 6, 53 | tsmsval 24139 | . . 3
⊢ (𝜑 → (𝐺 tsums (𝐹 ∘f + 𝐻)) = (((TopOpen‘𝐺) fLimf ((𝒫 𝐴 ∩ Fin)filGenran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦 ⊆ 𝑧})))‘(𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg ((𝐹 ∘f + 𝐻) ↾ 𝑧))))) | 
| 55 |  | eqid 2737 | . . . . . . 7
⊢
(0g‘𝐺) = (0g‘𝐺) | 
| 56 | 2 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐺 ∈ CMnd) | 
| 57 |  | elinel2 4202 | . . . . . . . 8
⊢ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) → 𝑧 ∈ Fin) | 
| 58 | 57 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑧 ∈ Fin) | 
| 59 |  | elfpw 9394 | . . . . . . . . 9
⊢ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝑧 ⊆ 𝐴 ∧ 𝑧 ∈ Fin)) | 
| 60 | 59 | simplbi 497 | . . . . . . . 8
⊢ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) → 𝑧 ⊆ 𝐴) | 
| 61 |  | fssres 6774 | . . . . . . . 8
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑧 ⊆ 𝐴) → (𝐹 ↾ 𝑧):𝑧⟶𝐵) | 
| 62 | 7, 60, 61 | syl2an 596 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ 𝑧):𝑧⟶𝐵) | 
| 63 |  | fssres 6774 | . . . . . . . 8
⊢ ((𝐻:𝐴⟶𝐵 ∧ 𝑧 ⊆ 𝐴) → (𝐻 ↾ 𝑧):𝑧⟶𝐵) | 
| 64 | 11, 60, 63 | syl2an 596 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐻 ↾ 𝑧):𝑧⟶𝐵) | 
| 65 |  | fvexd 6921 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) →
(0g‘𝐺)
∈ V) | 
| 66 | 62, 58, 65 | fdmfifsupp 9415 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ 𝑧) finSupp (0g‘𝐺)) | 
| 67 | 64, 58, 65 | fdmfifsupp 9415 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐻 ↾ 𝑧) finSupp (0g‘𝐺)) | 
| 68 | 1, 55, 15, 56, 58, 62, 64, 66, 67 | gsumadd 19941 | . . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐺 Σg ((𝐹 ↾ 𝑧) ∘f + (𝐻 ↾ 𝑧))) = ((𝐺 Σg (𝐹 ↾ 𝑧)) + (𝐺 Σg (𝐻 ↾ 𝑧)))) | 
| 69 | 7, 6 | fexd 7247 | . . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ V) | 
| 70 | 11, 6 | fexd 7247 | . . . . . . . . 9
⊢ (𝜑 → 𝐻 ∈ V) | 
| 71 |  | offres 8008 | . . . . . . . . 9
⊢ ((𝐹 ∈ V ∧ 𝐻 ∈ V) → ((𝐹 ∘f + 𝐻) ↾ 𝑧) = ((𝐹 ↾ 𝑧) ∘f + (𝐻 ↾ 𝑧))) | 
| 72 | 69, 70, 71 | syl2anc 584 | . . . . . . . 8
⊢ (𝜑 → ((𝐹 ∘f + 𝐻) ↾ 𝑧) = ((𝐹 ↾ 𝑧) ∘f + (𝐻 ↾ 𝑧))) | 
| 73 | 72 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → ((𝐹 ∘f + 𝐻) ↾ 𝑧) = ((𝐹 ↾ 𝑧) ∘f + (𝐻 ↾ 𝑧))) | 
| 74 | 73 | oveq2d 7447 | . . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐺 Σg ((𝐹 ∘f + 𝐻) ↾ 𝑧)) = (𝐺 Σg ((𝐹 ↾ 𝑧) ∘f + (𝐻 ↾ 𝑧)))) | 
| 75 | 1, 15, 16 | plusfval 18660 | . . . . . . 7
⊢ (((𝐺 Σg
(𝐹 ↾ 𝑧)) ∈ 𝐵 ∧ (𝐺 Σg (𝐻 ↾ 𝑧)) ∈ 𝐵) → ((𝐺 Σg (𝐹 ↾ 𝑧))(+𝑓‘𝐺)(𝐺 Σg (𝐻 ↾ 𝑧))) = ((𝐺 Σg (𝐹 ↾ 𝑧)) + (𝐺 Σg (𝐻 ↾ 𝑧)))) | 
| 76 | 28, 29, 75 | syl2anc 584 | . . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → ((𝐺 Σg (𝐹 ↾ 𝑧))(+𝑓‘𝐺)(𝐺 Σg (𝐻 ↾ 𝑧))) = ((𝐺 Σg (𝐹 ↾ 𝑧)) + (𝐺 Σg (𝐻 ↾ 𝑧)))) | 
| 77 | 68, 74, 76 | 3eqtr4d 2787 | . . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐺 Σg ((𝐹 ∘f + 𝐻) ↾ 𝑧)) = ((𝐺 Σg (𝐹 ↾ 𝑧))(+𝑓‘𝐺)(𝐺 Σg (𝐻 ↾ 𝑧)))) | 
| 78 | 77 | mpteq2dva 5242 | . . . 4
⊢ (𝜑 → (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg ((𝐹 ∘f + 𝐻) ↾ 𝑧))) = (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((𝐺 Σg (𝐹 ↾ 𝑧))(+𝑓‘𝐺)(𝐺 Σg (𝐻 ↾ 𝑧))))) | 
| 79 | 78 | fveq2d 6910 | . . 3
⊢ (𝜑 → (((TopOpen‘𝐺) fLimf ((𝒫 𝐴 ∩ Fin)filGenran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦 ⊆ 𝑧})))‘(𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg ((𝐹 ∘f + 𝐻) ↾ 𝑧)))) = (((TopOpen‘𝐺) fLimf ((𝒫 𝐴 ∩ Fin)filGenran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦 ⊆ 𝑧})))‘(𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((𝐺 Σg (𝐹 ↾ 𝑧))(+𝑓‘𝐺)(𝐺 Σg (𝐻 ↾ 𝑧)))))) | 
| 80 | 54, 79 | eqtrd 2777 | . 2
⊢ (𝜑 → (𝐺 tsums (𝐹 ∘f + 𝐻)) = (((TopOpen‘𝐺) fLimf ((𝒫 𝐴 ∩ Fin)filGenran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦 ⊆ 𝑧})))‘(𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((𝐺 Σg (𝐹 ↾ 𝑧))(+𝑓‘𝐺)(𝐺 Σg (𝐻 ↾ 𝑧)))))) | 
| 81 | 46, 80 | eleqtrrd 2844 | 1
⊢ (𝜑 → (𝑋 + 𝑌) ∈ (𝐺 tsums (𝐹 ∘f + 𝐻))) |