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