Metamath Proof Explorer

Theorem metnrmlem1

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 metnrmlem1 
|- ( ( ph /\ ( A e. S /\ B e. T ) ) -> if ( 1 <_ ( F ` B ) , 1 , ( F ` B ) ) <_ ( A D B ) )

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 1xr 
 |-  1 e. RR*
8 3 adantr 
 |-  ( ( ph /\ ( A e. S /\ B e. T ) ) -> D e. ( *Met ` X ) )
9 4 adantr 
 |-  ( ( ph /\ ( A e. S /\ B e. T ) ) -> S e. ( Clsd ` J ) )
10 eqid 
 |-  U. J = U. J
11 10 cldss 
 |-  ( S e. ( Clsd ` J ) -> S C_ U. J )
12 9 11 syl 
 |-  ( ( ph /\ ( A e. S /\ B e. T ) ) -> S C_ U. J )
13 2 mopnuni 
 |-  ( D e. ( *Met ` X ) -> X = U. J )
14 8 13 syl 
 |-  ( ( ph /\ ( A e. S /\ B e. T ) ) -> X = U. J )
15 12 14 sseqtrrd 
 |-  ( ( ph /\ ( A e. S /\ B e. T ) ) -> S C_ X )
16 1 metdsf 
 |-  ( ( D e. ( *Met ` X ) /\ S C_ X ) -> F : X --> ( 0 [,] +oo ) )
17 8 15 16 syl2anc 
 |-  ( ( ph /\ ( A e. S /\ B e. T ) ) -> F : X --> ( 0 [,] +oo ) )
18 5 adantr 
 |-  ( ( ph /\ ( A e. S /\ B e. T ) ) -> T e. ( Clsd ` J ) )
19 10 cldss 
 |-  ( T e. ( Clsd ` J ) -> T C_ U. J )
20 18 19 syl 
 |-  ( ( ph /\ ( A e. S /\ B e. T ) ) -> T C_ U. J )
21 20 14 sseqtrrd 
 |-  ( ( ph /\ ( A e. S /\ B e. T ) ) -> T C_ X )
22 simprr 
 |-  ( ( ph /\ ( A e. S /\ B e. T ) ) -> B e. T )
23 21 22 sseldd 
 |-  ( ( ph /\ ( A e. S /\ B e. T ) ) -> B e. X )
24 17 23 ffvelrnd 
 |-  ( ( ph /\ ( A e. S /\ B e. T ) ) -> ( F ` B ) e. ( 0 [,] +oo ) )
25 eliccxr 
 |-  ( ( F ` B ) e. ( 0 [,] +oo ) -> ( F ` B ) e. RR* )
26 24 25 syl 
 |-  ( ( ph /\ ( A e. S /\ B e. T ) ) -> ( F ` B ) e. RR* )
27 ifcl 
 |-  ( ( 1 e. RR* /\ ( F ` B ) e. RR* ) -> if ( 1 <_ ( F ` B ) , 1 , ( F ` B ) ) e. RR* )
28 7 26 27 sylancr 
 |-  ( ( ph /\ ( A e. S /\ B e. T ) ) -> if ( 1 <_ ( F ` B ) , 1 , ( F ` B ) ) e. RR* )
29 simprl 
 |-  ( ( ph /\ ( A e. S /\ B e. T ) ) -> A e. S )
30 15 29 sseldd 
 |-  ( ( ph /\ ( A e. S /\ B e. T ) ) -> A e. X )
31 xmetcl 
 |-  ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> ( A D B ) e. RR* )
32 8 30 23 31 syl3anc 
 |-  ( ( ph /\ ( A e. S /\ B e. T ) ) -> ( A D B ) e. RR* )
33 xrmin2 
 |-  ( ( 1 e. RR* /\ ( F ` B ) e. RR* ) -> if ( 1 <_ ( F ` B ) , 1 , ( F ` B ) ) <_ ( F ` B ) )
34 7 26 33 sylancr 
 |-  ( ( ph /\ ( A e. S /\ B e. T ) ) -> if ( 1 <_ ( F ` B ) , 1 , ( F ` B ) ) <_ ( F ` B ) )
35 1 metdstri 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( B e. X /\ A e. X ) ) -> ( F ` B ) <_ ( ( B D A ) +e ( F ` A ) ) )
36 8 15 23 30 35 syl22anc 
 |-  ( ( ph /\ ( A e. S /\ B e. T ) ) -> ( F ` B ) <_ ( ( B D A ) +e ( F ` A ) ) )
37 xmetsym 
 |-  ( ( D e. ( *Met ` X ) /\ B e. X /\ A e. X ) -> ( B D A ) = ( A D B ) )
38 8 23 30 37 syl3anc 
 |-  ( ( ph /\ ( A e. S /\ B e. T ) ) -> ( B D A ) = ( A D B ) )
39 1 metds0 
 |-  ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. S ) -> ( F ` A ) = 0 )
40 8 15 29 39 syl3anc 
 |-  ( ( ph /\ ( A e. S /\ B e. T ) ) -> ( F ` A ) = 0 )
41 38 40 oveq12d 
 |-  ( ( ph /\ ( A e. S /\ B e. T ) ) -> ( ( B D A ) +e ( F ` A ) ) = ( ( A D B ) +e 0 ) )
42 32 xaddid1d 
 |-  ( ( ph /\ ( A e. S /\ B e. T ) ) -> ( ( A D B ) +e 0 ) = ( A D B ) )
43 41 42 eqtrd 
 |-  ( ( ph /\ ( A e. S /\ B e. T ) ) -> ( ( B D A ) +e ( F ` A ) ) = ( A D B ) )
44 36 43 breqtrd 
 |-  ( ( ph /\ ( A e. S /\ B e. T ) ) -> ( F ` B ) <_ ( A D B ) )
45 28 26 32 34 44 xrletrd 
 |-  ( ( ph /\ ( A e. S /\ B e. T ) ) -> if ( 1 <_ ( F ` B ) , 1 , ( F ` B ) ) <_ ( A D B ) )