This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ inf ( ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ* , < ) )
metdscn.j ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
metnrmlem.1 ⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
metnrmlem.2 ⊢ ( 𝜑 → 𝑆 ∈ ( Clsd ‘ 𝐽 ) )
metnrmlem.3 ⊢ ( 𝜑 → 𝑇 ∈ ( Clsd ‘ 𝐽 ) )
metnrmlem.4 ⊢ ( 𝜑 → ( 𝑆 ∩ 𝑇 ) = ∅ )
Assertion metnrmlem1 ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → if ( 1 ≤ ( 𝐹 ‘ 𝐵 ) , 1 , ( 𝐹 ‘ 𝐵 ) ) ≤ ( 𝐴 𝐷 𝐵 ) )

Proof

Step Hyp Ref Expression
1 metdscn.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ inf ( ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ* , < ) )
2 metdscn.j ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
3 metnrmlem.1 ⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
4 metnrmlem.2 ⊢ ( 𝜑 → 𝑆 ∈ ( Clsd ‘ 𝐽 ) )
5 metnrmlem.3 ⊢ ( 𝜑 → 𝑇 ∈ ( Clsd ‘ 𝐽 ) )
6 metnrmlem.4 ⊢ ( 𝜑 → ( 𝑆 ∩ 𝑇 ) = ∅ )
7 1xr ⊢ 1 ∈ ℝ*
8 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
9 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → 𝑆 ∈ ( Clsd ‘ 𝐽 ) )
10 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
11 10 cldss ⊢ ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) → 𝑆 ⊆ ∪ 𝐽 )
12 9 11 syl ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → 𝑆 ⊆ ∪ 𝐽 )
13 2 mopnuni ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
14 8 13 syl ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → 𝑋 = ∪ 𝐽 )
15 12 14 sseqtrrd ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → 𝑆 ⊆ 𝑋 )
16 1 metdsf ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
17 8 15 16 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
18 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → 𝑇 ∈ ( Clsd ‘ 𝐽 ) )
19 10 cldss ⊢ ( 𝑇 ∈ ( Clsd ‘ 𝐽 ) → 𝑇 ⊆ ∪ 𝐽 )
20 18 19 syl ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → 𝑇 ⊆ ∪ 𝐽 )
21 20 14 sseqtrrd ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → 𝑇 ⊆ 𝑋 )
22 simprr ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → 𝐵 ∈ 𝑇 )
23 21 22 sseldd ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → 𝐵 ∈ 𝑋 )
24 17 23 ffvelcdmd ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → ( 𝐹 ‘ 𝐵 ) ∈ ( 0 [,] +∞ ) )
25 eliccxr ⊢ ( ( 𝐹 ‘ 𝐵 ) ∈ ( 0 [,] +∞ ) → ( 𝐹 ‘ 𝐵 ) ∈ ℝ* )
26 24 25 syl ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → ( 𝐹 ‘ 𝐵 ) ∈ ℝ* )
27 ifcl ⊢ ( ( 1 ∈ ℝ* ∧ ( 𝐹 ‘ 𝐵 ) ∈ ℝ* ) → if ( 1 ≤ ( 𝐹 ‘ 𝐵 ) , 1 , ( 𝐹 ‘ 𝐵 ) ) ∈ ℝ* )
28 7 26 27 sylancr ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → if ( 1 ≤ ( 𝐹 ‘ 𝐵 ) , 1 , ( 𝐹 ‘ 𝐵 ) ) ∈ ℝ* )
29 simprl ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → 𝐴 ∈ 𝑆 )
30 15 29 sseldd ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → 𝐴 ∈ 𝑋 )
31 xmetcl ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐵 ) ∈ ℝ* )
32 8 30 23 31 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → ( 𝐴 𝐷 𝐵 ) ∈ ℝ* )
33 xrmin2 ⊢ ( ( 1 ∈ ℝ* ∧ ( 𝐹 ‘ 𝐵 ) ∈ ℝ* ) → if ( 1 ≤ ( 𝐹 ‘ 𝐵 ) , 1 , ( 𝐹 ‘ 𝐵 ) ) ≤ ( 𝐹 ‘ 𝐵 ) )
34 7 26 33 sylancr ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → if ( 1 ≤ ( 𝐹 ‘ 𝐵 ) , 1 , ( 𝐹 ‘ 𝐵 ) ) ≤ ( 𝐹 ‘ 𝐵 ) )
35 1 metdstri ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝐵 ) ≤ ( ( 𝐵 𝐷 𝐴 ) +𝑒 ( 𝐹 ‘ 𝐴 ) ) )
36 8 15 23 30 35 syl22anc ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → ( 𝐹 ‘ 𝐵 ) ≤ ( ( 𝐵 𝐷 𝐴 ) +𝑒 ( 𝐹 ‘ 𝐴 ) ) )
37 xmetsym ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐵 𝐷 𝐴 ) = ( 𝐴 𝐷 𝐵 ) )
38 8 23 30 37 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → ( 𝐵 𝐷 𝐴 ) = ( 𝐴 𝐷 𝐵 ) )
39 1 metds0 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆 ) → ( 𝐹 ‘ 𝐴 ) = 0 )
40 8 15 29 39 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → ( 𝐹 ‘ 𝐴 ) = 0 )
41 38 40 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → ( ( 𝐵 𝐷 𝐴 ) +𝑒 ( 𝐹 ‘ 𝐴 ) ) = ( ( 𝐴 𝐷 𝐵 ) +𝑒 0 ) )
42 32 xaddridd ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → ( ( 𝐴 𝐷 𝐵 ) +𝑒 0 ) = ( 𝐴 𝐷 𝐵 ) )
43 41 42 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → ( ( 𝐵 𝐷 𝐴 ) +𝑒 ( 𝐹 ‘ 𝐴 ) ) = ( 𝐴 𝐷 𝐵 ) )
44 36 43 breqtrd ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → ( 𝐹 ‘ 𝐵 ) ≤ ( 𝐴 𝐷 𝐵 ) )
45 28 26 32 34 44 xrletrd ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → if ( 1 ≤ ( 𝐹 ‘ 𝐵 ) , 1 , ( 𝐹 ‘ 𝐵 ) ) ≤ ( 𝐴 𝐷 𝐵 ) )