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