Step |
Hyp |
Ref |
Expression |
1 |
|
tngbas.t |
|- T = ( G toNrmGrp N ) |
2 |
|
tngtset.2 |
|- D = ( dist ` T ) |
3 |
|
tngtset.3 |
|- J = ( MetOpen ` D ) |
4 |
|
ovex |
|- ( G sSet <. ( dist ` ndx ) , ( N o. ( -g ` G ) ) >. ) e. _V |
5 |
|
fvex |
|- ( MetOpen ` ( N o. ( -g ` G ) ) ) e. _V |
6 |
|
tsetid |
|- TopSet = Slot ( TopSet ` ndx ) |
7 |
6
|
setsid |
|- ( ( ( G sSet <. ( dist ` ndx ) , ( N o. ( -g ` G ) ) >. ) e. _V /\ ( MetOpen ` ( N o. ( -g ` G ) ) ) e. _V ) -> ( MetOpen ` ( N o. ( -g ` G ) ) ) = ( TopSet ` ( ( G sSet <. ( dist ` ndx ) , ( N o. ( -g ` G ) ) >. ) sSet <. ( TopSet ` ndx ) , ( MetOpen ` ( N o. ( -g ` G ) ) ) >. ) ) ) |
8 |
4 5 7
|
mp2an |
|- ( MetOpen ` ( N o. ( -g ` G ) ) ) = ( TopSet ` ( ( G sSet <. ( dist ` ndx ) , ( N o. ( -g ` G ) ) >. ) sSet <. ( TopSet ` ndx ) , ( MetOpen ` ( N o. ( -g ` G ) ) ) >. ) ) |
9 |
|
eqid |
|- ( -g ` G ) = ( -g ` G ) |
10 |
1 9
|
tngds |
|- ( N e. W -> ( N o. ( -g ` G ) ) = ( dist ` T ) ) |
11 |
2 10
|
eqtr4id |
|- ( N e. W -> D = ( N o. ( -g ` G ) ) ) |
12 |
11
|
adantl |
|- ( ( G e. V /\ N e. W ) -> D = ( N o. ( -g ` G ) ) ) |
13 |
12
|
fveq2d |
|- ( ( G e. V /\ N e. W ) -> ( MetOpen ` D ) = ( MetOpen ` ( N o. ( -g ` G ) ) ) ) |
14 |
3 13
|
syl5eq |
|- ( ( G e. V /\ N e. W ) -> J = ( MetOpen ` ( N o. ( -g ` G ) ) ) ) |
15 |
|
eqid |
|- ( N o. ( -g ` G ) ) = ( N o. ( -g ` G ) ) |
16 |
|
eqid |
|- ( MetOpen ` ( N o. ( -g ` G ) ) ) = ( MetOpen ` ( N o. ( -g ` G ) ) ) |
17 |
1 9 15 16
|
tngval |
|- ( ( G e. V /\ N e. W ) -> T = ( ( G sSet <. ( dist ` ndx ) , ( N o. ( -g ` G ) ) >. ) sSet <. ( TopSet ` ndx ) , ( MetOpen ` ( N o. ( -g ` G ) ) ) >. ) ) |
18 |
17
|
fveq2d |
|- ( ( G e. V /\ N e. W ) -> ( TopSet ` T ) = ( TopSet ` ( ( G sSet <. ( dist ` ndx ) , ( N o. ( -g ` G ) ) >. ) sSet <. ( TopSet ` ndx ) , ( MetOpen ` ( N o. ( -g ` G ) ) ) >. ) ) ) |
19 |
8 14 18
|
3eqtr4a |
|- ( ( G e. V /\ N e. W ) -> J = ( TopSet ` T ) ) |