Step |
Hyp |
Ref |
Expression |
1 |
|
tngval.t |
⊢ 𝑇 = ( 𝐺 toNrmGrp 𝑁 ) |
2 |
|
tngval.m |
⊢ − = ( -g ‘ 𝐺 ) |
3 |
|
tngval.d |
⊢ 𝐷 = ( 𝑁 ∘ − ) |
4 |
|
tngval.j |
⊢ 𝐽 = ( MetOpen ‘ 𝐷 ) |
5 |
|
elex |
⊢ ( 𝐺 ∈ 𝑉 → 𝐺 ∈ V ) |
6 |
|
elex |
⊢ ( 𝑁 ∈ 𝑊 → 𝑁 ∈ V ) |
7 |
|
simpl |
⊢ ( ( 𝑔 = 𝐺 ∧ 𝑓 = 𝑁 ) → 𝑔 = 𝐺 ) |
8 |
|
simpr |
⊢ ( ( 𝑔 = 𝐺 ∧ 𝑓 = 𝑁 ) → 𝑓 = 𝑁 ) |
9 |
7
|
fveq2d |
⊢ ( ( 𝑔 = 𝐺 ∧ 𝑓 = 𝑁 ) → ( -g ‘ 𝑔 ) = ( -g ‘ 𝐺 ) ) |
10 |
9 2
|
eqtr4di |
⊢ ( ( 𝑔 = 𝐺 ∧ 𝑓 = 𝑁 ) → ( -g ‘ 𝑔 ) = − ) |
11 |
8 10
|
coeq12d |
⊢ ( ( 𝑔 = 𝐺 ∧ 𝑓 = 𝑁 ) → ( 𝑓 ∘ ( -g ‘ 𝑔 ) ) = ( 𝑁 ∘ − ) ) |
12 |
11 3
|
eqtr4di |
⊢ ( ( 𝑔 = 𝐺 ∧ 𝑓 = 𝑁 ) → ( 𝑓 ∘ ( -g ‘ 𝑔 ) ) = 𝐷 ) |
13 |
12
|
opeq2d |
⊢ ( ( 𝑔 = 𝐺 ∧ 𝑓 = 𝑁 ) → 〈 ( dist ‘ ndx ) , ( 𝑓 ∘ ( -g ‘ 𝑔 ) ) 〉 = 〈 ( dist ‘ ndx ) , 𝐷 〉 ) |
14 |
7 13
|
oveq12d |
⊢ ( ( 𝑔 = 𝐺 ∧ 𝑓 = 𝑁 ) → ( 𝑔 sSet 〈 ( dist ‘ ndx ) , ( 𝑓 ∘ ( -g ‘ 𝑔 ) ) 〉 ) = ( 𝐺 sSet 〈 ( dist ‘ ndx ) , 𝐷 〉 ) ) |
15 |
12
|
fveq2d |
⊢ ( ( 𝑔 = 𝐺 ∧ 𝑓 = 𝑁 ) → ( MetOpen ‘ ( 𝑓 ∘ ( -g ‘ 𝑔 ) ) ) = ( MetOpen ‘ 𝐷 ) ) |
16 |
15 4
|
eqtr4di |
⊢ ( ( 𝑔 = 𝐺 ∧ 𝑓 = 𝑁 ) → ( MetOpen ‘ ( 𝑓 ∘ ( -g ‘ 𝑔 ) ) ) = 𝐽 ) |
17 |
16
|
opeq2d |
⊢ ( ( 𝑔 = 𝐺 ∧ 𝑓 = 𝑁 ) → 〈 ( TopSet ‘ ndx ) , ( MetOpen ‘ ( 𝑓 ∘ ( -g ‘ 𝑔 ) ) ) 〉 = 〈 ( TopSet ‘ ndx ) , 𝐽 〉 ) |
18 |
14 17
|
oveq12d |
⊢ ( ( 𝑔 = 𝐺 ∧ 𝑓 = 𝑁 ) → ( ( 𝑔 sSet 〈 ( dist ‘ ndx ) , ( 𝑓 ∘ ( -g ‘ 𝑔 ) ) 〉 ) sSet 〈 ( TopSet ‘ ndx ) , ( MetOpen ‘ ( 𝑓 ∘ ( -g ‘ 𝑔 ) ) ) 〉 ) = ( ( 𝐺 sSet 〈 ( dist ‘ ndx ) , 𝐷 〉 ) sSet 〈 ( TopSet ‘ ndx ) , 𝐽 〉 ) ) |
19 |
|
df-tng |
⊢ toNrmGrp = ( 𝑔 ∈ V , 𝑓 ∈ V ↦ ( ( 𝑔 sSet 〈 ( dist ‘ ndx ) , ( 𝑓 ∘ ( -g ‘ 𝑔 ) ) 〉 ) sSet 〈 ( TopSet ‘ ndx ) , ( MetOpen ‘ ( 𝑓 ∘ ( -g ‘ 𝑔 ) ) ) 〉 ) ) |
20 |
|
ovex |
⊢ ( ( 𝐺 sSet 〈 ( dist ‘ ndx ) , 𝐷 〉 ) sSet 〈 ( TopSet ‘ ndx ) , 𝐽 〉 ) ∈ V |
21 |
18 19 20
|
ovmpoa |
⊢ ( ( 𝐺 ∈ V ∧ 𝑁 ∈ V ) → ( 𝐺 toNrmGrp 𝑁 ) = ( ( 𝐺 sSet 〈 ( dist ‘ ndx ) , 𝐷 〉 ) sSet 〈 ( TopSet ‘ ndx ) , 𝐽 〉 ) ) |
22 |
5 6 21
|
syl2an |
⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ) → ( 𝐺 toNrmGrp 𝑁 ) = ( ( 𝐺 sSet 〈 ( dist ‘ ndx ) , 𝐷 〉 ) sSet 〈 ( TopSet ‘ ndx ) , 𝐽 〉 ) ) |
23 |
1 22
|
syl5eq |
⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ) → 𝑇 = ( ( 𝐺 sSet 〈 ( dist ‘ ndx ) , 𝐷 〉 ) sSet 〈 ( TopSet ‘ ndx ) , 𝐽 〉 ) ) |