metdscnlem - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > metdscnlem		Structured version Visualization version GIF version

Theorem metdscnlem 23150

Description: Lemma for metdscn 23151. (Contributed by Mario Carneiro, 4-Sep-2015.)

**Hypotheses**
Ref	Expression
metdscn.f	⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ inf(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ^*, < ))
metdscn.j	⊢ 𝐽 = (MetOpen‘𝐷)
metdscn.c	⊢ 𝐶 = (dist‘ℝ^*_𝑠)
metdscn.k	⊢ 𝐾 = (MetOpen‘𝐶)
metdscnlem.1	⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))
metdscnlem.2	⊢ (𝜑 → 𝑆 ⊆ 𝑋)
metdscnlem.3	⊢ (𝜑 → 𝐴 ∈ 𝑋)
metdscnlem.4	⊢ (𝜑 → 𝐵 ∈ 𝑋)
metdscnlem.5	⊢ (𝜑 → 𝑅 ∈ ℝ⁺)
metdscnlem.6	⊢ (𝜑 → (𝐴𝐷𝐵) < 𝑅)

**Assertion**
Ref	Expression
metdscnlem	⊢ (𝜑 → ((𝐹‘𝐴) +_𝑒 -_𝑒(𝐹‘𝐵)) < 𝑅)

Distinct variable groups: 𝑥,𝑦,𝐴 𝑥,𝐷,𝑦 𝑦,𝐽 𝑥,𝐵,𝑦 𝑥,𝑆,𝑦 𝑥,𝑋,𝑦 Allowed substitution hints: 𝜑(𝑥,𝑦) 𝐶(𝑥,𝑦) 𝑅(𝑥,𝑦) 𝐹(𝑥,𝑦) 𝐽(𝑥) 𝐾(𝑥,𝑦)

**Proof of Theorem metdscnlem**
Step	Hyp	Ref	Expression
1		metdscnlem.1	. . . . . 6 ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))
2		metdscnlem.2	. . . . . 6 ⊢ (𝜑 → 𝑆 ⊆ 𝑋)
3		metdscn.f	. . . . . . 7 ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ inf(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ^*, < ))
4	3	metdsf 23143	. . . . . 6 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) → 𝐹:𝑋⟶(0[,]+∞))
5	1, 2, 4	syl2anc 584	. . . . 5 ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞))
6		metdscnlem.3	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ 𝑋)
7	5, 6	ffvelrnd 6724	. . . 4 ⊢ (𝜑 → (𝐹‘𝐴) ∈ (0[,]+∞))
8		eliccxr 12677	. . . 4 ⊢ ((𝐹‘𝐴) ∈ (0[,]+∞) → (𝐹‘𝐴) ∈ ℝ^*)
9	7, 8	syl 17	. . 3 ⊢ (𝜑 → (𝐹‘𝐴) ∈ ℝ^*)
10		metdscnlem.4	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ 𝑋)
11	5, 10	ffvelrnd 6724	. . . . 5 ⊢ (𝜑 → (𝐹‘𝐵) ∈ (0[,]+∞))
12		eliccxr 12677	. . . . 5 ⊢ ((𝐹‘𝐵) ∈ (0[,]+∞) → (𝐹‘𝐵) ∈ ℝ^*)
13	11, 12	syl 17	. . . 4 ⊢ (𝜑 → (𝐹‘𝐵) ∈ ℝ^*)
14	13	xnegcld 12547	. . 3 ⊢ (𝜑 → -_𝑒(𝐹‘𝐵) ∈ ℝ^*)
15	9, 14	xaddcld 12548	. 2 ⊢ (𝜑 → ((𝐹‘𝐴) +_𝑒 -_𝑒(𝐹‘𝐵)) ∈ ℝ^*)
16		xmetcl 22628	. . 3 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) ∈ ℝ^*)
17	1, 6, 10, 16	syl3anc 1364	. 2 ⊢ (𝜑 → (𝐴𝐷𝐵) ∈ ℝ^*)
18		metdscnlem.5	. . 3 ⊢ (𝜑 → 𝑅 ∈ ℝ⁺)
19	18	rpxrd 12286	. 2 ⊢ (𝜑 → 𝑅 ∈ ℝ^*)
20	3	metdstri 23146	. . . 4 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘𝐴) ≤ ((𝐴𝐷𝐵) +_𝑒 (𝐹‘𝐵)))
21	1, 2, 6, 10, 20	syl22anc 835	. . 3 ⊢ (𝜑 → (𝐹‘𝐴) ≤ ((𝐴𝐷𝐵) +_𝑒 (𝐹‘𝐵)))
22		elxrge0 12699	. . . . . 6 ⊢ ((𝐹‘𝐴) ∈ (0[,]+∞) ↔ ((𝐹‘𝐴) ∈ ℝ^* ∧ 0 ≤ (𝐹‘𝐴)))
23	22	simprbi 497	. . . . 5 ⊢ ((𝐹‘𝐴) ∈ (0[,]+∞) → 0 ≤ (𝐹‘𝐴))
24	7, 23	syl 17	. . . 4 ⊢ (𝜑 → 0 ≤ (𝐹‘𝐴))
25		elxrge0 12699	. . . . . . 7 ⊢ ((𝐹‘𝐵) ∈ (0[,]+∞) ↔ ((𝐹‘𝐵) ∈ ℝ^* ∧ 0 ≤ (𝐹‘𝐵)))
26	25	simprbi 497	. . . . . 6 ⊢ ((𝐹‘𝐵) ∈ (0[,]+∞) → 0 ≤ (𝐹‘𝐵))
27	11, 26	syl 17	. . . . 5 ⊢ (𝜑 → 0 ≤ (𝐹‘𝐵))
28		ge0nemnf 12420	. . . . 5 ⊢ (((𝐹‘𝐵) ∈ ℝ^* ∧ 0 ≤ (𝐹‘𝐵)) → (𝐹‘𝐵) ≠ -∞)
29	13, 27, 28	syl2anc 584	. . . 4 ⊢ (𝜑 → (𝐹‘𝐵) ≠ -∞)
30		xmetge0 22641	. . . . 5 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 0 ≤ (𝐴𝐷𝐵))
31	1, 6, 10, 30	syl3anc 1364	. . . 4 ⊢ (𝜑 → 0 ≤ (𝐴𝐷𝐵))
32		xlesubadd 12510	. . . 4 ⊢ ((((𝐹‘𝐴) ∈ ℝ^* ∧ (𝐹‘𝐵) ∈ ℝ^* ∧ (𝐴𝐷𝐵) ∈ ℝ^*) ∧ (0 ≤ (𝐹‘𝐴) ∧ (𝐹‘𝐵) ≠ -∞ ∧ 0 ≤ (𝐴𝐷𝐵))) → (((𝐹‘𝐴) +_𝑒 -_𝑒(𝐹‘𝐵)) ≤ (𝐴𝐷𝐵) ↔ (𝐹‘𝐴) ≤ ((𝐴𝐷𝐵) +_𝑒 (𝐹‘𝐵))))
33	9, 13, 17, 24, 29, 31, 32	syl33anc 1378	. . 3 ⊢ (𝜑 → (((𝐹‘𝐴) +_𝑒 -_𝑒(𝐹‘𝐵)) ≤ (𝐴𝐷𝐵) ↔ (𝐹‘𝐴) ≤ ((𝐴𝐷𝐵) +_𝑒 (𝐹‘𝐵))))
34	21, 33	mpbird 258	. 2 ⊢ (𝜑 → ((𝐹‘𝐴) +_𝑒 -_𝑒(𝐹‘𝐵)) ≤ (𝐴𝐷𝐵))
35		metdscnlem.6	. 2 ⊢ (𝜑 → (𝐴𝐷𝐵) < 𝑅)
36	15, 17, 19, 34, 35	xrlelttrd 12407	1 ⊢ (𝜑 → ((𝐹‘𝐴) +_𝑒 -_𝑒(𝐹‘𝐵)) < 𝑅)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 207 = wceq 1525 ∈ wcel 2083 ≠ wne 2986 ⊆ wss 3865 class class class wbr 4968 ↦ cmpt 5047 ran crn 5451 ⟶wf 6228 ‘cfv 6232 (class class class)co 7023 infcinf 8758 0cc0 10390 +∞cpnf 10525 -∞cmnf 10526 ℝ^*cxr 10527 < clt 10528 ≤ cle 10529 ℝ⁺crp 12243 -_𝑒cxne 12358 +_𝑒 cxad 12359 [,]cicc 12595 distcds 16407 ℝ^*_𝑠cxrs 16606 ∞Metcxmet 20216 MetOpencmopn 20221

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1781 ax-4 1795 ax-5 1892 ax-6 1951 ax-7 1996 ax-8 2085 ax-9 2093 ax-10 2114 ax-11 2128 ax-12 2143 ax-13 2346 ax-ext 2771 ax-sep 5101 ax-nul 5108 ax-pow 5164 ax-pr 5228 ax-un 7326 ax-cnex 10446 ax-resscn 10447 ax-1cn 10448 ax-icn 10449 ax-addcl 10450 ax-addrcl 10451 ax-mulcl 10452 ax-mulrcl 10453 ax-mulcom 10454 ax-addass 10455 ax-mulass 10456 ax-distr 10457 ax-i2m1 10458 ax-1ne0 10459 ax-1rid 10460 ax-rnegex 10461 ax-rrecex 10462 ax-cnre 10463 ax-pre-lttri 10464 ax-pre-lttrn 10465 ax-pre-ltadd 10466 ax-pre-mulgt0 10467 ax-pre-sup 10468

This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3or 1081 df-3an 1082 df-tru 1528 df-ex 1766 df-nf 1770 df-sb 2045 df-mo 2578 df-eu 2614 df-clab 2778 df-cleq 2790 df-clel 2865 df-nfc 2937 df-ne 2987 df-nel 3093 df-ral 3112 df-rex 3113 df-reu 3114 df-rmo 3115 df-rab 3116 df-v 3442 df-sbc 3712 df-csb 3818 df-dif 3868 df-un 3870 df-in 3872 df-ss 3880 df-nul 4218 df-if 4388 df-pw 4461 df-sn 4479 df-pr 4481 df-op 4485 df-uni 4752 df-iun 4833 df-br 4969 df-opab 5031 df-mpt 5048 df-id 5355 df-po 5369 df-so 5370 df-xp 5456 df-rel 5457 df-cnv 5458 df-co 5459 df-dm 5460 df-rn 5461 df-res 5462 df-ima 5463 df-iota 6196 df-fun 6234 df-fn 6235 df-f 6236 df-f1 6237 df-fo 6238 df-f1o 6239 df-fv 6240 df-riota 6984 df-ov 7026 df-oprab 7027 df-mpo 7028 df-1st 7552 df-2nd 7553 df-er 8146 df-ec 8148 df-map 8265 df-en 8365 df-dom 8366 df-sdom 8367 df-sup 8759 df-inf 8760 df-pnf 10530 df-mnf 10531 df-xr 10532 df-ltxr 10533 df-le 10534 df-sub 10725 df-neg 10726 df-div 11152 df-2 11554 df-rp 12244 df-xneg 12361 df-xadd 12362 df-xmul 12363 df-icc 12599 df-psmet 20223 df-xmet 20224 df-bl 20226

This theorem is referenced by: metdscn 23151

W3C validator