Step |
Hyp |
Ref |
Expression |
1 |
|
tngbas.t |
|- T = ( G toNrmGrp N ) |
2 |
|
tngds.2 |
|- .- = ( -g ` G ) |
3 |
|
dsid |
|- dist = Slot ( dist ` ndx ) |
4 |
|
dsndxntsetndx |
|- ( dist ` ndx ) =/= ( TopSet ` ndx ) |
5 |
3 4
|
setsnid |
|- ( dist ` ( G sSet <. ( dist ` ndx ) , ( N o. .- ) >. ) ) = ( dist ` ( ( G sSet <. ( dist ` ndx ) , ( N o. .- ) >. ) sSet <. ( TopSet ` ndx ) , ( MetOpen ` ( N o. .- ) ) >. ) ) |
6 |
2
|
fvexi |
|- .- e. _V |
7 |
|
coexg |
|- ( ( N e. V /\ .- e. _V ) -> ( N o. .- ) e. _V ) |
8 |
6 7
|
mpan2 |
|- ( N e. V -> ( N o. .- ) e. _V ) |
9 |
3
|
setsid |
|- ( ( G e. _V /\ ( N o. .- ) e. _V ) -> ( N o. .- ) = ( dist ` ( G sSet <. ( dist ` ndx ) , ( N o. .- ) >. ) ) ) |
10 |
8 9
|
sylan2 |
|- ( ( G e. _V /\ N e. V ) -> ( N o. .- ) = ( dist ` ( G sSet <. ( dist ` ndx ) , ( N o. .- ) >. ) ) ) |
11 |
|
eqid |
|- ( N o. .- ) = ( N o. .- ) |
12 |
|
eqid |
|- ( MetOpen ` ( N o. .- ) ) = ( MetOpen ` ( N o. .- ) ) |
13 |
1 2 11 12
|
tngval |
|- ( ( G e. _V /\ N e. V ) -> T = ( ( G sSet <. ( dist ` ndx ) , ( N o. .- ) >. ) sSet <. ( TopSet ` ndx ) , ( MetOpen ` ( N o. .- ) ) >. ) ) |
14 |
13
|
fveq2d |
|- ( ( G e. _V /\ N e. V ) -> ( dist ` T ) = ( dist ` ( ( G sSet <. ( dist ` ndx ) , ( N o. .- ) >. ) sSet <. ( TopSet ` ndx ) , ( MetOpen ` ( N o. .- ) ) >. ) ) ) |
15 |
5 10 14
|
3eqtr4a |
|- ( ( G e. _V /\ N e. V ) -> ( N o. .- ) = ( dist ` T ) ) |
16 |
|
co02 |
|- ( N o. (/) ) = (/) |
17 |
3
|
str0 |
|- (/) = ( dist ` (/) ) |
18 |
16 17
|
eqtri |
|- ( N o. (/) ) = ( dist ` (/) ) |
19 |
|
fvprc |
|- ( -. G e. _V -> ( -g ` G ) = (/) ) |
20 |
2 19
|
eqtrid |
|- ( -. G e. _V -> .- = (/) ) |
21 |
20
|
coeq2d |
|- ( -. G e. _V -> ( N o. .- ) = ( N o. (/) ) ) |
22 |
|
reldmtng |
|- Rel dom toNrmGrp |
23 |
22
|
ovprc1 |
|- ( -. G e. _V -> ( G toNrmGrp N ) = (/) ) |
24 |
1 23
|
eqtrid |
|- ( -. G e. _V -> T = (/) ) |
25 |
24
|
fveq2d |
|- ( -. G e. _V -> ( dist ` T ) = ( dist ` (/) ) ) |
26 |
18 21 25
|
3eqtr4a |
|- ( -. G e. _V -> ( N o. .- ) = ( dist ` T ) ) |
27 |
26
|
adantr |
|- ( ( -. G e. _V /\ N e. V ) -> ( N o. .- ) = ( dist ` T ) ) |
28 |
15 27
|
pm2.61ian |
|- ( N e. V -> ( N o. .- ) = ( dist ` T ) ) |