Theorem minveclem1

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

	Ref	Expression
Hypotheses	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	minveclem1	⊢ ( 𝜑 → ( 𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) )

Proof

Step	Hyp	Ref	Expression
1		minvec.x	⊢ 𝑋 = ( Base ‘ 𝑈 )
2		minvec.m	⊢ − = ( -g ‘ 𝑈 )
3		minvec.n	⊢ 𝑁 = ( norm ‘ 𝑈 )
4		minvec.u	⊢ ( 𝜑 → 𝑈 ∈ ℂPreHil )
5		minvec.y	⊢ ( 𝜑 → 𝑌 ∈ ( LSubSp ‘ 𝑈 ) )
6		minvec.w	⊢ ( 𝜑 → ( 𝑈 ↾s 𝑌 ) ∈ CMetSp )
7		minvec.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
8		minvec.j	⊢ 𝐽 = ( TopOpen ‘ 𝑈 )
9		minvec.r	⊢ 𝑅 = ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) )
10		cphngp	⊢ ( 𝑈 ∈ ℂPreHil → 𝑈 ∈ NrmGrp )
11	4 10	syl	⊢ ( 𝜑 → 𝑈 ∈ NrmGrp )
12		cphlmod	⊢ ( 𝑈 ∈ ℂPreHil → 𝑈 ∈ LMod )
13	4 12	syl	⊢ ( 𝜑 → 𝑈 ∈ LMod )
14	13	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → 𝑈 ∈ LMod )
15	7	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → 𝐴 ∈ 𝑋 )
16		eqid	⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
17	1 16	lssss	⊢ ( 𝑌 ∈ ( LSubSp ‘ 𝑈 ) → 𝑌 ⊆ 𝑋 )
18	5 17	syl	⊢ ( 𝜑 → 𝑌 ⊆ 𝑋 )
19	18	sselda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → 𝑦 ∈ 𝑋 )
20	1 2	lmodvsubcl	⊢ ( ( 𝑈 ∈ LMod ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝐴 − 𝑦 ) ∈ 𝑋 )
21	14 15 19 20	syl3anc	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ( 𝐴 − 𝑦 ) ∈ 𝑋 )
22	1 3	nmcl	⊢ ( ( 𝑈 ∈ NrmGrp ∧ ( 𝐴 − 𝑦 ) ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ∈ ℝ )
23	11 21 22	syl2an2r	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ∈ ℝ )
24	23	fmpttd	⊢ ( 𝜑 → ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) : 𝑌 ⟶ ℝ )
25	24	frnd	⊢ ( 𝜑 → ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ⊆ ℝ )
26	9 25	eqsstrid	⊢ ( 𝜑 → 𝑅 ⊆ ℝ )
27	16	lssn0	⊢ ( 𝑌 ∈ ( LSubSp ‘ 𝑈 ) → 𝑌 ≠ ∅ )
28	5 27	syl	⊢ ( 𝜑 → 𝑌 ≠ ∅ )
29	9	eqeq1i	⊢ ( 𝑅 = ∅ ↔ ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) = ∅ )
30		dm0rn0	⊢ ( dom ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) = ∅ ↔ ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) = ∅ )
31		fvex	⊢ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ∈ V
32		eqid	⊢ ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) = ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) )
33	31 32	dmmpti	⊢ dom ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) = 𝑌
34	33	eqeq1i	⊢ ( dom ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) = ∅ ↔ 𝑌 = ∅ )
35	29 30 34	3bitr2i	⊢ ( 𝑅 = ∅ ↔ 𝑌 = ∅ )
36	35	necon3bii	⊢ ( 𝑅 ≠ ∅ ↔ 𝑌 ≠ ∅ )
37	28 36	sylibr	⊢ ( 𝜑 → 𝑅 ≠ ∅ )
38	1 3	nmge0	⊢ ( ( 𝑈 ∈ NrmGrp ∧ ( 𝐴 − 𝑦 ) ∈ 𝑋 ) → 0 ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) )
39	11 21 38	syl2an2r	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → 0 ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) )
40	39	ralrimiva	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝑌 0 ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) )
41	31	rgenw	⊢ ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ∈ V
42		breq2	⊢ ( 𝑤 = ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) → ( 0 ≤ 𝑤 ↔ 0 ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) )
43	32 42	ralrnmptw	⊢ ( ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ∈ V → ( ∀ 𝑤 ∈ ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) 0 ≤ 𝑤 ↔ ∀ 𝑦 ∈ 𝑌 0 ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) )
44	41 43	ax-mp	⊢ ( ∀ 𝑤 ∈ ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) 0 ≤ 𝑤 ↔ ∀ 𝑦 ∈ 𝑌 0 ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) )
45	40 44	sylibr	⊢ ( 𝜑 → ∀ 𝑤 ∈ ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) 0 ≤ 𝑤 )
46	9	raleqi	⊢ ( ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ↔ ∀ 𝑤 ∈ ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) 0 ≤ 𝑤 )
47	45 46	sylibr	⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 )
48	26 37 47	3jca	⊢ ( 𝜑 → ( 𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) )