Metamath Proof Explorer


Theorem tngds

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

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