Metamath Proof Explorer


Theorem tngdsOLD

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 T=GtoNrmGrpN
tngds.2 -˙=-G
Assertion tngdsOLD NVN-˙=distT

Proof

Step Hyp Ref Expression
1 tngbas.t T=GtoNrmGrpN
2 tngds.2 -˙=-G
3 dsid dist=Slotdistndx
4 9re 9
5 1nn 1
6 2nn0 20
7 9nn0 90
8 9lt10 9<10
9 5 6 7 8 declti 9<12
10 4 9 gtneii 129
11 dsndx distndx=12
12 tsetndx TopSetndx=9
13 11 12 neeq12i distndxTopSetndx129
14 10 13 mpbir distndxTopSetndx
15 3 14 setsnid distGsSetdistndxN-˙=distGsSetdistndxN-˙sSetTopSetndxMetOpenN-˙
16 2 fvexi -˙V
17 coexg NV-˙VN-˙V
18 16 17 mpan2 NVN-˙V
19 3 setsid GVN-˙VN-˙=distGsSetdistndxN-˙
20 18 19 sylan2 GVNVN-˙=distGsSetdistndxN-˙
21 eqid N-˙=N-˙
22 eqid MetOpenN-˙=MetOpenN-˙
23 1 2 21 22 tngval GVNVT=GsSetdistndxN-˙sSetTopSetndxMetOpenN-˙
24 23 fveq2d GVNVdistT=distGsSetdistndxN-˙sSetTopSetndxMetOpenN-˙
25 15 20 24 3eqtr4a GVNVN-˙=distT
26 co02 N=
27 df-ds dist=Slot12
28 27 str0 =dist
29 26 28 eqtri N=dist
30 fvprc ¬GV-G=
31 2 30 eqtrid ¬GV-˙=
32 31 coeq2d ¬GVN-˙=N
33 reldmtng ReldomtoNrmGrp
34 33 ovprc1 ¬GVGtoNrmGrpN=
35 1 34 eqtrid ¬GVT=
36 35 fveq2d ¬GVdistT=dist
37 29 32 36 3eqtr4a ¬GVN-˙=distT
38 37 adantr ¬GVNVN-˙=distT
39 25 38 pm2.61ian NVN-˙=distT