Metamath Proof Explorer

Theorem metnrmlem3

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

Ref Expression
Hypotheses metdscn.f ⊢F=x∈X⟼supran⁡y∈S⟼xDyℝ*<
metdscn.j ⊢J=MetOpen⁡D
metnrmlem.1 ⊢φ→D∈∞Met⁡X
metnrmlem.2 ⊢φ→S∈Clsd⁡J
metnrmlem.3 ⊢φ→T∈Clsd⁡J
metnrmlem.4 ⊢φ→S∩T=∅
metnrmlem.u ⊢U=⋃t∈Ttball⁡Dif1≤F⁡t1F⁡t2
metnrmlem.g ⊢G=x∈X⟼supran⁡y∈T⟼xDyℝ*<
metnrmlem.v ⊢V=⋃s∈Ssball⁡Dif1≤G⁡s1G⁡s2
Assertion metnrmlem3 ⊢φ→∃z∈J∃w∈JS⊆z∧T⊆w∧z∩w=∅

Proof

Step Hyp Ref Expression
1 metdscn.f ⊢F=x∈X⟼supran⁡y∈S⟼xDyℝ*<
2 metdscn.j ⊢J=MetOpen⁡D
3 metnrmlem.1 ⊢φ→D∈∞Met⁡X
4 metnrmlem.2 ⊢φ→S∈Clsd⁡J
5 metnrmlem.3 ⊢φ→T∈Clsd⁡J
6 metnrmlem.4 ⊢φ→S∩T=∅
7 metnrmlem.u ⊢U=⋃t∈Ttball⁡Dif1≤F⁡t1F⁡t2
8 metnrmlem.g ⊢G=x∈X⟼supran⁡y∈T⟼xDyℝ*<
9 metnrmlem.v ⊢V=⋃s∈Ssball⁡Dif1≤G⁡s1G⁡s2
10 incom ⊢T∩S=S∩T
11 10 6 eqtrid ⊢φ→T∩S=∅
12 8 2 3 5 4 11 9 metnrmlem2 ⊢φ→V∈J∧S⊆V
13 12 simpld ⊢φ→V∈J
14 1 2 3 4 5 6 7 metnrmlem2 ⊢φ→U∈J∧T⊆U
15 14 simpld ⊢φ→U∈J
16 12 simprd ⊢φ→S⊆V
17 14 simprd ⊢φ→T⊆U
18 9 ineq1i ⊢V∩U=⋃s∈Ssball⁡Dif1≤G⁡s1G⁡s2∩U
19 iunin1 ⊢⋃s∈Ssball⁡Dif1≤G⁡s1G⁡s2∩U=⋃s∈Ssball⁡Dif1≤G⁡s1G⁡s2∩U
20 18 19 eqtr4i ⊢V∩U=⋃s∈Ssball⁡Dif1≤G⁡s1G⁡s2∩U
21 7 ineq2i ⊢sball⁡Dif1≤G⁡s1G⁡s2∩U=sball⁡Dif1≤G⁡s1G⁡s2∩⋃t∈Ttball⁡Dif1≤F⁡t1F⁡t2
22 iunin2 ⊢⋃t∈Tsball⁡Dif1≤G⁡s1G⁡s2∩tball⁡Dif1≤F⁡t1F⁡t2=sball⁡Dif1≤G⁡s1G⁡s2∩⋃t∈Ttball⁡Dif1≤F⁡t1F⁡t2
23 21 22 eqtr4i ⊢sball⁡Dif1≤G⁡s1G⁡s2∩U=⋃t∈Tsball⁡Dif1≤G⁡s1G⁡s2∩tball⁡Dif1≤F⁡t1F⁡t2
24 3 adantr ⊢φ∧s∈S∧t∈T→D∈∞Met⁡X
25 eqid ⊢⋃J=⋃J
26 25 cldss ⊢S∈Clsd⁡J→S⊆⋃J
27 4 26 syl ⊢φ→S⊆⋃J
28 2 mopnuni ⊢D∈∞Met⁡X→X=⋃J
29 3 28 syl ⊢φ→X=⋃J
30 27 29 sseqtrrd ⊢φ→S⊆X
31 30 sselda ⊢φ∧s∈S→s∈X
32 31 adantrr ⊢φ∧s∈S∧t∈T→s∈X
33 25 cldss ⊢T∈Clsd⁡J→T⊆⋃J
34 5 33 syl ⊢φ→T⊆⋃J
35 34 29 sseqtrrd ⊢φ→T⊆X
36 35 sselda ⊢φ∧t∈T→t∈X
37 36 adantrl ⊢φ∧s∈S∧t∈T→t∈X
38 8 2 3 5 4 11 metnrmlem1a ⊢φ∧s∈S→0<G⁡s∧if1≤G⁡s1G⁡s∈ℝ+
39 38 simprd ⊢φ∧s∈S→if1≤G⁡s1G⁡s∈ℝ+
40 39 adantrr ⊢φ∧s∈S∧t∈T→if1≤G⁡s1G⁡s∈ℝ+
41 40 rphalfcld ⊢φ∧s∈S∧t∈T→if1≤G⁡s1G⁡s2∈ℝ+
42 41 rpxrd ⊢φ∧s∈S∧t∈T→if1≤G⁡s1G⁡s2∈ℝ*
43 1 2 3 4 5 6 metnrmlem1a ⊢φ∧t∈T→0<F⁡t∧if1≤F⁡t1F⁡t∈ℝ+
44 43 adantrl ⊢φ∧s∈S∧t∈T→0<F⁡t∧if1≤F⁡t1F⁡t∈ℝ+
45 44 simprd ⊢φ∧s∈S∧t∈T→if1≤F⁡t1F⁡t∈ℝ+
46 45 rphalfcld ⊢φ∧s∈S∧t∈T→if1≤F⁡t1F⁡t2∈ℝ+
47 46 rpxrd ⊢φ∧s∈S∧t∈T→if1≤F⁡t1F⁡t2∈ℝ*
48 40 rpred ⊢φ∧s∈S∧t∈T→if1≤G⁡s1G⁡s∈ℝ
49 48 rehalfcld ⊢φ∧s∈S∧t∈T→if1≤G⁡s1G⁡s2∈ℝ
50 45 rpred ⊢φ∧s∈S∧t∈T→if1≤F⁡t1F⁡t∈ℝ
51 50 rehalfcld ⊢φ∧s∈S∧t∈T→if1≤F⁡t1F⁡t2∈ℝ
52 49 51 rexaddd ⊢φ∧s∈S∧t∈T→if1≤G⁡s1G⁡s2+𝑒if1≤F⁡t1F⁡t2=if1≤G⁡s1G⁡s2+if1≤F⁡t1F⁡t2
53 48 recnd ⊢φ∧s∈S∧t∈T→if1≤G⁡s1G⁡s∈ℂ
54 50 recnd ⊢φ∧s∈S∧t∈T→if1≤F⁡t1F⁡t∈ℂ
55 2cnd ⊢φ∧s∈S∧t∈T→2∈ℂ
56 2ne0 ⊢2≠0
57 56 a1i ⊢φ∧s∈S∧t∈T→2≠0
58 53 54 55 57 divdird ⊢φ∧s∈S∧t∈T→if1≤G⁡s1G⁡s+if1≤F⁡t1F⁡t2=if1≤G⁡s1G⁡s2+if1≤F⁡t1F⁡t2
59 52 58 eqtr4d ⊢φ∧s∈S∧t∈T→if1≤G⁡s1G⁡s2+𝑒if1≤F⁡t1F⁡t2=if1≤G⁡s1G⁡s+if1≤F⁡t1F⁡t2
60 8 2 3 5 4 11 metnrmlem1 ⊢φ∧t∈T∧s∈S→if1≤G⁡s1G⁡s≤tDs
61 60 ancom2s ⊢φ∧s∈S∧t∈T→if1≤G⁡s1G⁡s≤tDs
62 xmetsym ⊢D∈∞Met⁡X∧t∈X∧s∈X→tDs=sDt
63 24 37 32 62 syl3anc ⊢φ∧s∈S∧t∈T→tDs=sDt
64 61 63 breqtrd ⊢φ∧s∈S∧t∈T→if1≤G⁡s1G⁡s≤sDt
65 1 2 3 4 5 6 metnrmlem1 ⊢φ∧s∈S∧t∈T→if1≤F⁡t1F⁡t≤sDt
66 40 rpxrd ⊢φ∧s∈S∧t∈T→if1≤G⁡s1G⁡s∈ℝ*
67 45 rpxrd ⊢φ∧s∈S∧t∈T→if1≤F⁡t1F⁡t∈ℝ*
68 xmetcl ⊢D∈∞Met⁡X∧s∈X∧t∈X→sDt∈ℝ*
69 24 32 37 68 syl3anc ⊢φ∧s∈S∧t∈T→sDt∈ℝ*
70 xle2add ⊢if1≤G⁡s1G⁡s∈ℝ*∧if1≤F⁡t1F⁡t∈ℝ*∧sDt∈ℝ*∧sDt∈ℝ*→if1≤G⁡s1G⁡s≤sDt∧if1≤F⁡t1F⁡t≤sDt→if1≤G⁡s1G⁡s+𝑒if1≤F⁡t1F⁡t≤sDt+𝑒sDt
71 66 67 69 69 70 syl22anc ⊢φ∧s∈S∧t∈T→if1≤G⁡s1G⁡s≤sDt∧if1≤F⁡t1F⁡t≤sDt→if1≤G⁡s1G⁡s+𝑒if1≤F⁡t1F⁡t≤sDt+𝑒sDt
72 64 65 71 mp2and ⊢φ∧s∈S∧t∈T→if1≤G⁡s1G⁡s+𝑒if1≤F⁡t1F⁡t≤sDt+𝑒sDt
73 48 50 readdcld ⊢φ∧s∈S∧t∈T→if1≤G⁡s1G⁡s+if1≤F⁡t1F⁡t∈ℝ
74 73 recnd ⊢φ∧s∈S∧t∈T→if1≤G⁡s1G⁡s+if1≤F⁡t1F⁡t∈ℂ
75 74 55 57 divcan2d ⊢φ∧s∈S∧t∈T→2⁢if1≤G⁡s1G⁡s+if1≤F⁡t1F⁡t2=if1≤G⁡s1G⁡s+if1≤F⁡t1F⁡t
76 2re ⊢2∈ℝ
77 73 rehalfcld ⊢φ∧s∈S∧t∈T→if1≤G⁡s1G⁡s+if1≤F⁡t1F⁡t2∈ℝ
78 rexmul ⊢2∈ℝ∧if1≤G⁡s1G⁡s+if1≤F⁡t1F⁡t2∈ℝ→2⋅𝑒if1≤G⁡s1G⁡s+if1≤F⁡t1F⁡t2=2⁢if1≤G⁡s1G⁡s+if1≤F⁡t1F⁡t2
79 76 77 78 sylancr ⊢φ∧s∈S∧t∈T→2⋅𝑒if1≤G⁡s1G⁡s+if1≤F⁡t1F⁡t2=2⁢if1≤G⁡s1G⁡s+if1≤F⁡t1F⁡t2
80 48 50 rexaddd ⊢φ∧s∈S∧t∈T→if1≤G⁡s1G⁡s+𝑒if1≤F⁡t1F⁡t=if1≤G⁡s1G⁡s+if1≤F⁡t1F⁡t
81 75 79 80 3eqtr4d ⊢φ∧s∈S∧t∈T→2⋅𝑒if1≤G⁡s1G⁡s+if1≤F⁡t1F⁡t2=if1≤G⁡s1G⁡s+𝑒if1≤F⁡t1F⁡t
82 x2times ⊢sDt∈ℝ*→2⋅𝑒sDt=sDt+𝑒sDt
83 69 82 syl ⊢φ∧s∈S∧t∈T→2⋅𝑒sDt=sDt+𝑒sDt
84 72 81 83 3brtr4d ⊢φ∧s∈S∧t∈T→2⋅𝑒if1≤G⁡s1G⁡s+if1≤F⁡t1F⁡t2≤2⋅𝑒sDt
85 77 rexrd ⊢φ∧s∈S∧t∈T→if1≤G⁡s1G⁡s+if1≤F⁡t1F⁡t2∈ℝ*
86 2rp ⊢2∈ℝ+
87 86 a1i ⊢φ∧s∈S∧t∈T→2∈ℝ+
88 xlemul2 ⊢if1≤G⁡s1G⁡s+if1≤F⁡t1F⁡t2∈ℝ*∧sDt∈ℝ*∧2∈ℝ+→if1≤G⁡s1G⁡s+if1≤F⁡t1F⁡t2≤sDt↔2⋅𝑒if1≤G⁡s1G⁡s+if1≤F⁡t1F⁡t2≤2⋅𝑒sDt
89 85 69 87 88 syl3anc ⊢φ∧s∈S∧t∈T→if1≤G⁡s1G⁡s+if1≤F⁡t1F⁡t2≤sDt↔2⋅𝑒if1≤G⁡s1G⁡s+if1≤F⁡t1F⁡t2≤2⋅𝑒sDt
90 84 89 mpbird ⊢φ∧s∈S∧t∈T→if1≤G⁡s1G⁡s+if1≤F⁡t1F⁡t2≤sDt
91 59 90 eqbrtrd ⊢φ∧s∈S∧t∈T→if1≤G⁡s1G⁡s2+𝑒if1≤F⁡t1F⁡t2≤sDt
92 bldisj ⊢D∈∞Met⁡X∧s∈X∧t∈X∧if1≤G⁡s1G⁡s2∈ℝ*∧if1≤F⁡t1F⁡t2∈ℝ*∧if1≤G⁡s1G⁡s2+𝑒if1≤F⁡t1F⁡t2≤sDt→sball⁡Dif1≤G⁡s1G⁡s2∩tball⁡Dif1≤F⁡t1F⁡t2=∅
93 24 32 37 42 47 91 92 syl33anc ⊢φ∧s∈S∧t∈T→sball⁡Dif1≤G⁡s1G⁡s2∩tball⁡Dif1≤F⁡t1F⁡t2=∅
94 eqimss ⊢sball⁡Dif1≤G⁡s1G⁡s2∩tball⁡Dif1≤F⁡t1F⁡t2=∅→sball⁡Dif1≤G⁡s1G⁡s2∩tball⁡Dif1≤F⁡t1F⁡t2⊆∅
95 93 94 syl ⊢φ∧s∈S∧t∈T→sball⁡Dif1≤G⁡s1G⁡s2∩tball⁡Dif1≤F⁡t1F⁡t2⊆∅
96 95 anassrs ⊢φ∧s∈S∧t∈T→sball⁡Dif1≤G⁡s1G⁡s2∩tball⁡Dif1≤F⁡t1F⁡t2⊆∅
97 96 ralrimiva ⊢φ∧s∈S→∀t∈Tsball⁡Dif1≤G⁡s1G⁡s2∩tball⁡Dif1≤F⁡t1F⁡t2⊆∅
98 iunss ⊢⋃t∈Tsball⁡Dif1≤G⁡s1G⁡s2∩tball⁡Dif1≤F⁡t1F⁡t2⊆∅↔∀t∈Tsball⁡Dif1≤G⁡s1G⁡s2∩tball⁡Dif1≤F⁡t1F⁡t2⊆∅
99 97 98 sylibr ⊢φ∧s∈S→⋃t∈Tsball⁡Dif1≤G⁡s1G⁡s2∩tball⁡Dif1≤F⁡t1F⁡t2⊆∅
100 23 99 eqsstrid ⊢φ∧s∈S→sball⁡Dif1≤G⁡s1G⁡s2∩U⊆∅
101 100 ralrimiva ⊢φ→∀s∈Ssball⁡Dif1≤G⁡s1G⁡s2∩U⊆∅
102 iunss ⊢⋃s∈Ssball⁡Dif1≤G⁡s1G⁡s2∩U⊆∅↔∀s∈Ssball⁡Dif1≤G⁡s1G⁡s2∩U⊆∅
103 101 102 sylibr ⊢φ→⋃s∈Ssball⁡Dif1≤G⁡s1G⁡s2∩U⊆∅
104 ss0 ⊢⋃s∈Ssball⁡Dif1≤G⁡s1G⁡s2∩U⊆∅→⋃s∈Ssball⁡Dif1≤G⁡s1G⁡s2∩U=∅
105 103 104 syl ⊢φ→⋃s∈Ssball⁡Dif1≤G⁡s1G⁡s2∩U=∅
106 20 105 eqtrid ⊢φ→V∩U=∅
107 sseq2 ⊢z=V→S⊆z↔S⊆V
108 ineq1 ⊢z=V→z∩w=V∩w
109 108 eqeq1d ⊢z=V→z∩w=∅↔V∩w=∅
110 107 109 3anbi13d ⊢z=V→S⊆z∧T⊆w∧z∩w=∅↔S⊆V∧T⊆w∧V∩w=∅
111 sseq2 ⊢w=U→T⊆w↔T⊆U
112 ineq2 ⊢w=U→V∩w=V∩U
113 112 eqeq1d ⊢w=U→V∩w=∅↔V∩U=∅
114 111 113 3anbi23d ⊢w=U→S⊆V∧T⊆w∧V∩w=∅↔S⊆V∧T⊆U∧V∩U=∅
115 110 114 rspc2ev ⊢V∈J∧U∈J∧S⊆V∧T⊆U∧V∩U=∅→∃z∈J∃w∈JS⊆z∧T⊆w∧z∩w=∅
116 13 15 16 17 106 115 syl113anc ⊢φ→∃z∈J∃w∈JS⊆z∧T⊆w∧z∩w=∅