Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  tngds Structured version   Unicode version

Theorem tngds 18720
 Description: The metric function of a structure augmented with a norm. (Contributed by Mario Carneiro, 3-Oct-2015.)
Hypotheses
Ref Expression
tngbas.t toNrmGrp
tngds.2
Assertion
Ref Expression
tngds

Proof of Theorem tngds
StepHypRef Expression
1 dsid 13662 . . . 4 Slot
2 9re 10110 . . . . . 6
3 1nn 10042 . . . . . . 7
4 2nn0 10269 . . . . . . 7
5 9nn0 10276 . . . . . . 7
6 9lt10 10209 . . . . . . 7
73, 4, 5, 6declti 10438 . . . . . 6 ;
82, 7gtneii 9216 . . . . 5 ;
9 dsndx 13661 . . . . . 6 ;
10 tsetndx 13645 . . . . . 6 TopSet
119, 10neeq12i 2619 . . . . 5 TopSet ;
128, 11mpbir 202 . . . 4 TopSet
131, 12setsnid 13540 . . 3 sSet sSet sSet TopSet
14 tngds.2 . . . . . 6
15 fvex 5771 . . . . . 6
1614, 15eqeltri 2512 . . . . 5
17 coexg 5441 . . . . 5
1816, 17mpan2 654 . . . 4
191setsid 13539 . . . 4 sSet
2018, 19sylan2 462 . . 3 sSet
21 tngbas.t . . . . 5 toNrmGrp
22 eqid 2442 . . . . 5
23 eqid 2442 . . . . 5
2421, 14, 22, 23tngval 18711 . . . 4 sSet sSet TopSet
2524fveq2d 5761 . . 3 sSet sSet TopSet
2613, 20, 253eqtr4a 2500 . 2
27 co02 5412 . . . . 5
28 df-ds 13582 . . . . . 6 Slot ;
2928str0 13536 . . . . 5
3027, 29eqtri 2462 . . . 4
31 fvprc 5751 . . . . . 6
3214, 31syl5eq 2486 . . . . 5
3332coeq2d 5064 . . . 4
34 reldmtng 18710 . . . . . . 7 toNrmGrp
3534ovprc1 6138 . . . . . 6 toNrmGrp
3621, 35syl5eq 2486 . . . . 5
3736fveq2d 5761 . . . 4
3830, 33, 373eqtr4a 2500 . . 3