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 ) )