Step |
Hyp |
Ref |
Expression |
1 |
|
tngbas.t |
|- T = ( G toNrmGrp N ) |
2 |
|
tngds.2 |
|- .- = ( -g ` G ) |
3 |
|
dsid |
|- dist = Slot ( dist ` ndx ) |
4 |
|
9re |
|- 9 e. RR |
5 |
|
1nn |
|- 1 e. NN |
6 |
|
2nn0 |
|- 2 e. NN0 |
7 |
|
9nn0 |
|- 9 e. NN0 |
8 |
|
9lt10 |
|- 9 < ; 1 0 |
9 |
5 6 7 8
|
declti |
|- 9 < ; 1 2 |
10 |
4 9
|
gtneii |
|- ; 1 2 =/= 9 |
11 |
|
dsndx |
|- ( dist ` ndx ) = ; 1 2 |
12 |
|
tsetndx |
|- ( TopSet ` ndx ) = 9 |
13 |
11 12
|
neeq12i |
|- ( ( dist ` ndx ) =/= ( TopSet ` ndx ) <-> ; 1 2 =/= 9 ) |
14 |
10 13
|
mpbir |
|- ( dist ` ndx ) =/= ( TopSet ` ndx ) |
15 |
3 14
|
setsnid |
|- ( dist ` ( G sSet <. ( dist ` ndx ) , ( N o. .- ) >. ) ) = ( dist ` ( ( G sSet <. ( dist ` ndx ) , ( N o. .- ) >. ) sSet <. ( TopSet ` ndx ) , ( MetOpen ` ( N o. .- ) ) >. ) ) |
16 |
2
|
fvexi |
|- .- e. _V |
17 |
|
coexg |
|- ( ( N e. V /\ .- e. _V ) -> ( N o. .- ) e. _V ) |
18 |
16 17
|
mpan2 |
|- ( N e. V -> ( N o. .- ) e. _V ) |
19 |
3
|
setsid |
|- ( ( G e. _V /\ ( N o. .- ) e. _V ) -> ( N o. .- ) = ( dist ` ( G sSet <. ( dist ` ndx ) , ( N o. .- ) >. ) ) ) |
20 |
18 19
|
sylan2 |
|- ( ( G e. _V /\ N e. V ) -> ( N o. .- ) = ( dist ` ( G sSet <. ( dist ` ndx ) , ( N o. .- ) >. ) ) ) |
21 |
|
eqid |
|- ( N o. .- ) = ( N o. .- ) |
22 |
|
eqid |
|- ( MetOpen ` ( N o. .- ) ) = ( MetOpen ` ( N o. .- ) ) |
23 |
1 2 21 22
|
tngval |
|- ( ( G e. _V /\ N e. V ) -> T = ( ( G sSet <. ( dist ` ndx ) , ( N o. .- ) >. ) sSet <. ( TopSet ` ndx ) , ( MetOpen ` ( N o. .- ) ) >. ) ) |
24 |
23
|
fveq2d |
|- ( ( G e. _V /\ N e. V ) -> ( dist ` T ) = ( dist ` ( ( G sSet <. ( dist ` ndx ) , ( N o. .- ) >. ) sSet <. ( TopSet ` ndx ) , ( MetOpen ` ( N o. .- ) ) >. ) ) ) |
25 |
15 20 24
|
3eqtr4a |
|- ( ( G e. _V /\ N e. V ) -> ( N o. .- ) = ( dist ` T ) ) |
26 |
|
co02 |
|- ( N o. (/) ) = (/) |
27 |
|
df-ds |
|- dist = Slot ; 1 2 |
28 |
27
|
str0 |
|- (/) = ( dist ` (/) ) |
29 |
26 28
|
eqtri |
|- ( N o. (/) ) = ( dist ` (/) ) |
30 |
|
fvprc |
|- ( -. G e. _V -> ( -g ` G ) = (/) ) |
31 |
2 30
|
syl5eq |
|- ( -. G e. _V -> .- = (/) ) |
32 |
31
|
coeq2d |
|- ( -. G e. _V -> ( N o. .- ) = ( N o. (/) ) ) |
33 |
|
reldmtng |
|- Rel dom toNrmGrp |
34 |
33
|
ovprc1 |
|- ( -. G e. _V -> ( G toNrmGrp N ) = (/) ) |
35 |
1 34
|
syl5eq |
|- ( -. G e. _V -> T = (/) ) |
36 |
35
|
fveq2d |
|- ( -. G e. _V -> ( dist ` T ) = ( dist ` (/) ) ) |
37 |
29 32 36
|
3eqtr4a |
|- ( -. G e. _V -> ( N o. .- ) = ( dist ` T ) ) |
38 |
37
|
adantr |
|- ( ( -. G e. _V /\ N e. V ) -> ( N o. .- ) = ( dist ` T ) ) |
39 |
25 38
|
pm2.61ian |
|- ( N e. V -> ( N o. .- ) = ( dist ` T ) ) |