| Step |
Hyp |
Ref |
Expression |
| 1 |
|
tngbas.t |
|- T = ( G toNrmGrp N ) |
| 2 |
|
tnglem.e |
|- E = Slot ( E ` ndx ) |
| 3 |
|
tnglem.t |
|- ( E ` ndx ) =/= ( TopSet ` ndx ) |
| 4 |
|
tnglem.d |
|- ( E ` ndx ) =/= ( dist ` ndx ) |
| 5 |
2 4
|
setsnid |
|- ( E ` G ) = ( E ` ( G sSet <. ( dist ` ndx ) , ( N o. ( -g ` G ) ) >. ) ) |
| 6 |
2 3
|
setsnid |
|- ( E ` ( G sSet <. ( dist ` ndx ) , ( N o. ( -g ` G ) ) >. ) ) = ( E ` ( ( G sSet <. ( dist ` ndx ) , ( N o. ( -g ` G ) ) >. ) sSet <. ( TopSet ` ndx ) , ( MetOpen ` ( N o. ( -g ` G ) ) ) >. ) ) |
| 7 |
5 6
|
eqtri |
|- ( E ` G ) = ( E ` ( ( G sSet <. ( dist ` ndx ) , ( N o. ( -g ` G ) ) >. ) sSet <. ( TopSet ` ndx ) , ( MetOpen ` ( N o. ( -g ` G ) ) ) >. ) ) |
| 8 |
|
eqid |
|- ( -g ` G ) = ( -g ` G ) |
| 9 |
|
eqid |
|- ( N o. ( -g ` G ) ) = ( N o. ( -g ` G ) ) |
| 10 |
|
eqid |
|- ( MetOpen ` ( N o. ( -g ` G ) ) ) = ( MetOpen ` ( N o. ( -g ` G ) ) ) |
| 11 |
1 8 9 10
|
tngval |
|- ( ( G e. _V /\ N e. V ) -> T = ( ( G sSet <. ( dist ` ndx ) , ( N o. ( -g ` G ) ) >. ) sSet <. ( TopSet ` ndx ) , ( MetOpen ` ( N o. ( -g ` G ) ) ) >. ) ) |
| 12 |
11
|
fveq2d |
|- ( ( G e. _V /\ N e. V ) -> ( E ` T ) = ( E ` ( ( G sSet <. ( dist ` ndx ) , ( N o. ( -g ` G ) ) >. ) sSet <. ( TopSet ` ndx ) , ( MetOpen ` ( N o. ( -g ` G ) ) ) >. ) ) ) |
| 13 |
7 12
|
eqtr4id |
|- ( ( G e. _V /\ N e. V ) -> ( E ` G ) = ( E ` T ) ) |
| 14 |
2
|
str0 |
|- (/) = ( E ` (/) ) |
| 15 |
14
|
eqcomi |
|- ( E ` (/) ) = (/) |
| 16 |
|
reldmtng |
|- Rel dom toNrmGrp |
| 17 |
15 1 16
|
oveqprc |
|- ( -. G e. _V -> ( E ` G ) = ( E ` T ) ) |
| 18 |
17
|
adantr |
|- ( ( -. G e. _V /\ N e. V ) -> ( E ` G ) = ( E ` T ) ) |
| 19 |
13 18
|
pm2.61ian |
|- ( N e. V -> ( E ` G ) = ( E ` T ) ) |