Metamath Proof Explorer

Theorem tngds

Description: The metric function of a structure augmented with a norm. (Contributed by Mario Carneiro, 3-Oct-2015)

Ref Expression
Hypotheses tngbas.t 
|- T = ( G toNrmGrp N )
tngds.2 
|- .- = ( -g ` G )
Assertion tngds 
|- ( N e. V -> ( N o. .- ) = ( dist ` T ) )

Proof

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 ) )