Description: Obsolete proof of tngds as of 29-Oct-2024. The metric function of a structure augmented with a norm. (Contributed by Mario Carneiro, 3-Oct-2015) (Proof modification is discouraged.) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | tngbas.t | |
|
tngds.2 | |
||
Assertion | tngdsOLD | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tngbas.t | |
|
2 | tngds.2 | |
|
3 | dsid | |
|
4 | 9re | |
|
5 | 1nn | |
|
6 | 2nn0 | |
|
7 | 9nn0 | |
|
8 | 9lt10 | |
|
9 | 5 6 7 8 | declti | |
10 | 4 9 | gtneii | |
11 | dsndx | |
|
12 | tsetndx | |
|
13 | 11 12 | neeq12i | |
14 | 10 13 | mpbir | |
15 | 3 14 | setsnid | |
16 | 2 | fvexi | |
17 | coexg | |
|
18 | 16 17 | mpan2 | |
19 | 3 | setsid | |
20 | 18 19 | sylan2 | |
21 | eqid | |
|
22 | eqid | |
|
23 | 1 2 21 22 | tngval | |
24 | 23 | fveq2d | |
25 | 15 20 24 | 3eqtr4a | |
26 | co02 | |
|
27 | df-ds | |
|
28 | 27 | str0 | |
29 | 26 28 | eqtri | |
30 | fvprc | |
|
31 | 2 30 | eqtrid | |
32 | 31 | coeq2d | |
33 | reldmtng | |
|
34 | 33 | ovprc1 | |
35 | 1 34 | eqtrid | |
36 | 35 | fveq2d | |
37 | 29 32 36 | 3eqtr4a | |
38 | 37 | adantr | |
39 | 25 38 | pm2.61ian | |