| Step | Hyp | Ref
| Expression |
| 1 | | subgtgp.h |
. . . 4
⊢ 𝐻 = (𝐺 ↾s 𝑆) |
| 2 | 1 | submmnd 18826 |
. . 3
⊢ (𝑆 ∈ (SubMnd‘𝐺) → 𝐻 ∈ Mnd) |
| 3 | 2 | adantl 481 |
. 2
⊢ ((𝐺 ∈ TopMnd ∧ 𝑆 ∈ (SubMnd‘𝐺)) → 𝐻 ∈ Mnd) |
| 4 | | tmdtps 24084 |
. . . 4
⊢ (𝐺 ∈ TopMnd → 𝐺 ∈ TopSp) |
| 5 | | resstps 23195 |
. . . 4
⊢ ((𝐺 ∈ TopSp ∧ 𝑆 ∈ (SubMnd‘𝐺)) → (𝐺 ↾s 𝑆) ∈ TopSp) |
| 6 | 4, 5 | sylan 580 |
. . 3
⊢ ((𝐺 ∈ TopMnd ∧ 𝑆 ∈ (SubMnd‘𝐺)) → (𝐺 ↾s 𝑆) ∈ TopSp) |
| 7 | 1, 6 | eqeltrid 2845 |
. 2
⊢ ((𝐺 ∈ TopMnd ∧ 𝑆 ∈ (SubMnd‘𝐺)) → 𝐻 ∈ TopSp) |
| 8 | | eqid 2737 |
. . . . . 6
⊢
(Base‘𝐻) =
(Base‘𝐻) |
| 9 | | eqid 2737 |
. . . . . 6
⊢
(+g‘𝐻) = (+g‘𝐻) |
| 10 | | eqid 2737 |
. . . . . 6
⊢
(+𝑓‘𝐻) = (+𝑓‘𝐻) |
| 11 | 8, 9, 10 | plusffval 18659 |
. . . . 5
⊢
(+𝑓‘𝐻) = (𝑥 ∈ (Base‘𝐻), 𝑦 ∈ (Base‘𝐻) ↦ (𝑥(+g‘𝐻)𝑦)) |
| 12 | 1 | submbas 18827 |
. . . . . . 7
⊢ (𝑆 ∈ (SubMnd‘𝐺) → 𝑆 = (Base‘𝐻)) |
| 13 | 12 | adantl 481 |
. . . . . 6
⊢ ((𝐺 ∈ TopMnd ∧ 𝑆 ∈ (SubMnd‘𝐺)) → 𝑆 = (Base‘𝐻)) |
| 14 | | eqid 2737 |
. . . . . . . . 9
⊢
(+g‘𝐺) = (+g‘𝐺) |
| 15 | 1, 14 | ressplusg 17334 |
. . . . . . . 8
⊢ (𝑆 ∈ (SubMnd‘𝐺) →
(+g‘𝐺) =
(+g‘𝐻)) |
| 16 | 15 | adantl 481 |
. . . . . . 7
⊢ ((𝐺 ∈ TopMnd ∧ 𝑆 ∈ (SubMnd‘𝐺)) →
(+g‘𝐺) =
(+g‘𝐻)) |
| 17 | 16 | oveqd 7448 |
. . . . . 6
⊢ ((𝐺 ∈ TopMnd ∧ 𝑆 ∈ (SubMnd‘𝐺)) → (𝑥(+g‘𝐺)𝑦) = (𝑥(+g‘𝐻)𝑦)) |
| 18 | 13, 13, 17 | mpoeq123dv 7508 |
. . . . 5
⊢ ((𝐺 ∈ TopMnd ∧ 𝑆 ∈ (SubMnd‘𝐺)) → (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ (𝑥(+g‘𝐺)𝑦)) = (𝑥 ∈ (Base‘𝐻), 𝑦 ∈ (Base‘𝐻) ↦ (𝑥(+g‘𝐻)𝑦))) |
| 19 | 11, 18 | eqtr4id 2796 |
. . . 4
⊢ ((𝐺 ∈ TopMnd ∧ 𝑆 ∈ (SubMnd‘𝐺)) →
(+𝑓‘𝐻) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ (𝑥(+g‘𝐺)𝑦))) |
| 20 | | eqid 2737 |
. . . . 5
⊢
((TopOpen‘𝐺)
↾t 𝑆) =
((TopOpen‘𝐺)
↾t 𝑆) |
| 21 | | eqid 2737 |
. . . . . . 7
⊢
(TopOpen‘𝐺) =
(TopOpen‘𝐺) |
| 22 | | eqid 2737 |
. . . . . . 7
⊢
(Base‘𝐺) =
(Base‘𝐺) |
| 23 | 21, 22 | tmdtopon 24089 |
. . . . . 6
⊢ (𝐺 ∈ TopMnd →
(TopOpen‘𝐺) ∈
(TopOn‘(Base‘𝐺))) |
| 24 | 23 | adantr 480 |
. . . . 5
⊢ ((𝐺 ∈ TopMnd ∧ 𝑆 ∈ (SubMnd‘𝐺)) → (TopOpen‘𝐺) ∈
(TopOn‘(Base‘𝐺))) |
| 25 | 22 | submss 18822 |
. . . . . 6
⊢ (𝑆 ∈ (SubMnd‘𝐺) → 𝑆 ⊆ (Base‘𝐺)) |
| 26 | 25 | adantl 481 |
. . . . 5
⊢ ((𝐺 ∈ TopMnd ∧ 𝑆 ∈ (SubMnd‘𝐺)) → 𝑆 ⊆ (Base‘𝐺)) |
| 27 | | eqid 2737 |
. . . . . . . 8
⊢
(+𝑓‘𝐺) = (+𝑓‘𝐺) |
| 28 | 22, 14, 27 | plusffval 18659 |
. . . . . . 7
⊢
(+𝑓‘𝐺) = (𝑥 ∈ (Base‘𝐺), 𝑦 ∈ (Base‘𝐺) ↦ (𝑥(+g‘𝐺)𝑦)) |
| 29 | 21, 27 | tmdcn 24091 |
. . . . . . 7
⊢ (𝐺 ∈ TopMnd →
(+𝑓‘𝐺) ∈ (((TopOpen‘𝐺) ×t (TopOpen‘𝐺)) Cn (TopOpen‘𝐺))) |
| 30 | 28, 29 | eqeltrrid 2846 |
. . . . . 6
⊢ (𝐺 ∈ TopMnd → (𝑥 ∈ (Base‘𝐺), 𝑦 ∈ (Base‘𝐺) ↦ (𝑥(+g‘𝐺)𝑦)) ∈ (((TopOpen‘𝐺) ×t (TopOpen‘𝐺)) Cn (TopOpen‘𝐺))) |
| 31 | 30 | adantr 480 |
. . . . 5
⊢ ((𝐺 ∈ TopMnd ∧ 𝑆 ∈ (SubMnd‘𝐺)) → (𝑥 ∈ (Base‘𝐺), 𝑦 ∈ (Base‘𝐺) ↦ (𝑥(+g‘𝐺)𝑦)) ∈ (((TopOpen‘𝐺) ×t (TopOpen‘𝐺)) Cn (TopOpen‘𝐺))) |
| 32 | 20, 24, 26, 20, 24, 26, 31 | cnmpt2res 23685 |
. . . 4
⊢ ((𝐺 ∈ TopMnd ∧ 𝑆 ∈ (SubMnd‘𝐺)) → (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ (𝑥(+g‘𝐺)𝑦)) ∈ ((((TopOpen‘𝐺) ↾t 𝑆) ×t ((TopOpen‘𝐺) ↾t 𝑆)) Cn (TopOpen‘𝐺))) |
| 33 | 19, 32 | eqeltrd 2841 |
. . 3
⊢ ((𝐺 ∈ TopMnd ∧ 𝑆 ∈ (SubMnd‘𝐺)) →
(+𝑓‘𝐻) ∈ ((((TopOpen‘𝐺) ↾t 𝑆) ×t ((TopOpen‘𝐺) ↾t 𝑆)) Cn (TopOpen‘𝐺))) |
| 34 | 8, 10 | mndplusf 18765 |
. . . . . 6
⊢ (𝐻 ∈ Mnd →
(+𝑓‘𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻)) |
| 35 | | frn 6743 |
. . . . . 6
⊢
((+𝑓‘𝐻):((Base‘𝐻) × (Base‘𝐻))⟶(Base‘𝐻) → ran
(+𝑓‘𝐻) ⊆ (Base‘𝐻)) |
| 36 | 3, 34, 35 | 3syl 18 |
. . . . 5
⊢ ((𝐺 ∈ TopMnd ∧ 𝑆 ∈ (SubMnd‘𝐺)) → ran
(+𝑓‘𝐻) ⊆ (Base‘𝐻)) |
| 37 | 36, 13 | sseqtrrd 4021 |
. . . 4
⊢ ((𝐺 ∈ TopMnd ∧ 𝑆 ∈ (SubMnd‘𝐺)) → ran
(+𝑓‘𝐻) ⊆ 𝑆) |
| 38 | | cnrest2 23294 |
. . . 4
⊢
(((TopOpen‘𝐺)
∈ (TopOn‘(Base‘𝐺)) ∧ ran
(+𝑓‘𝐻) ⊆ 𝑆 ∧ 𝑆 ⊆ (Base‘𝐺)) →
((+𝑓‘𝐻) ∈ ((((TopOpen‘𝐺) ↾t 𝑆) ×t ((TopOpen‘𝐺) ↾t 𝑆)) Cn (TopOpen‘𝐺)) ↔
(+𝑓‘𝐻) ∈ ((((TopOpen‘𝐺) ↾t 𝑆) ×t ((TopOpen‘𝐺) ↾t 𝑆)) Cn ((TopOpen‘𝐺) ↾t 𝑆)))) |
| 39 | 24, 37, 26, 38 | syl3anc 1373 |
. . 3
⊢ ((𝐺 ∈ TopMnd ∧ 𝑆 ∈ (SubMnd‘𝐺)) →
((+𝑓‘𝐻) ∈ ((((TopOpen‘𝐺) ↾t 𝑆) ×t ((TopOpen‘𝐺) ↾t 𝑆)) Cn (TopOpen‘𝐺)) ↔
(+𝑓‘𝐻) ∈ ((((TopOpen‘𝐺) ↾t 𝑆) ×t ((TopOpen‘𝐺) ↾t 𝑆)) Cn ((TopOpen‘𝐺) ↾t 𝑆)))) |
| 40 | 33, 39 | mpbid 232 |
. 2
⊢ ((𝐺 ∈ TopMnd ∧ 𝑆 ∈ (SubMnd‘𝐺)) →
(+𝑓‘𝐻) ∈ ((((TopOpen‘𝐺) ↾t 𝑆) ×t ((TopOpen‘𝐺) ↾t 𝑆)) Cn ((TopOpen‘𝐺) ↾t 𝑆))) |
| 41 | 1, 21 | resstopn 23194 |
. . 3
⊢
((TopOpen‘𝐺)
↾t 𝑆) =
(TopOpen‘𝐻) |
| 42 | 10, 41 | istmd 24082 |
. 2
⊢ (𝐻 ∈ TopMnd ↔ (𝐻 ∈ Mnd ∧ 𝐻 ∈ TopSp ∧
(+𝑓‘𝐻) ∈ ((((TopOpen‘𝐺) ↾t 𝑆) ×t ((TopOpen‘𝐺) ↾t 𝑆)) Cn ((TopOpen‘𝐺) ↾t 𝑆)))) |
| 43 | 3, 7, 40, 42 | syl3anbrc 1344 |
1
⊢ ((𝐺 ∈ TopMnd ∧ 𝑆 ∈ (SubMnd‘𝐺)) → 𝐻 ∈ TopMnd) |