Theorem minvecolem6

Description: Lemma for minveco . Any minimal point is less than S away from A . (Contributed by Mario Carneiro, 9-May-2014) (Revised by AV, 4-Oct-2020) (New usage is discouraged.)

	Ref	Expression
Hypotheses	minveco.x	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
	minveco.m	⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
	minveco.n	⊢ 𝑁 = ( normCV ‘ 𝑈 )
	minveco.y	⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
	minveco.u	⊢ ( 𝜑 → 𝑈 ∈ CPreHilOLD )
	minveco.w	⊢ ( 𝜑 → 𝑊 ∈ ( ( SubSp ‘ 𝑈 ) ∩ CBan ) )
	minveco.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
	minveco.d	⊢ 𝐷 = ( IndMet ‘ 𝑈 )
	minveco.j	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
	minveco.r	⊢ 𝑅 = ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )
	minveco.s	⊢ 𝑆 = inf ( 𝑅 , ℝ , < )
Assertion	minvecolem6	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( ( ( 𝐴 𝐷 𝑥 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ↔ ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		minveco.x	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		minveco.m	⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
3		minveco.n	⊢ 𝑁 = ( normCV ‘ 𝑈 )
4		minveco.y	⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
5		minveco.u	⊢ ( 𝜑 → 𝑈 ∈ CPreHilOLD )
6		minveco.w	⊢ ( 𝜑 → 𝑊 ∈ ( ( SubSp ‘ 𝑈 ) ∩ CBan ) )
7		minveco.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
8		minveco.d	⊢ 𝐷 = ( IndMet ‘ 𝑈 )
9		minveco.j	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
10		minveco.r	⊢ 𝑅 = ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )
11		minveco.s	⊢ 𝑆 = inf ( 𝑅 , ℝ , < )
12		phnv	⊢ ( 𝑈 ∈ CPreHilOLD → 𝑈 ∈ NrmCVec )
13	5 12	syl	⊢ ( 𝜑 → 𝑈 ∈ NrmCVec )
14	13	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → 𝑈 ∈ NrmCVec )
15	7	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → 𝐴 ∈ 𝑋 )
16		inss1	⊢ ( ( SubSp ‘ 𝑈 ) ∩ CBan ) ⊆ ( SubSp ‘ 𝑈 )
17	16 6	sseldi	⊢ ( 𝜑 → 𝑊 ∈ ( SubSp ‘ 𝑈 ) )
18		eqid	⊢ ( SubSp ‘ 𝑈 ) = ( SubSp ‘ 𝑈 )
19	1 4 18	sspba	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ ( SubSp ‘ 𝑈 ) ) → 𝑌 ⊆ 𝑋 )
20	13 17 19	syl2anc	⊢ ( 𝜑 → 𝑌 ⊆ 𝑋 )
21	20	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → 𝑥 ∈ 𝑋 )
22	1 2 3 8	imsdval	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐴 𝐷 𝑥 ) = ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) )
23	14 15 21 22	syl3anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( 𝐴 𝐷 𝑥 ) = ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) )
24	23	oveq1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( ( 𝐴 𝐷 𝑥 ) ↑ 2 ) = ( ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ↑ 2 ) )
25	1 2 3 4 5 6 7 8 9 10	minvecolem1	⊢ ( 𝜑 → ( 𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) )
26	25	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( 𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) )
27	26	simp1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → 𝑅 ⊆ ℝ )
28	26	simp2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → 𝑅 ≠ ∅ )
29		0red	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → 0 ∈ ℝ )
30	26	simp3d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 )
31		breq1	⊢ ( 𝑥 = 0 → ( 𝑥 ≤ 𝑤 ↔ 0 ≤ 𝑤 ) )
32	31	ralbidv	⊢ ( 𝑥 = 0 → ( ∀ 𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ↔ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) )
33	32	rspcev	⊢ ( ( 0 ∈ ℝ ∧ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 )
34	29 30 33	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 )
35		infrecl	⊢ ( ( 𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ) → inf ( 𝑅 , ℝ , < ) ∈ ℝ )
36	27 28 34 35	syl3anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → inf ( 𝑅 , ℝ , < ) ∈ ℝ )
37	11 36	eqeltrid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → 𝑆 ∈ ℝ )
38	37	resqcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( 𝑆 ↑ 2 ) ∈ ℝ )
39	38	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( 𝑆 ↑ 2 ) ∈ ℂ )
40	39	addid1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( ( 𝑆 ↑ 2 ) + 0 ) = ( 𝑆 ↑ 2 ) )
41	24 40	breq12d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( ( ( 𝐴 𝐷 𝑥 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ↔ ( ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ↑ 2 ) ≤ ( 𝑆 ↑ 2 ) ) )
42	1 2	nvmcl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐴 𝑀 𝑥 ) ∈ 𝑋 )
43	14 15 21 42	syl3anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( 𝐴 𝑀 𝑥 ) ∈ 𝑋 )
44	1 3	nvcl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 𝑀 𝑥 ) ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ∈ ℝ )
45	14 43 44	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ∈ ℝ )
46	1 3	nvge0	⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 𝑀 𝑥 ) ∈ 𝑋 ) → 0 ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) )
47	14 43 46	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → 0 ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) )
48		infregelb	⊢ ( ( ( 𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ) ∧ 0 ∈ ℝ ) → ( 0 ≤ inf ( 𝑅 , ℝ , < ) ↔ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) )
49	27 28 34 29 48	syl31anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( 0 ≤ inf ( 𝑅 , ℝ , < ) ↔ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) )
50	30 49	mpbird	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → 0 ≤ inf ( 𝑅 , ℝ , < ) )
51	50 11	breqtrrdi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → 0 ≤ 𝑆 )
52	45 37 47 51	le2sqd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ 𝑆 ↔ ( ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ↑ 2 ) ≤ ( 𝑆 ↑ 2 ) ) )
53	11	breq2i	⊢ ( ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ 𝑆 ↔ ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ inf ( 𝑅 , ℝ , < ) )
54		infregelb	⊢ ( ( ( 𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ) ∧ ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ∈ ℝ ) → ( ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ inf ( 𝑅 , ℝ , < ) ↔ ∀ 𝑤 ∈ 𝑅 ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ 𝑤 ) )
55	27 28 34 45 54	syl31anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ inf ( 𝑅 , ℝ , < ) ↔ ∀ 𝑤 ∈ 𝑅 ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ 𝑤 ) )
56	53 55	syl5bb	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ 𝑆 ↔ ∀ 𝑤 ∈ 𝑅 ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ 𝑤 ) )
57	41 52 56	3bitr2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( ( ( 𝐴 𝐷 𝑥 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ↔ ∀ 𝑤 ∈ 𝑅 ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ 𝑤 ) )
58	10	raleqi	⊢ ( ∀ 𝑤 ∈ 𝑅 ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ 𝑤 ↔ ∀ 𝑤 ∈ ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ 𝑤 )
59		fvex	⊢ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ∈ V
60	59	rgenw	⊢ ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ∈ V
61		eqid	⊢ ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) = ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )
62		breq2	⊢ ( 𝑤 = ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) → ( ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ 𝑤 ↔ ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) )
63	61 62	ralrnmptw	⊢ ( ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ∈ V → ( ∀ 𝑤 ∈ ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ 𝑤 ↔ ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) )
64	60 63	ax-mp	⊢ ( ∀ 𝑤 ∈ ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ 𝑤 ↔ ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )
65	58 64	bitri	⊢ ( ∀ 𝑤 ∈ 𝑅 ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ 𝑤 ↔ ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )
66	57 65	bitrdi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( ( ( 𝐴 𝐷 𝑥 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ↔ ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) )