Step | Hyp | Ref
| Expression |
1 | | tsmsadd.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐺) |
2 | | tsmsadd.1 |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ CMnd) |
3 | | tsmsadd.2 |
. . . . . . 7
⊢ (𝜑 → 𝐺 ∈ TopMnd) |
4 | | tmdtps 21690 |
. . . . . . 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 21748 |
. . . . 5
⊢ (𝜑 → (𝐺 tsums 𝐹) ⊆ 𝐵) |
9 | | tsmsadd.x |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ (𝐺 tsums 𝐹)) |
10 | 8, 9 | sseldd 3569 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
11 | | tsmsadd.h |
. . . . . 6
⊢ (𝜑 → 𝐻:𝐴⟶𝐵) |
12 | 1, 2, 5, 6, 11 | tsmscl 21748 |
. . . . 5
⊢ (𝜑 → (𝐺 tsums 𝐻) ⊆ 𝐵) |
13 | | tsmsadd.y |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ (𝐺 tsums 𝐻)) |
14 | 12, 13 | sseldd 3569 |
. . . 4
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
15 | | tsmsadd.p |
. . . . 5
⊢ + =
(+g‘𝐺) |
16 | | eqid 2610 |
. . . . 5
⊢
(+𝑓‘𝐺) = (+𝑓‘𝐺) |
17 | 1, 15, 16 | plusfval 17071 |
. . . 4
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋(+𝑓‘𝐺)𝑌) = (𝑋 + 𝑌)) |
18 | 10, 14, 17 | syl2anc 691 |
. . 3
⊢ (𝜑 → (𝑋(+𝑓‘𝐺)𝑌) = (𝑋 + 𝑌)) |
19 | | eqid 2610 |
. . . . . 6
⊢
(TopOpen‘𝐺) =
(TopOpen‘𝐺) |
20 | 1, 19 | istps 20551 |
. . . . 5
⊢ (𝐺 ∈ TopSp ↔
(TopOpen‘𝐺) ∈
(TopOn‘𝐵)) |
21 | 5, 20 | sylib 207 |
. . . 4
⊢ (𝜑 → (TopOpen‘𝐺) ∈ (TopOn‘𝐵)) |
22 | | eqid 2610 |
. . . . . 6
⊢
(𝒫 𝐴 ∩
Fin) = (𝒫 𝐴 ∩
Fin) |
23 | | eqid 2610 |
. . . . . 6
⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦 ⊆ 𝑧}) = (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦 ⊆ 𝑧}) |
24 | | eqid 2610 |
. . . . . 6
⊢ ran
(𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦 ⊆ 𝑧}) = ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦 ⊆ 𝑧}) |
25 | 22, 23, 24, 6 | tsmsfbas 21741 |
. . . . 5
⊢ (𝜑 → ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦 ⊆ 𝑧}) ∈ (fBas‘(𝒫 𝐴 ∩ Fin))) |
26 | | fgcl 21492 |
. . . . 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 21742 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝐵) |
29 | 1, 22, 2, 6, 11 | tsmslem1 21742 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐺 Σg (𝐻 ↾ 𝑧)) ∈ 𝐵) |
30 | 1, 19, 22, 24, 2, 6, 7 | tsmsval 21744 |
. . . . 5
⊢ (𝜑 → (𝐺 tsums 𝐹) = (((TopOpen‘𝐺) fLimf ((𝒫 𝐴 ∩ Fin)filGenran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦 ⊆ 𝑧})))‘(𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑧))))) |
31 | 9, 30 | eleqtrd 2690 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ (((TopOpen‘𝐺) fLimf ((𝒫 𝐴 ∩ Fin)filGenran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦 ⊆ 𝑧})))‘(𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑧))))) |
32 | 1, 19, 22, 24, 2, 6, 11 | tsmsval 21744 |
. . . . 5
⊢ (𝜑 → (𝐺 tsums 𝐻) = (((TopOpen‘𝐺) fLimf ((𝒫 𝐴 ∩ Fin)filGenran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦 ⊆ 𝑧})))‘(𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐻 ↾ 𝑧))))) |
33 | 13, 32 | eleqtrd 2690 |
. . . 4
⊢ (𝜑 → 𝑌 ∈ (((TopOpen‘𝐺) fLimf ((𝒫 𝐴 ∩ Fin)filGenran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦 ⊆ 𝑧})))‘(𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐻 ↾ 𝑧))))) |
34 | 19, 16 | tmdcn 21697 |
. . . . . 6
⊢ (𝐺 ∈ TopMnd →
(+𝑓‘𝐺) ∈ (((TopOpen‘𝐺) ×t (TopOpen‘𝐺)) Cn (TopOpen‘𝐺))) |
35 | 3, 34 | syl 17 |
. . . . 5
⊢ (𝜑 →
(+𝑓‘𝐺) ∈ (((TopOpen‘𝐺) ×t (TopOpen‘𝐺)) Cn (TopOpen‘𝐺))) |
36 | | opelxpi 5072 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 〈𝑋, 𝑌〉 ∈ (𝐵 × 𝐵)) |
37 | 10, 14, 36 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → 〈𝑋, 𝑌〉 ∈ (𝐵 × 𝐵)) |
38 | | txtopon 21204 |
. . . . . . . 8
⊢
(((TopOpen‘𝐺)
∈ (TopOn‘𝐵)
∧ (TopOpen‘𝐺)
∈ (TopOn‘𝐵))
→ ((TopOpen‘𝐺)
×t (TopOpen‘𝐺)) ∈ (TopOn‘(𝐵 × 𝐵))) |
39 | 21, 21, 38 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → ((TopOpen‘𝐺) ×t
(TopOpen‘𝐺)) ∈
(TopOn‘(𝐵 ×
𝐵))) |
40 | | toponuni 20542 |
. . . . . . 7
⊢
(((TopOpen‘𝐺)
×t (TopOpen‘𝐺)) ∈ (TopOn‘(𝐵 × 𝐵)) → (𝐵 × 𝐵) = ∪
((TopOpen‘𝐺)
×t (TopOpen‘𝐺))) |
41 | 39, 40 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝐵 × 𝐵) = ∪
((TopOpen‘𝐺)
×t (TopOpen‘𝐺))) |
42 | 37, 41 | eleqtrd 2690 |
. . . . 5
⊢ (𝜑 → 〈𝑋, 𝑌〉 ∈ ∪
((TopOpen‘𝐺)
×t (TopOpen‘𝐺))) |
43 | | eqid 2610 |
. . . . . 6
⊢ ∪ ((TopOpen‘𝐺) ×t (TopOpen‘𝐺)) = ∪ ((TopOpen‘𝐺) ×t (TopOpen‘𝐺)) |
44 | 43 | cncnpi 20892 |
. . . . 5
⊢
(((+𝑓‘𝐺) ∈ (((TopOpen‘𝐺) ×t (TopOpen‘𝐺)) Cn (TopOpen‘𝐺)) ∧ 〈𝑋, 𝑌〉 ∈ ∪
((TopOpen‘𝐺)
×t (TopOpen‘𝐺))) →
(+𝑓‘𝐺) ∈ ((((TopOpen‘𝐺) ×t (TopOpen‘𝐺)) CnP (TopOpen‘𝐺))‘〈𝑋, 𝑌〉)) |
45 | 35, 42, 44 | syl2anc 691 |
. . . 4
⊢ (𝜑 →
(+𝑓‘𝐺) ∈ ((((TopOpen‘𝐺) ×t (TopOpen‘𝐺)) CnP (TopOpen‘𝐺))‘〈𝑋, 𝑌〉)) |
46 | 21, 21, 27, 28, 29, 31, 33, 45 | flfcnp2 21621 |
. . 3
⊢ (𝜑 → (𝑋(+𝑓‘𝐺)𝑌) ∈ (((TopOpen‘𝐺) fLimf ((𝒫 𝐴 ∩ Fin)filGenran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦 ⊆ 𝑧})))‘(𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((𝐺 Σg (𝐹 ↾ 𝑧))(+𝑓‘𝐺)(𝐺 Σg (𝐻 ↾ 𝑧)))))) |
47 | 18, 46 | eqeltrrd 2689 |
. 2
⊢ (𝜑 → (𝑋 + 𝑌) ∈ (((TopOpen‘𝐺) fLimf ((𝒫 𝐴 ∩ Fin)filGenran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦 ⊆ 𝑧})))‘(𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((𝐺 Σg (𝐹 ↾ 𝑧))(+𝑓‘𝐺)(𝐺 Σg (𝐻 ↾ 𝑧)))))) |
48 | | cmnmnd 18031 |
. . . . . . 7
⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd) |
49 | 2, 48 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ Mnd) |
50 | 1, 15 | mndcl 17124 |
. . . . . . 7
⊢ ((𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵) |
51 | 50 | 3expb 1258 |
. . . . . 6
⊢ ((𝐺 ∈ Mnd ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) ∈ 𝐵) |
52 | 49, 51 | sylan 487 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) ∈ 𝐵) |
53 | | inidm 3784 |
. . . . 5
⊢ (𝐴 ∩ 𝐴) = 𝐴 |
54 | 52, 7, 11, 6, 6, 53 | off 6810 |
. . . 4
⊢ (𝜑 → (𝐹 ∘𝑓 + 𝐻):𝐴⟶𝐵) |
55 | 1, 19, 22, 24, 2, 6, 54 | tsmsval 21744 |
. . 3
⊢ (𝜑 → (𝐺 tsums (𝐹 ∘𝑓 + 𝐻)) = (((TopOpen‘𝐺) fLimf ((𝒫 𝐴 ∩ Fin)filGenran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦 ⊆ 𝑧})))‘(𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg ((𝐹 ∘𝑓
+ 𝐻) ↾ 𝑧))))) |
56 | | eqid 2610 |
. . . . . . 7
⊢
(0g‘𝐺) = (0g‘𝐺) |
57 | 2 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐺 ∈ CMnd) |
58 | | elfpw 8151 |
. . . . . . . . 9
⊢ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝑧 ⊆ 𝐴 ∧ 𝑧 ∈ Fin)) |
59 | 58 | simprbi 479 |
. . . . . . . 8
⊢ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) → 𝑧 ∈ Fin) |
60 | 59 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑧 ∈ Fin) |
61 | 58 | simplbi 475 |
. . . . . . . 8
⊢ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) → 𝑧 ⊆ 𝐴) |
62 | | fssres 5983 |
. . . . . . . 8
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑧 ⊆ 𝐴) → (𝐹 ↾ 𝑧):𝑧⟶𝐵) |
63 | 7, 61, 62 | syl2an 493 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ 𝑧):𝑧⟶𝐵) |
64 | | fssres 5983 |
. . . . . . . 8
⊢ ((𝐻:𝐴⟶𝐵 ∧ 𝑧 ⊆ 𝐴) → (𝐻 ↾ 𝑧):𝑧⟶𝐵) |
65 | 11, 61, 64 | syl2an 493 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐻 ↾ 𝑧):𝑧⟶𝐵) |
66 | | fvex 6113 |
. . . . . . . . 9
⊢
(0g‘𝐺) ∈ V |
67 | 66 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) →
(0g‘𝐺)
∈ V) |
68 | 63, 60, 67 | fdmfifsupp 8168 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ 𝑧) finSupp (0g‘𝐺)) |
69 | 65, 60, 67 | fdmfifsupp 8168 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐻 ↾ 𝑧) finSupp (0g‘𝐺)) |
70 | 1, 56, 15, 57, 60, 63, 65, 68, 69 | gsumadd 18146 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐺 Σg ((𝐹 ↾ 𝑧) ∘𝑓 + (𝐻 ↾ 𝑧))) = ((𝐺 Σg (𝐹 ↾ 𝑧)) + (𝐺 Σg (𝐻 ↾ 𝑧)))) |
71 | | fvex 6113 |
. . . . . . . . . . . 12
⊢
(Base‘𝐺)
∈ V |
72 | 1, 71 | eqeltri 2684 |
. . . . . . . . . . 11
⊢ 𝐵 ∈ V |
73 | 72 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ V) |
74 | | fex2 7014 |
. . . . . . . . . 10
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ V) → 𝐹 ∈ V) |
75 | 7, 6, 73, 74 | syl3anc 1318 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ V) |
76 | | fex2 7014 |
. . . . . . . . . 10
⊢ ((𝐻:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ V) → 𝐻 ∈ V) |
77 | 11, 6, 73, 76 | syl3anc 1318 |
. . . . . . . . 9
⊢ (𝜑 → 𝐻 ∈ V) |
78 | | offres 7054 |
. . . . . . . . 9
⊢ ((𝐹 ∈ V ∧ 𝐻 ∈ V) → ((𝐹 ∘𝑓
+ 𝐻) ↾ 𝑧) = ((𝐹 ↾ 𝑧) ∘𝑓 + (𝐻 ↾ 𝑧))) |
79 | 75, 77, 78 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 → ((𝐹 ∘𝑓 + 𝐻) ↾ 𝑧) = ((𝐹 ↾ 𝑧) ∘𝑓 + (𝐻 ↾ 𝑧))) |
80 | 79 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → ((𝐹 ∘𝑓 + 𝐻) ↾ 𝑧) = ((𝐹 ↾ 𝑧) ∘𝑓 + (𝐻 ↾ 𝑧))) |
81 | 80 | oveq2d 6565 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐺 Σg ((𝐹 ∘𝑓
+ 𝐻) ↾ 𝑧)) = (𝐺 Σg ((𝐹 ↾ 𝑧) ∘𝑓 + (𝐻 ↾ 𝑧)))) |
82 | 1, 15, 16 | plusfval 17071 |
. . . . . . 7
⊢ (((𝐺 Σg
(𝐹 ↾ 𝑧)) ∈ 𝐵 ∧ (𝐺 Σg (𝐻 ↾ 𝑧)) ∈ 𝐵) → ((𝐺 Σg (𝐹 ↾ 𝑧))(+𝑓‘𝐺)(𝐺 Σg (𝐻 ↾ 𝑧))) = ((𝐺 Σg (𝐹 ↾ 𝑧)) + (𝐺 Σg (𝐻 ↾ 𝑧)))) |
83 | 28, 29, 82 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → ((𝐺 Σg (𝐹 ↾ 𝑧))(+𝑓‘𝐺)(𝐺 Σg (𝐻 ↾ 𝑧))) = ((𝐺 Σg (𝐹 ↾ 𝑧)) + (𝐺 Σg (𝐻 ↾ 𝑧)))) |
84 | 70, 81, 83 | 3eqtr4d 2654 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐺 Σg ((𝐹 ∘𝑓
+ 𝐻) ↾ 𝑧)) = ((𝐺 Σg (𝐹 ↾ 𝑧))(+𝑓‘𝐺)(𝐺 Σg (𝐻 ↾ 𝑧)))) |
85 | 84 | mpteq2dva 4672 |
. . . 4
⊢ (𝜑 → (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg ((𝐹 ∘𝑓
+ 𝐻) ↾ 𝑧))) = (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((𝐺 Σg (𝐹 ↾ 𝑧))(+𝑓‘𝐺)(𝐺 Σg (𝐻 ↾ 𝑧))))) |
86 | 85 | fveq2d 6107 |
. . 3
⊢ (𝜑 → (((TopOpen‘𝐺) fLimf ((𝒫 𝐴 ∩ Fin)filGenran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦 ⊆ 𝑧})))‘(𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg ((𝐹 ∘𝑓
+ 𝐻) ↾ 𝑧)))) = (((TopOpen‘𝐺) fLimf ((𝒫 𝐴 ∩ Fin)filGenran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦 ⊆ 𝑧})))‘(𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((𝐺 Σg (𝐹 ↾ 𝑧))(+𝑓‘𝐺)(𝐺 Σg (𝐻 ↾ 𝑧)))))) |
87 | 55, 86 | eqtrd 2644 |
. 2
⊢ (𝜑 → (𝐺 tsums (𝐹 ∘𝑓 + 𝐻)) = (((TopOpen‘𝐺) fLimf ((𝒫 𝐴 ∩ Fin)filGenran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ {𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∣ 𝑦 ⊆ 𝑧})))‘(𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((𝐺 Σg (𝐹 ↾ 𝑧))(+𝑓‘𝐺)(𝐺 Σg (𝐻 ↾ 𝑧)))))) |
88 | 47, 87 | eleqtrrd 2691 |
1
⊢ (𝜑 → (𝑋 + 𝑌) ∈ (𝐺 tsums (𝐹 ∘𝑓 + 𝐻))) |