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