minveclem1 - Metamath Proof Explorer

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

Theorem minveclem1 22866

Description: Lemma for minvec 22878. The set of all distances from points of 𝑌 to 𝐴 are a nonempty set of nonnegative reals. (Contributed by Mario Carneiro, 8-May-2014.) (Revised by Mario Carneiro, 15-Oct-2015.)

**Hypotheses**
Ref	Expression
minvec.x	⊢ 𝑋 = (Base‘𝑈)
minvec.m	⊢ − = (-_g‘𝑈)
minvec.n	⊢ 𝑁 = (norm‘𝑈)
minvec.u	⊢ (𝜑 → 𝑈 ∈ ℂPreHil)
minvec.y	⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈))
minvec.w	⊢ (𝜑 → (𝑈 ↾_s 𝑌) ∈ CMetSp)
minvec.a	⊢ (𝜑 → 𝐴 ∈ 𝑋)
minvec.j	⊢ 𝐽 = (TopOpen‘𝑈)
minvec.r	⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))

**Assertion**
Ref	Expression
minveclem1	⊢ (𝜑 → (𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤))

Distinct variable groups: 𝑦,𝑤, − 𝑤,𝐴,𝑦 𝑤,𝐽,𝑦 𝑤,𝑁,𝑦 𝜑,𝑤,𝑦 𝑤,𝑅,𝑦 𝑤,𝑈,𝑦 𝑤,𝑋,𝑦 𝑤,𝑌,𝑦

**Proof of Theorem minveclem1**
Step	Hyp	Ref	Expression
1		minvec.r	. . 3 ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))
2		minvec.u	. . . . . . . 8 ⊢ (𝜑 → 𝑈 ∈ ℂPreHil)
3		cphngp 22651	. . . . . . . 8 ⊢ (𝑈 ∈ ℂPreHil → 𝑈 ∈ NrmGrp)
4	2, 3	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑈 ∈ NrmGrp)
5	4	adantr 479	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑈 ∈ NrmGrp)
6		cphlmod 22652	. . . . . . . . 9 ⊢ (𝑈 ∈ ℂPreHil → 𝑈 ∈ LMod)
7	2, 6	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑈 ∈ LMod)
8	7	adantr 479	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑈 ∈ LMod)
9		minvec.a	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ 𝑋)
10	9	adantr 479	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝐴 ∈ 𝑋)
11		minvec.y	. . . . . . . . 9 ⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈))
12		minvec.x	. . . . . . . . . 10 ⊢ 𝑋 = (Base‘𝑈)
13		eqid 2514	. . . . . . . . . 10 ⊢ (LSubSp‘𝑈) = (LSubSp‘𝑈)
14	12, 13	lssss 18662	. . . . . . . . 9 ⊢ (𝑌 ∈ (LSubSp‘𝑈) → 𝑌 ⊆ 𝑋)
15	11, 14	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ⊆ 𝑋)
16	15	sselda 3472	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝑋)
17		minvec.m	. . . . . . . 8 ⊢ − = (-_g‘𝑈)
18	12, 17	lmodvsubcl 18635	. . . . . . 7 ⊢ ((𝑈 ∈ LMod ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐴 − 𝑦) ∈ 𝑋)
19	8, 10, 16, 18	syl3anc 1317	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝐴 − 𝑦) ∈ 𝑋)
20		minvec.n	. . . . . . 7 ⊢ 𝑁 = (norm‘𝑈)
21	12, 20	nmcl 22131	. . . . . 6 ⊢ ((𝑈 ∈ NrmGrp ∧ (𝐴 − 𝑦) ∈ 𝑋) → (𝑁‘(𝐴 − 𝑦)) ∈ ℝ)
22	5, 19, 21	syl2anc 690	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝑁‘(𝐴 − 𝑦)) ∈ ℝ)
23		eqid 2514	. . . . 5 ⊢ (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦))) = (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))
24	22, 23	fmptd 6176	. . . 4 ⊢ (𝜑 → (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦))):𝑌⟶ℝ)
25		frn 5851	. . . 4 ⊢ ((𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦))):𝑌⟶ℝ → ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦))) ⊆ ℝ)
26	24, 25	syl 17	. . 3 ⊢ (𝜑 → ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦))) ⊆ ℝ)
27	1, 26	syl5eqss 3516	. 2 ⊢ (𝜑 → 𝑅 ⊆ ℝ)
28	13	lssn0 18666	. . . 4 ⊢ (𝑌 ∈ (LSubSp‘𝑈) → 𝑌 ≠ ∅)
29	11, 28	syl 17	. . 3 ⊢ (𝜑 → 𝑌 ≠ ∅)
30	1	eqeq1i 2519	. . . . 5 ⊢ (𝑅 = ∅ ↔ ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦))) = ∅)
31		dm0rn0 5154	. . . . 5 ⊢ (dom (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦))) = ∅ ↔ ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦))) = ∅)
32		fvex 5997	. . . . . . 7 ⊢ (𝑁‘(𝐴 − 𝑦)) ∈ V
33	32, 23	dmmpti 5821	. . . . . 6 ⊢ dom (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦))) = 𝑌
34	33	eqeq1i 2519	. . . . 5 ⊢ (dom (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦))) = ∅ ↔ 𝑌 = ∅)
35	30, 31, 34	3bitr2i 286	. . . 4 ⊢ (𝑅 = ∅ ↔ 𝑌 = ∅)
36	35	necon3bii 2738	. . 3 ⊢ (𝑅 ≠ ∅ ↔ 𝑌 ≠ ∅)
37	29, 36	sylibr 222	. 2 ⊢ (𝜑 → 𝑅 ≠ ∅)
38	12, 20	nmge0 22132	. . . . . 6 ⊢ ((𝑈 ∈ NrmGrp ∧ (𝐴 − 𝑦) ∈ 𝑋) → 0 ≤ (𝑁‘(𝐴 − 𝑦)))
39	5, 19, 38	syl2anc 690	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 0 ≤ (𝑁‘(𝐴 − 𝑦)))
40	39	ralrimiva 2853	. . . 4 ⊢ (𝜑 → ∀𝑦 ∈ 𝑌 0 ≤ (𝑁‘(𝐴 − 𝑦)))
41	32	rgenw 2812	. . . . 5 ⊢ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑦)) ∈ V
42		breq2 4485	. . . . . 6 ⊢ (𝑤 = (𝑁‘(𝐴 − 𝑦)) → (0 ≤ 𝑤 ↔ 0 ≤ (𝑁‘(𝐴 − 𝑦))))
43	23, 42	ralrnmpt 6160	. . . . 5 ⊢ (∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑦)) ∈ V → (∀𝑤 ∈ ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))0 ≤ 𝑤 ↔ ∀𝑦 ∈ 𝑌 0 ≤ (𝑁‘(𝐴 − 𝑦))))
44	41, 43	ax-mp 5	. . . 4 ⊢ (∀𝑤 ∈ ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))0 ≤ 𝑤 ↔ ∀𝑦 ∈ 𝑌 0 ≤ (𝑁‘(𝐴 − 𝑦)))
45	40, 44	sylibr 222	. . 3 ⊢ (𝜑 → ∀𝑤 ∈ ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))0 ≤ 𝑤)
46	1	raleqi 3023	. . 3 ⊢ (∀𝑤 ∈ 𝑅 0 ≤ 𝑤 ↔ ∀𝑤 ∈ ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))0 ≤ 𝑤)
47	45, 46	sylibr 222	. 2 ⊢ (𝜑 → ∀𝑤 ∈ 𝑅 0 ≤ 𝑤)
48	27, 37, 47	3jca 1234	1 ⊢ (𝜑 → (𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 194 ∧ wa 382 ∧ w3a 1030 = wceq 1474 ∈ wcel 1938 ≠ wne 2684 ∀wral 2800 Vcvv 3077 ⊆ wss 3444 ∅c0 3777 class class class wbr 4481 ↦ cmpt 4541 dom cdm 4932 ran crn 4933 ⟶wf 5685 ‘cfv 5689 (class class class)co 6426 ℝcr 9690 0cc0 9691 ≤ cle 9830 Basecbs 15579 ↾_s cress 15580 TopOpenctopn 15789 -_gcsg 17139 LModclmod 18593 LSubSpclss 18657 normcnm 22093 NrmGrpcngp 22094 ℂPreHilccph 22644 CMetSpccms 22800

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1700 ax-4 1713 ax-5 1793 ax-6 1838 ax-7 1885 ax-8 1940 ax-9 1947 ax-10 1966 ax-11 1971 ax-12 1983 ax-13 2137 ax-ext 2494 ax-rep 4597 ax-sep 4607 ax-nul 4616 ax-pow 4668 ax-pr 4732 ax-un 6723 ax-cnex 9747 ax-resscn 9748 ax-1cn 9749 ax-icn 9750 ax-addcl 9751 ax-addrcl 9752 ax-mulcl 9753 ax-mulrcl 9754 ax-mulcom 9755 ax-addass 9756 ax-mulass 9757 ax-distr 9758 ax-i2m1 9759 ax-1ne0 9760 ax-1rid 9761 ax-rnegex 9762 ax-rrecex 9763 ax-cnre 9764 ax-pre-lttri 9765 ax-pre-lttrn 9766 ax-pre-ltadd 9767 ax-pre-mulgt0 9768 ax-pre-sup 9769

This theorem depends on definitions: df-bi 195 df-or 383 df-an 384 df-3or 1031 df-3an 1032 df-tru 1477 df-ex 1695 df-nf 1699 df-sb 1831 df-eu 2366 df-mo 2367 df-clab 2501 df-cleq 2507 df-clel 2510 df-nfc 2644 df-ne 2686 df-nel 2687 df-ral 2805 df-rex 2806 df-reu 2807 df-rmo 2808 df-rab 2809 df-v 3079 df-sbc 3307 df-csb 3404 df-dif 3447 df-un 3449 df-in 3451 df-ss 3458 df-pss 3460 df-nul 3778 df-if 3940 df-pw 4013 df-sn 4029 df-pr 4031 df-tp 4033 df-op 4035 df-uni 4271 df-iun 4355 df-br 4482 df-opab 4542 df-mpt 4543 df-tr 4579 df-eprel 4843 df-id 4847 df-po 4853 df-so 4854 df-fr 4891 df-we 4893 df-xp 4938 df-rel 4939 df-cnv 4940 df-co 4941 df-dm 4942 df-rn 4943 df-res 4944 df-ima 4945 df-pred 5487 df-ord 5533 df-on 5534 df-lim 5535 df-suc 5536 df-iota 5653 df-fun 5691 df-fn 5692 df-f 5693 df-f1 5694 df-fo 5695 df-f1o 5696 df-fv 5697 df-riota 6388 df-ov 6429 df-oprab 6430 df-mpt2 6431 df-om 6834 df-1st 6934 df-2nd 6935 df-wrecs 7169 df-recs 7231 df-rdg 7269 df-er 7505 df-map 7622 df-en 7718 df-dom 7719 df-sdom 7720 df-sup 8107 df-inf 8108 df-pnf 9831 df-mnf 9832 df-xr 9833 df-ltxr 9834 df-le 9835 df-sub 10019 df-neg 10020 df-div 10434 df-nn 10776 df-2 10834 df-n0 11048 df-z 11119 df-uz 11428 df-q 11531 df-rp 11575 df-xneg 11688 df-xadd 11689 df-xmul 11690 df-0g 15809 df-topgen 15811 df-mgm 16957 df-sgrp 16999 df-mnd 17010 df-grp 17140 df-minusg 17141 df-sbg 17142 df-lmod 18595 df-lss 18658 df-psmet 19463 df-xmet 19464 df-met 19465 df-bl 19466 df-mopn 19467 df-top 20424 df-bases 20425 df-topon 20426 df-topsp 20427 df-xms 21837 df-ms 21838 df-nm 22099 df-ngp 22100 df-nlm 22103 df-cph 22646

This theorem is referenced by: minveclem4c 22867 minveclem2 22868 minveclem3b 22870 minveclem4 22874 minveclem6 22876 minveclem4cOLD 22879 minveclem2OLD 22880 minveclem3bOLD 22882 minveclem4OLD 22886 minveclem6OLD 22888

W3C validator