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

Theorem tngds 21734
 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 15379 . . . 4 Slot
2 9re 10718 . . . . . 6
3 1nn 10642 . . . . . . 7
4 2nn0 10910 . . . . . . 7
5 9nn0 10917 . . . . . . 7
6 9lt10 10835 . . . . . . 7
73, 4, 5, 6declti 11099 . . . . . 6 ;
82, 7gtneii 9764 . . . . 5 ;
9 dsndx 15378 . . . . . 6 ;
10 tsetndx 15362 . . . . . 6 TopSet
119, 10neeq12i 2709 . . . . 5 TopSet ;
128, 11mpbir 214 . . . 4 TopSet
131, 12setsnid 15243 . . 3 sSet sSet sSet TopSet
14 tngds.2 . . . . . 6
15 fvex 5889 . . . . . 6
1614, 15eqeltri 2545 . . . . 5
17 coexg 6763 . . . . 5
1816, 17mpan2 685 . . . 4
191setsid 15242 . . . 4 sSet
2018, 19sylan2 482 . . 3 sSet
21 tngbas.t . . . . 5 toNrmGrp
22 eqid 2471 . . . . 5
23 eqid 2471 . . . . 5
2421, 14, 22, 23tngval 21725 . . . 4 sSet sSet TopSet
2524fveq2d 5883 . . 3 sSet sSet TopSet
2613, 20, 253eqtr4a 2531 . 2
27 co02 5356 . . . . 5
28 df-ds 15290 . . . . . 6 Slot ;
2928str0 15239 . . . . 5
3027, 29eqtri 2493 . . . 4
31 fvprc 5873 . . . . . 6
3214, 31syl5eq 2517 . . . . 5
3332coeq2d 5002 . . . 4
34 reldmtng 21724 . . . . . . 7 toNrmGrp
3534ovprc1 6339 . . . . . 6 toNrmGrp
3621, 35syl5eq 2517 . . . . 5
3736fveq2d 5883 . . . 4
3830, 33, 373eqtr4a 2531 . . 3