| Step |
Hyp |
Ref |
Expression |
| 1 |
|
tngbas.t |
⊢ 𝑇 = ( 𝐺 toNrmGrp 𝑁 ) |
| 2 |
|
tngds.2 |
⊢ − = ( -g ‘ 𝐺 ) |
| 3 |
|
dsid |
⊢ dist = Slot ( dist ‘ ndx ) |
| 4 |
|
dsndxntsetndx |
⊢ ( dist ‘ ndx ) ≠ ( TopSet ‘ ndx ) |
| 5 |
3 4
|
setsnid |
⊢ ( dist ‘ ( 𝐺 sSet ⟨ ( dist ‘ ndx ) , ( 𝑁 ∘ − ) ⟩ ) ) = ( dist ‘ ( ( 𝐺 sSet ⟨ ( dist ‘ ndx ) , ( 𝑁 ∘ − ) ⟩ ) sSet ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( 𝑁 ∘ − ) ) ⟩ ) ) |
| 6 |
2
|
fvexi |
⊢ − ∈ V |
| 7 |
|
coexg |
⊢ ( ( 𝑁 ∈ 𝑉 ∧ − ∈ V ) → ( 𝑁 ∘ − ) ∈ V ) |
| 8 |
6 7
|
mpan2 |
⊢ ( 𝑁 ∈ 𝑉 → ( 𝑁 ∘ − ) ∈ V ) |
| 9 |
3
|
setsid |
⊢ ( ( 𝐺 ∈ V ∧ ( 𝑁 ∘ − ) ∈ V ) → ( 𝑁 ∘ − ) = ( dist ‘ ( 𝐺 sSet ⟨ ( dist ‘ ndx ) , ( 𝑁 ∘ − ) ⟩ ) ) ) |
| 10 |
8 9
|
sylan2 |
⊢ ( ( 𝐺 ∈ V ∧ 𝑁 ∈ 𝑉 ) → ( 𝑁 ∘ − ) = ( dist ‘ ( 𝐺 sSet ⟨ ( dist ‘ ndx ) , ( 𝑁 ∘ − ) ⟩ ) ) ) |
| 11 |
|
eqid |
⊢ ( 𝑁 ∘ − ) = ( 𝑁 ∘ − ) |
| 12 |
|
eqid |
⊢ ( MetOpen ‘ ( 𝑁 ∘ − ) ) = ( MetOpen ‘ ( 𝑁 ∘ − ) ) |
| 13 |
1 2 11 12
|
tngval |
⊢ ( ( 𝐺 ∈ V ∧ 𝑁 ∈ 𝑉 ) → 𝑇 = ( ( 𝐺 sSet ⟨ ( dist ‘ ndx ) , ( 𝑁 ∘ − ) ⟩ ) sSet ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( 𝑁 ∘ − ) ) ⟩ ) ) |
| 14 |
13
|
fveq2d |
⊢ ( ( 𝐺 ∈ V ∧ 𝑁 ∈ 𝑉 ) → ( dist ‘ 𝑇 ) = ( dist ‘ ( ( 𝐺 sSet ⟨ ( dist ‘ ndx ) , ( 𝑁 ∘ − ) ⟩ ) sSet ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( 𝑁 ∘ − ) ) ⟩ ) ) ) |
| 15 |
5 10 14
|
3eqtr4a |
⊢ ( ( 𝐺 ∈ V ∧ 𝑁 ∈ 𝑉 ) → ( 𝑁 ∘ − ) = ( dist ‘ 𝑇 ) ) |
| 16 |
|
co02 |
⊢ ( 𝑁 ∘ ∅ ) = ∅ |
| 17 |
3
|
str0 |
⊢ ∅ = ( dist ‘ ∅ ) |
| 18 |
16 17
|
eqtri |
⊢ ( 𝑁 ∘ ∅ ) = ( dist ‘ ∅ ) |
| 19 |
|
fvprc |
⊢ ( ¬ 𝐺 ∈ V → ( -g ‘ 𝐺 ) = ∅ ) |
| 20 |
2 19
|
syl5eq |
⊢ ( ¬ 𝐺 ∈ V → − = ∅ ) |
| 21 |
20
|
coeq2d |
⊢ ( ¬ 𝐺 ∈ V → ( 𝑁 ∘ − ) = ( 𝑁 ∘ ∅ ) ) |
| 22 |
|
reldmtng |
⊢ Rel dom toNrmGrp |
| 23 |
22
|
ovprc1 |
⊢ ( ¬ 𝐺 ∈ V → ( 𝐺 toNrmGrp 𝑁 ) = ∅ ) |
| 24 |
1 23
|
syl5eq |
⊢ ( ¬ 𝐺 ∈ V → 𝑇 = ∅ ) |
| 25 |
24
|
fveq2d |
⊢ ( ¬ 𝐺 ∈ V → ( dist ‘ 𝑇 ) = ( dist ‘ ∅ ) ) |
| 26 |
18 21 25
|
3eqtr4a |
⊢ ( ¬ 𝐺 ∈ V → ( 𝑁 ∘ − ) = ( dist ‘ 𝑇 ) ) |
| 27 |
26
|
adantr |
⊢ ( ( ¬ 𝐺 ∈ V ∧ 𝑁 ∈ 𝑉 ) → ( 𝑁 ∘ − ) = ( dist ‘ 𝑇 ) ) |
| 28 |
15 27
|
pm2.61ian |
⊢ ( 𝑁 ∈ 𝑉 → ( 𝑁 ∘ − ) = ( dist ‘ 𝑇 ) ) |