Metamath Proof Explorer

Theorem metnrmlem1a

Description: Lemma for metnrm . (Contributed by Mario Carneiro, 14-Jan-2014) (Revised by Mario Carneiro, 4-Sep-2015)

Ref Expression
Hypotheses metdscn.f 
|- F = ( x e. X |-> inf ( ran ( y e. S |-> ( x D y ) ) , RR* , < ) )
metdscn.j 
|- J = ( MetOpen ` D )
metnrmlem.1 
|- ( ph -> D e. ( *Met ` X ) )
metnrmlem.2 
|- ( ph -> S e. ( Clsd ` J ) )
metnrmlem.3 
|- ( ph -> T e. ( Clsd ` J ) )
metnrmlem.4 
|- ( ph -> ( S i^i T ) = (/) )
Assertion metnrmlem1a 
|- ( ( ph /\ A e. T ) -> ( 0 < ( F ` A ) /\ if ( 1 <_ ( F ` A ) , 1 , ( F ` A ) ) e. RR+ ) )

Proof

Step Hyp Ref Expression
1 metdscn.f 
 |-  F = ( x e. X |-> inf ( ran ( y e. S |-> ( x D y ) ) , RR* , < ) )
2 metdscn.j 
 |-  J = ( MetOpen ` D )
3 metnrmlem.1 
 |-  ( ph -> D e. ( *Met ` X ) )
4 metnrmlem.2 
 |-  ( ph -> S e. ( Clsd ` J ) )
5 metnrmlem.3 
 |-  ( ph -> T e. ( Clsd ` J ) )
6 metnrmlem.4 
 |-  ( ph -> ( S i^i T ) = (/) )
7 6 adantr 
 |-  ( ( ph /\ A e. T ) -> ( S i^i T ) = (/) )
8 inelcm 
 |-  ( ( A e. S /\ A e. T ) -> ( S i^i T ) =/= (/) )
9 8 expcom 
 |-  ( A e. T -> ( A e. S -> ( S i^i T ) =/= (/) ) )
10 9 adantl 
 |-  ( ( ph /\ A e. T ) -> ( A e. S -> ( S i^i T ) =/= (/) ) )
11 10 necon2bd 
 |-  ( ( ph /\ A e. T ) -> ( ( S i^i T ) = (/) -> -. A e. S ) )
12 7 11 mpd 
 |-  ( ( ph /\ A e. T ) -> -. A e. S )
13 eqcom 
 |-  ( 0 = ( F ` A ) <-> ( F ` A ) = 0 )
14 3 adantr 
 |-  ( ( ph /\ A e. T ) -> D e. ( *Met ` X ) )
15 4 adantr 
 |-  ( ( ph /\ A e. T ) -> S e. ( Clsd ` J ) )
16 eqid 
 |-  U. J = U. J
17 16 cldss 
 |-  ( S e. ( Clsd ` J ) -> S C_ U. J )
18 15 17 syl 
 |-  ( ( ph /\ A e. T ) -> S C_ U. J )
19 2 mopnuni 
 |-  ( D e. ( *Met ` X ) -> X = U. J )
20 14 19 syl 
 |-  ( ( ph /\ A e. T ) -> X = U. J )
21 18 20 sseqtrrd 
 |-  ( ( ph /\ A e. T ) -> S C_ X )
22 5 adantr 
 |-  ( ( ph /\ A e. T ) -> T e. ( Clsd ` J ) )
23 16 cldss 
 |-  ( T e. ( Clsd ` J ) -> T C_ U. J )
24 22 23 syl 
 |-  ( ( ph /\ A e. T ) -> T C_ U. J )
25 24 20 sseqtrrd 
 |-  ( ( ph /\ A e. T ) -> T C_ X )
26 simpr 
 |-  ( ( ph /\ A e. T ) -> A e. T )
27 25 26 sseldd 
 |-  ( ( ph /\ A e. T ) -> A e. X )
28 1 2 metdseq0 
 |-  ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. X ) -> ( ( F ` A ) = 0 <-> A e. ( ( cls ` J ) ` S ) ) )
29 14 21 27 28 syl3anc 
 |-  ( ( ph /\ A e. T ) -> ( ( F ` A ) = 0 <-> A e. ( ( cls ` J ) ` S ) ) )
30 13 29 syl5bb 
 |-  ( ( ph /\ A e. T ) -> ( 0 = ( F ` A ) <-> A e. ( ( cls ` J ) ` S ) ) )
31 cldcls 
 |-  ( S e. ( Clsd ` J ) -> ( ( cls ` J ) ` S ) = S )
32 15 31 syl 
 |-  ( ( ph /\ A e. T ) -> ( ( cls ` J ) ` S ) = S )
33 32 eleq2d 
 |-  ( ( ph /\ A e. T ) -> ( A e. ( ( cls ` J ) ` S ) <-> A e. S ) )
34 30 33 bitrd 
 |-  ( ( ph /\ A e. T ) -> ( 0 = ( F ` A ) <-> A e. S ) )
35 12 34 mtbird 
 |-  ( ( ph /\ A e. T ) -> -. 0 = ( F ` A ) )
36 1 metdsf 
 |-  ( ( D e. ( *Met ` X ) /\ S C_ X ) -> F : X --> ( 0 [,] +oo ) )
37 14 21 36 syl2anc 
 |-  ( ( ph /\ A e. T ) -> F : X --> ( 0 [,] +oo ) )
38 37 27 ffvelrnd 
 |-  ( ( ph /\ A e. T ) -> ( F ` A ) e. ( 0 [,] +oo ) )
39 elxrge0 
 |-  ( ( F ` A ) e. ( 0 [,] +oo ) <-> ( ( F ` A ) e. RR* /\ 0 <_ ( F ` A ) ) )
40 39 simprbi 
 |-  ( ( F ` A ) e. ( 0 [,] +oo ) -> 0 <_ ( F ` A ) )
41 38 40 syl 
 |-  ( ( ph /\ A e. T ) -> 0 <_ ( F ` A ) )
42 0xr 
 |-  0 e. RR*
43 eliccxr 
 |-  ( ( F ` A ) e. ( 0 [,] +oo ) -> ( F ` A ) e. RR* )
44 38 43 syl 
 |-  ( ( ph /\ A e. T ) -> ( F ` A ) e. RR* )
45 xrleloe 
 |-  ( ( 0 e. RR* /\ ( F ` A ) e. RR* ) -> ( 0 <_ ( F ` A ) <-> ( 0 < ( F ` A ) \/ 0 = ( F ` A ) ) ) )
46 42 44 45 sylancr 
 |-  ( ( ph /\ A e. T ) -> ( 0 <_ ( F ` A ) <-> ( 0 < ( F ` A ) \/ 0 = ( F ` A ) ) ) )
47 41 46 mpbid 
 |-  ( ( ph /\ A e. T ) -> ( 0 < ( F ` A ) \/ 0 = ( F ` A ) ) )
48 47 ord 
 |-  ( ( ph /\ A e. T ) -> ( -. 0 < ( F ` A ) -> 0 = ( F ` A ) ) )
49 35 48 mt3d 
 |-  ( ( ph /\ A e. T ) -> 0 < ( F ` A ) )
50 1xr 
 |-  1 e. RR*
51 ifcl 
 |-  ( ( 1 e. RR* /\ ( F ` A ) e. RR* ) -> if ( 1 <_ ( F ` A ) , 1 , ( F ` A ) ) e. RR* )
52 50 44 51 sylancr 
 |-  ( ( ph /\ A e. T ) -> if ( 1 <_ ( F ` A ) , 1 , ( F ` A ) ) e. RR* )
53 1red 
 |-  ( ( ph /\ A e. T ) -> 1 e. RR )
54 0lt1 
 |-  0 < 1
55 breq2 
 |-  ( 1 = if ( 1 <_ ( F ` A ) , 1 , ( F ` A ) ) -> ( 0 < 1 <-> 0 < if ( 1 <_ ( F ` A ) , 1 , ( F ` A ) ) ) )
56 breq2 
 |-  ( ( F ` A ) = if ( 1 <_ ( F ` A ) , 1 , ( F ` A ) ) -> ( 0 < ( F ` A ) <-> 0 < if ( 1 <_ ( F ` A ) , 1 , ( F ` A ) ) ) )
57 55 56 ifboth 
 |-  ( ( 0 < 1 /\ 0 < ( F ` A ) ) -> 0 < if ( 1 <_ ( F ` A ) , 1 , ( F ` A ) ) )
58 54 49 57 sylancr 
 |-  ( ( ph /\ A e. T ) -> 0 < if ( 1 <_ ( F ` A ) , 1 , ( F ` A ) ) )
59 xrltle 
 |-  ( ( 0 e. RR* /\ if ( 1 <_ ( F ` A ) , 1 , ( F ` A ) ) e. RR* ) -> ( 0 < if ( 1 <_ ( F ` A ) , 1 , ( F ` A ) ) -> 0 <_ if ( 1 <_ ( F ` A ) , 1 , ( F ` A ) ) ) )
60 42 52 59 sylancr 
 |-  ( ( ph /\ A e. T ) -> ( 0 < if ( 1 <_ ( F ` A ) , 1 , ( F ` A ) ) -> 0 <_ if ( 1 <_ ( F ` A ) , 1 , ( F ` A ) ) ) )
61 58 60 mpd 
 |-  ( ( ph /\ A e. T ) -> 0 <_ if ( 1 <_ ( F ` A ) , 1 , ( F ` A ) ) )
62 xrmin1 
 |-  ( ( 1 e. RR* /\ ( F ` A ) e. RR* ) -> if ( 1 <_ ( F ` A ) , 1 , ( F ` A ) ) <_ 1 )
63 50 44 62 sylancr 
 |-  ( ( ph /\ A e. T ) -> if ( 1 <_ ( F ` A ) , 1 , ( F ` A ) ) <_ 1 )
64 xrrege0 
 |-  ( ( ( if ( 1 <_ ( F ` A ) , 1 , ( F ` A ) ) e. RR* /\ 1 e. RR ) /\ ( 0 <_ if ( 1 <_ ( F ` A ) , 1 , ( F ` A ) ) /\ if ( 1 <_ ( F ` A ) , 1 , ( F ` A ) ) <_ 1 ) ) -> if ( 1 <_ ( F ` A ) , 1 , ( F ` A ) ) e. RR )
65 52 53 61 63 64 syl22anc 
 |-  ( ( ph /\ A e. T ) -> if ( 1 <_ ( F ` A ) , 1 , ( F ` A ) ) e. RR )
66 65 58 elrpd 
 |-  ( ( ph /\ A e. T ) -> if ( 1 <_ ( F ` A ) , 1 , ( F ` A ) ) e. RR+ )
67 49 66 jca 
 |-  ( ( ph /\ A e. T ) -> ( 0 < ( F ` A ) /\ if ( 1 <_ ( F ` A ) , 1 , ( F ` A ) ) e. RR+ ) )