Step |
Hyp |
Ref |
Expression |
1 |
|
subgtgp.h |
⊢ 𝐻 = ( 𝐺 ↾s 𝑆 ) |
2 |
1
|
submmnd |
⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) → 𝐻 ∈ Mnd ) |
3 |
2
|
adantl |
⊢ ( ( 𝐺 ∈ TopMnd ∧ 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ) → 𝐻 ∈ Mnd ) |
4 |
|
tmdtps |
⊢ ( 𝐺 ∈ TopMnd → 𝐺 ∈ TopSp ) |
5 |
|
resstps |
⊢ ( ( 𝐺 ∈ TopSp ∧ 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ) → ( 𝐺 ↾s 𝑆 ) ∈ TopSp ) |
6 |
4 5
|
sylan |
⊢ ( ( 𝐺 ∈ TopMnd ∧ 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ) → ( 𝐺 ↾s 𝑆 ) ∈ TopSp ) |
7 |
1 6
|
eqeltrid |
⊢ ( ( 𝐺 ∈ TopMnd ∧ 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ) → 𝐻 ∈ TopSp ) |
8 |
|
eqid |
⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 ) |
9 |
|
eqid |
⊢ ( +g ‘ 𝐻 ) = ( +g ‘ 𝐻 ) |
10 |
|
eqid |
⊢ ( +𝑓 ‘ 𝐻 ) = ( +𝑓 ‘ 𝐻 ) |
11 |
8 9 10
|
plusffval |
⊢ ( +𝑓 ‘ 𝐻 ) = ( 𝑥 ∈ ( Base ‘ 𝐻 ) , 𝑦 ∈ ( Base ‘ 𝐻 ) ↦ ( 𝑥 ( +g ‘ 𝐻 ) 𝑦 ) ) |
12 |
1
|
submbas |
⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) → 𝑆 = ( Base ‘ 𝐻 ) ) |
13 |
12
|
adantl |
⊢ ( ( 𝐺 ∈ TopMnd ∧ 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ) → 𝑆 = ( Base ‘ 𝐻 ) ) |
14 |
|
eqid |
⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 ) |
15 |
1 14
|
ressplusg |
⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) → ( +g ‘ 𝐺 ) = ( +g ‘ 𝐻 ) ) |
16 |
15
|
adantl |
⊢ ( ( 𝐺 ∈ TopMnd ∧ 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ) → ( +g ‘ 𝐺 ) = ( +g ‘ 𝐻 ) ) |
17 |
16
|
oveqd |
⊢ ( ( 𝐺 ∈ TopMnd ∧ 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐻 ) 𝑦 ) ) |
18 |
13 13 17
|
mpoeq123dv |
⊢ ( ( 𝐺 ∈ TopMnd ∧ 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ) → ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) = ( 𝑥 ∈ ( Base ‘ 𝐻 ) , 𝑦 ∈ ( Base ‘ 𝐻 ) ↦ ( 𝑥 ( +g ‘ 𝐻 ) 𝑦 ) ) ) |
19 |
11 18
|
eqtr4id |
⊢ ( ( 𝐺 ∈ TopMnd ∧ 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ) → ( +𝑓 ‘ 𝐻 ) = ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) ) |
20 |
|
eqid |
⊢ ( ( TopOpen ‘ 𝐺 ) ↾t 𝑆 ) = ( ( TopOpen ‘ 𝐺 ) ↾t 𝑆 ) |
21 |
|
eqid |
⊢ ( TopOpen ‘ 𝐺 ) = ( TopOpen ‘ 𝐺 ) |
22 |
|
eqid |
⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 ) |
23 |
21 22
|
tmdtopon |
⊢ ( 𝐺 ∈ TopMnd → ( TopOpen ‘ 𝐺 ) ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) ) |
24 |
23
|
adantr |
⊢ ( ( 𝐺 ∈ TopMnd ∧ 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ) → ( TopOpen ‘ 𝐺 ) ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) ) |
25 |
22
|
submss |
⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) ) |
26 |
25
|
adantl |
⊢ ( ( 𝐺 ∈ TopMnd ∧ 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) ) |
27 |
|
eqid |
⊢ ( +𝑓 ‘ 𝐺 ) = ( +𝑓 ‘ 𝐺 ) |
28 |
22 14 27
|
plusffval |
⊢ ( +𝑓 ‘ 𝐺 ) = ( 𝑥 ∈ ( Base ‘ 𝐺 ) , 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) |
29 |
21 27
|
tmdcn |
⊢ ( 𝐺 ∈ TopMnd → ( +𝑓 ‘ 𝐺 ) ∈ ( ( ( TopOpen ‘ 𝐺 ) ×t ( TopOpen ‘ 𝐺 ) ) Cn ( TopOpen ‘ 𝐺 ) ) ) |
30 |
28 29
|
eqeltrrid |
⊢ ( 𝐺 ∈ TopMnd → ( 𝑥 ∈ ( Base ‘ 𝐺 ) , 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) ∈ ( ( ( TopOpen ‘ 𝐺 ) ×t ( TopOpen ‘ 𝐺 ) ) Cn ( TopOpen ‘ 𝐺 ) ) ) |
31 |
30
|
adantr |
⊢ ( ( 𝐺 ∈ TopMnd ∧ 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ) → ( 𝑥 ∈ ( Base ‘ 𝐺 ) , 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) ∈ ( ( ( TopOpen ‘ 𝐺 ) ×t ( TopOpen ‘ 𝐺 ) ) Cn ( TopOpen ‘ 𝐺 ) ) ) |
32 |
20 24 26 20 24 26 31
|
cnmpt2res |
⊢ ( ( 𝐺 ∈ TopMnd ∧ 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ) → ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) ∈ ( ( ( ( TopOpen ‘ 𝐺 ) ↾t 𝑆 ) ×t ( ( TopOpen ‘ 𝐺 ) ↾t 𝑆 ) ) Cn ( TopOpen ‘ 𝐺 ) ) ) |
33 |
19 32
|
eqeltrd |
⊢ ( ( 𝐺 ∈ TopMnd ∧ 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ) → ( +𝑓 ‘ 𝐻 ) ∈ ( ( ( ( TopOpen ‘ 𝐺 ) ↾t 𝑆 ) ×t ( ( TopOpen ‘ 𝐺 ) ↾t 𝑆 ) ) Cn ( TopOpen ‘ 𝐺 ) ) ) |
34 |
8 10
|
mndplusf |
⊢ ( 𝐻 ∈ Mnd → ( +𝑓 ‘ 𝐻 ) : ( ( Base ‘ 𝐻 ) × ( Base ‘ 𝐻 ) ) ⟶ ( Base ‘ 𝐻 ) ) |
35 |
|
frn |
⊢ ( ( +𝑓 ‘ 𝐻 ) : ( ( Base ‘ 𝐻 ) × ( Base ‘ 𝐻 ) ) ⟶ ( Base ‘ 𝐻 ) → ran ( +𝑓 ‘ 𝐻 ) ⊆ ( Base ‘ 𝐻 ) ) |
36 |
3 34 35
|
3syl |
⊢ ( ( 𝐺 ∈ TopMnd ∧ 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ) → ran ( +𝑓 ‘ 𝐻 ) ⊆ ( Base ‘ 𝐻 ) ) |
37 |
36 13
|
sseqtrrd |
⊢ ( ( 𝐺 ∈ TopMnd ∧ 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ) → ran ( +𝑓 ‘ 𝐻 ) ⊆ 𝑆 ) |
38 |
|
cnrest2 |
⊢ ( ( ( 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 |
⊢ ( ( 𝐺 ∈ TopMnd ∧ 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ) → ( ( +𝑓 ‘ 𝐻 ) ∈ ( ( ( ( TopOpen ‘ 𝐺 ) ↾t 𝑆 ) ×t ( ( TopOpen ‘ 𝐺 ) ↾t 𝑆 ) ) Cn ( TopOpen ‘ 𝐺 ) ) ↔ ( +𝑓 ‘ 𝐻 ) ∈ ( ( ( ( TopOpen ‘ 𝐺 ) ↾t 𝑆 ) ×t ( ( TopOpen ‘ 𝐺 ) ↾t 𝑆 ) ) Cn ( ( TopOpen ‘ 𝐺 ) ↾t 𝑆 ) ) ) ) |
40 |
33 39
|
mpbid |
⊢ ( ( 𝐺 ∈ TopMnd ∧ 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ) → ( +𝑓 ‘ 𝐻 ) ∈ ( ( ( ( TopOpen ‘ 𝐺 ) ↾t 𝑆 ) ×t ( ( TopOpen ‘ 𝐺 ) ↾t 𝑆 ) ) Cn ( ( TopOpen ‘ 𝐺 ) ↾t 𝑆 ) ) ) |
41 |
1 21
|
resstopn |
⊢ ( ( TopOpen ‘ 𝐺 ) ↾t 𝑆 ) = ( TopOpen ‘ 𝐻 ) |
42 |
10 41
|
istmd |
⊢ ( 𝐻 ∈ TopMnd ↔ ( 𝐻 ∈ Mnd ∧ 𝐻 ∈ TopSp ∧ ( +𝑓 ‘ 𝐻 ) ∈ ( ( ( ( TopOpen ‘ 𝐺 ) ↾t 𝑆 ) ×t ( ( TopOpen ‘ 𝐺 ) ↾t 𝑆 ) ) Cn ( ( TopOpen ‘ 𝐺 ) ↾t 𝑆 ) ) ) ) |
43 |
3 7 40 42
|
syl3anbrc |
⊢ ( ( 𝐺 ∈ TopMnd ∧ 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ) → 𝐻 ∈ TopMnd ) |