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	ffvelrnd	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → ( 𝐹 ‘ 𝐵 ) ∈ ( 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	xaddid1d	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → ( ( 𝐴 𝐷 𝐵 ) +𝑒 0 ) = ( 𝐴 𝐷 𝐵 ) )
43	41 42	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → ( ( 𝐵 𝐷 𝐴 ) +𝑒 ( 𝐹 ‘ 𝐴 ) ) = ( 𝐴 𝐷 𝐵 ) )
44	36 43	breqtrd	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → ( 𝐹 ‘ 𝐵 ) ≤ ( 𝐴 𝐷 𝐵 ) )
45	28 26 32 34 44	xrletrd	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → if ( 1 ≤ ( 𝐹 ‘ 𝐵 ) , 1 , ( 𝐹 ‘ 𝐵 ) ) ≤ ( 𝐴 𝐷 𝐵 ) )