minvecolem5

Description: Lemma for minveco . Discharge the assumption about the sequence F by applying countable choice ax-cc . (Contributed by Mario Carneiro, 9-May-2014) (Revised by AV, 4-Oct-2020) (New usage is discouraged.)

	Ref	Expression
Hypotheses	minveco.x	$⊢ X = BaseSet (U)$
	minveco.m	$⊢ M = -_{v} (U)$
	minveco.n	$⊢ N = {norm}_{CV} (U)$
	minveco.y	$⊢ Y = BaseSet (W)$
	minveco.u	$⊢ φ \to U \in {CPreHil}_{OLD}$
	minveco.w	$⊢ φ \to W \in (SubSp (U) \cap CBan)$
	minveco.a	$⊢ φ \to A \in X$
	minveco.d	$⊢ D = IndMet (U)$
	minveco.j	$⊢ J = MetOpen (D)$
	minveco.r	$⊢ R = ran (y \in Y ⟼ N (A M y))$
	minveco.s	$⊢ S = inf (R ℝ <)$
Assertion	minvecolem5	$⊢ φ \to \exists x \in Y \forall y \in Y N (A M x) \leq N (A M y)$

Proof

Step	Hyp	Ref	Expression
1		minveco.x	$⊢ X = BaseSet (U)$
2		minveco.m	$⊢ M = -_{v} (U)$
3		minveco.n	$⊢ N = {norm}_{CV} (U)$
4		minveco.y	$⊢ Y = BaseSet (W)$
5		minveco.u	$⊢ φ \to U \in {CPreHil}_{OLD}$
6		minveco.w	$⊢ φ \to W \in (SubSp (U) \cap CBan)$
7		minveco.a	$⊢ φ \to A \in X$
8		minveco.d	$⊢ D = IndMet (U)$
9		minveco.j	$⊢ J = MetOpen (D)$
10		minveco.r	$⊢ R = ran (y \in Y ⟼ N (A M y))$
11		minveco.s	$⊢ S = inf (R ℝ <)$
12		nnrecgt0	$⊢ n \in ℕ \to 0 < \frac{1}{n}$
13	12	adantl	$⊢ (φ \land n \in ℕ) \to 0 < \frac{1}{n}$
14		nnrecre	$⊢ n \in ℕ \to \frac{1}{n} \in ℝ$
15	14	adantl	$⊢ (φ \land n \in ℕ) \to \frac{1}{n} \in ℝ$
16	1 2 3 4 5 6 7 8 9 10	minvecolem1	$⊢ φ \to (R \subseteq ℝ \land R \neq \emptyset \land \forall w \in R 0 \leq w)$
17	16	adantr	$⊢ (φ \land n \in ℕ) \to (R \subseteq ℝ \land R \neq \emptyset \land \forall w \in R 0 \leq w)$
18	17	simp1d	$⊢ (φ \land n \in ℕ) \to R \subseteq ℝ$
19	17	simp2d	$⊢ (φ \land n \in ℕ) \to R \neq \emptyset$
20		0re	$⊢ 0 \in ℝ$
21	17	simp3d	$⊢ (φ \land n \in ℕ) \to \forall w \in R 0 \leq w$
22		breq1	$⊢ x = 0 \to (x \leq w \leftrightarrow 0 \leq w)$
23	22	ralbidv	$⊢ x = 0 \to (\forall w \in R x \leq w \leftrightarrow \forall w \in R 0 \leq w)$
24	23	rspcev	$⊢ (0 \in ℝ \land \forall w \in R 0 \leq w) \to \exists x \in ℝ \forall w \in R x \leq w$
25	20 21 24	sylancr	$⊢ (φ \land n \in ℕ) \to \exists x \in ℝ \forall w \in R x \leq w$
26		infrecl	$⊢ (R \subseteq ℝ \land R \neq \emptyset \land \exists x \in ℝ \forall w \in R x \leq w) \to inf (R ℝ <) \in ℝ$
27	18 19 25 26	syl3anc	$⊢ (φ \land n \in ℕ) \to inf (R ℝ <) \in ℝ$
28	11 27	eqeltrid	$⊢ (φ \land n \in ℕ) \to S \in ℝ$
29	28	resqcld	$⊢ (φ \land n \in ℕ) \to S^{2} \in ℝ$
30	15 29	ltaddposd	$⊢ (φ \land n \in ℕ) \to (0 < \frac{1}{n} \leftrightarrow S^{2} < S^{2} + (\frac{1}{n}))$
31	13 30	mpbid	$⊢ (φ \land n \in ℕ) \to S^{2} < S^{2} + (\frac{1}{n})$
32	29 15	readdcld	$⊢ (φ \land n \in ℕ) \to S^{2} + (\frac{1}{n}) \in ℝ$
33	28	sqge0d	$⊢ (φ \land n \in ℕ) \to 0 \leq S^{2}$
34	29 15 33 13	addgegt0d	$⊢ (φ \land n \in ℕ) \to 0 < S^{2} + (\frac{1}{n})$
35	32 34	elrpd	$⊢ (φ \land n \in ℕ) \to S^{2} + (\frac{1}{n}) \in ℝ^{+}$
36	35	rpge0d	$⊢ (φ \land n \in ℕ) \to 0 \leq S^{2} + (\frac{1}{n})$
37		resqrtth	$⊢ (S^{2} + (\frac{1}{n}) \in ℝ \land 0 \leq S^{2} + (\frac{1}{n})) \to {\sqrt{S^{2} + (\frac{1}{n})}}^{2} = S^{2} + (\frac{1}{n})$
38	32 36 37	syl2anc	$⊢ (φ \land n \in ℕ) \to {\sqrt{S^{2} + (\frac{1}{n})}}^{2} = S^{2} + (\frac{1}{n})$
39	31 38	breqtrrd	$⊢ (φ \land n \in ℕ) \to S^{2} < {\sqrt{S^{2} + (\frac{1}{n})}}^{2}$
40	35	rpsqrtcld	$⊢ (φ \land n \in ℕ) \to \sqrt{S^{2} + (\frac{1}{n})} \in ℝ^{+}$
41	40	rpred	$⊢ (φ \land n \in ℕ) \to \sqrt{S^{2} + (\frac{1}{n})} \in ℝ$
42		0red	$⊢ (φ \land n \in ℕ) \to 0 \in ℝ$
43		infregelb	$⊢ ((R \subseteq ℝ \land R \neq \emptyset \land \exists x \in ℝ \forall w \in R x \leq w) \land 0 \in ℝ) \to (0 \leq inf (R ℝ <) \leftrightarrow \forall w \in R 0 \leq w)$
44	18 19 25 42 43	syl31anc	$⊢ (φ \land n \in ℕ) \to (0 \leq inf (R ℝ <) \leftrightarrow \forall w \in R 0 \leq w)$
45	21 44	mpbird	$⊢ (φ \land n \in ℕ) \to 0 \leq inf (R ℝ <)$
46	45 11	breqtrrdi	$⊢ (φ \land n \in ℕ) \to 0 \leq S$
47	32 36	sqrtge0d	$⊢ (φ \land n \in ℕ) \to 0 \leq \sqrt{S^{2} + (\frac{1}{n})}$
48	28 41 46 47	lt2sqd	$⊢ (φ \land n \in ℕ) \to (S < \sqrt{S^{2} + (\frac{1}{n})} \leftrightarrow S^{2} < {\sqrt{S^{2} + (\frac{1}{n})}}^{2})$
49	39 48	mpbird	$⊢ (φ \land n \in ℕ) \to S < \sqrt{S^{2} + (\frac{1}{n})}$
50	28 41	ltnled	$⊢ (φ \land n \in ℕ) \to (S < \sqrt{S^{2} + (\frac{1}{n})} \leftrightarrow \neg \sqrt{S^{2} + (\frac{1}{n})} \leq S)$
51	49 50	mpbid	$⊢ (φ \land n \in ℕ) \to \neg \sqrt{S^{2} + (\frac{1}{n})} \leq S$
52	11	breq2i	$⊢ \sqrt{S^{2} + (\frac{1}{n})} \leq S \leftrightarrow \sqrt{S^{2} + (\frac{1}{n})} \leq inf (R ℝ <)$
53		infregelb	$⊢ ((R \subseteq ℝ \land R \neq \emptyset \land \exists x \in ℝ \forall w \in R x \leq w) \land \sqrt{S^{2} + (\frac{1}{n})} \in ℝ) \to (\sqrt{S^{2} + (\frac{1}{n})} \leq inf (R ℝ <) \leftrightarrow \forall w \in R \sqrt{S^{2} + (\frac{1}{n})} \leq w)$
54	18 19 25 41 53	syl31anc	$⊢ (φ \land n \in ℕ) \to (\sqrt{S^{2} + (\frac{1}{n})} \leq inf (R ℝ <) \leftrightarrow \forall w \in R \sqrt{S^{2} + (\frac{1}{n})} \leq w)$
55	52 54	bitrid	$⊢ (φ \land n \in ℕ) \to (\sqrt{S^{2} + (\frac{1}{n})} \leq S \leftrightarrow \forall w \in R \sqrt{S^{2} + (\frac{1}{n})} \leq w)$
56	10	raleqi	$⊢ \forall w \in R \sqrt{S^{2} + (\frac{1}{n})} \leq w \leftrightarrow \forall w \in ran (y \in Y ⟼ N (A M y)) \sqrt{S^{2} + (\frac{1}{n})} \leq w$
57		fvex	$⊢ N (A M y) \in V$
58	57	rgenw	$⊢ \forall y \in Y N (A M y) \in V$
59		eqid	$⊢ (y \in Y ⟼ N (A M y)) = (y \in Y ⟼ N (A M y))$
60		breq2	$⊢ w = N (A M y) \to (\sqrt{S^{2} + (\frac{1}{n})} \leq w \leftrightarrow \sqrt{S^{2} + (\frac{1}{n})} \leq N (A M y))$
61	59 60	ralrnmptw	$⊢ \forall y \in Y N (A M y) \in V \to (\forall w \in ran (y \in Y ⟼ N (A M y)) \sqrt{S^{2} + (\frac{1}{n})} \leq w \leftrightarrow \forall y \in Y \sqrt{S^{2} + (\frac{1}{n})} \leq N (A M y))$
62	58 61	ax-mp	$⊢ \forall w \in ran (y \in Y ⟼ N (A M y)) \sqrt{S^{2} + (\frac{1}{n})} \leq w \leftrightarrow \forall y \in Y \sqrt{S^{2} + (\frac{1}{n})} \leq N (A M y)$
63	56 62	bitri	$⊢ \forall w \in R \sqrt{S^{2} + (\frac{1}{n})} \leq w \leftrightarrow \forall y \in Y \sqrt{S^{2} + (\frac{1}{n})} \leq N (A M y)$
64	55 63	bitrdi	$⊢ (φ \land n \in ℕ) \to (\sqrt{S^{2} + (\frac{1}{n})} \leq S \leftrightarrow \forall y \in Y \sqrt{S^{2} + (\frac{1}{n})} \leq N (A M y))$
65	51 64	mtbid	$⊢ (φ \land n \in ℕ) \to \neg \forall y \in Y \sqrt{S^{2} + (\frac{1}{n})} \leq N (A M y)$
66		rexnal	$⊢ \exists y \in Y \neg \sqrt{S^{2} + (\frac{1}{n})} \leq N (A M y) \leftrightarrow \neg \forall y \in Y \sqrt{S^{2} + (\frac{1}{n})} \leq N (A M y)$
67	65 66	sylibr	$⊢ (φ \land n \in ℕ) \to \exists y \in Y \neg \sqrt{S^{2} + (\frac{1}{n})} \leq N (A M y)$
68	32	adantr	$⊢ ((φ \land n \in ℕ) \land y \in Y) \to S^{2} + (\frac{1}{n}) \in ℝ$
69		phnv	$⊢ U \in {CPreHil}_{OLD} \to U \in NrmCVec$
70	5 69	syl	$⊢ φ \to U \in NrmCVec$
71	70	ad2antrr	$⊢ ((φ \land n \in ℕ) \land y \in Y) \to U \in NrmCVec$
72	7	ad2antrr	$⊢ ((φ \land n \in ℕ) \land y \in Y) \to A \in X$
73		inss1	$⊢ SubSp (U) \cap CBan \subseteq SubSp (U)$
74	73 6	sselid	$⊢ φ \to W \in SubSp (U)$
75		eqid	$⊢ SubSp (U) = SubSp (U)$
76	1 4 75	sspba	$⊢ (U \in NrmCVec \land W \in SubSp (U)) \to Y \subseteq X$
77	70 74 76	syl2anc	$⊢ φ \to Y \subseteq X$
78	77	adantr	$⊢ (φ \land n \in ℕ) \to Y \subseteq X$
79	78	sselda	$⊢ ((φ \land n \in ℕ) \land y \in Y) \to y \in X$
80	1 2	nvmcl	$⊢ (U \in NrmCVec \land A \in X \land y \in X) \to A M y \in X$
81	71 72 79 80	syl3anc	$⊢ ((φ \land n \in ℕ) \land y \in Y) \to A M y \in X$
82	1 3	nvcl	$⊢ (U \in NrmCVec \land A M y \in X) \to N (A M y) \in ℝ$
83	71 81 82	syl2anc	$⊢ ((φ \land n \in ℕ) \land y \in Y) \to N (A M y) \in ℝ$
84	83	resqcld	$⊢ ((φ \land n \in ℕ) \land y \in Y) \to {N (A M y)}^{2} \in ℝ$
85	68 84	letrid	$⊢ ((φ \land n \in ℕ) \land y \in Y) \to (S^{2} + (\frac{1}{n}) \leq {N (A M y)}^{2} \lor {N (A M y)}^{2} \leq S^{2} + (\frac{1}{n}))$
86	85	ord	$⊢ ((φ \land n \in ℕ) \land y \in Y) \to (\neg S^{2} + (\frac{1}{n}) \leq {N (A M y)}^{2} \to {N (A M y)}^{2} \leq S^{2} + (\frac{1}{n}))$
87	41	adantr	$⊢ ((φ \land n \in ℕ) \land y \in Y) \to \sqrt{S^{2} + (\frac{1}{n})} \in ℝ$
88	47	adantr	$⊢ ((φ \land n \in ℕ) \land y \in Y) \to 0 \leq \sqrt{S^{2} + (\frac{1}{n})}$
89	1 3	nvge0	$⊢ (U \in NrmCVec \land A M y \in X) \to 0 \leq N (A M y)$
90	71 81 89	syl2anc	$⊢ ((φ \land n \in ℕ) \land y \in Y) \to 0 \leq N (A M y)$
91	87 83 88 90	le2sqd	$⊢ ((φ \land n \in ℕ) \land y \in Y) \to (\sqrt{S^{2} + (\frac{1}{n})} \leq N (A M y) \leftrightarrow {\sqrt{S^{2} + (\frac{1}{n})}}^{2} \leq {N (A M y)}^{2})$
92	38	adantr	$⊢ ((φ \land n \in ℕ) \land y \in Y) \to {\sqrt{S^{2} + (\frac{1}{n})}}^{2} = S^{2} + (\frac{1}{n})$
93	92	breq1d	$⊢ ((φ \land n \in ℕ) \land y \in Y) \to ({\sqrt{S^{2} + (\frac{1}{n})}}^{2} \leq {N (A M y)}^{2} \leftrightarrow S^{2} + (\frac{1}{n}) \leq {N (A M y)}^{2})$
94	91 93	bitrd	$⊢ ((φ \land n \in ℕ) \land y \in Y) \to (\sqrt{S^{2} + (\frac{1}{n})} \leq N (A M y) \leftrightarrow S^{2} + (\frac{1}{n}) \leq {N (A M y)}^{2})$
95	94	notbid	$⊢ ((φ \land n \in ℕ) \land y \in Y) \to (\neg \sqrt{S^{2} + (\frac{1}{n})} \leq N (A M y) \leftrightarrow \neg S^{2} + (\frac{1}{n}) \leq {N (A M y)}^{2})$
96	1 2 3 8	imsdval	$⊢ (U \in NrmCVec \land A \in X \land y \in X) \to A D y = N (A M y)$
97	71 72 79 96	syl3anc	$⊢ ((φ \land n \in ℕ) \land y \in Y) \to A D y = N (A M y)$
98	97	oveq1d	$⊢ ((φ \land n \in ℕ) \land y \in Y) \to {(A D y)}^{2} = {N (A M y)}^{2}$
99	98	breq1d	$⊢ ((φ \land n \in ℕ) \land y \in Y) \to ({(A D y)}^{2} \leq S^{2} + (\frac{1}{n}) \leftrightarrow {N (A M y)}^{2} \leq S^{2} + (\frac{1}{n}))$
100	86 95 99	3imtr4d	$⊢ ((φ \land n \in ℕ) \land y \in Y) \to (\neg \sqrt{S^{2} + (\frac{1}{n})} \leq N (A M y) \to {(A D y)}^{2} \leq S^{2} + (\frac{1}{n}))$
101	100	reximdva	$⊢ (φ \land n \in ℕ) \to (\exists y \in Y \neg \sqrt{S^{2} + (\frac{1}{n})} \leq N (A M y) \to \exists y \in Y {(A D y)}^{2} \leq S^{2} + (\frac{1}{n}))$
102	67 101	mpd	$⊢ (φ \land n \in ℕ) \to \exists y \in Y {(A D y)}^{2} \leq S^{2} + (\frac{1}{n})$
103	102	ralrimiva	$⊢ φ \to \forall n \in ℕ \exists y \in Y {(A D y)}^{2} \leq S^{2} + (\frac{1}{n})$
104	4	fvexi	$⊢ Y \in V$
105		nnenom	$⊢ ℕ \approx ω$
106		oveq2	$⊢ y = f (n) \to A D y = A D f (n)$
107	106	oveq1d	$⊢ y = f (n) \to {(A D y)}^{2} = {(A D f (n))}^{2}$
108	107	breq1d	$⊢ y = f (n) \to ({(A D y)}^{2} \leq S^{2} + (\frac{1}{n}) \leftrightarrow {(A D f (n))}^{2} \leq S^{2} + (\frac{1}{n}))$
109	104 105 108	axcc4	$⊢ \forall n \in ℕ \exists y \in Y {(A D y)}^{2} \leq S^{2} + (\frac{1}{n}) \to \exists f (f : ℕ ⟶ Y \land \forall n \in ℕ {(A D f (n))}^{2} \leq S^{2} + (\frac{1}{n}))$
110	103 109	syl	$⊢ φ \to \exists f (f : ℕ ⟶ Y \land \forall n \in ℕ {(A D f (n))}^{2} \leq S^{2} + (\frac{1}{n}))$
111	5	adantr	$⊢ (φ \land (f : ℕ ⟶ Y \land \forall n \in ℕ {(A D f (n))}^{2} \leq S^{2} + (\frac{1}{n}))) \to U \in {CPreHil}_{OLD}$
112	6	adantr	$⊢ (φ \land (f : ℕ ⟶ Y \land \forall n \in ℕ {(A D f (n))}^{2} \leq S^{2} + (\frac{1}{n}))) \to W \in (SubSp (U) \cap CBan)$
113	7	adantr	$⊢ (φ \land (f : ℕ ⟶ Y \land \forall n \in ℕ {(A D f (n))}^{2} \leq S^{2} + (\frac{1}{n}))) \to A \in X$
114		simprl	$⊢ (φ \land (f : ℕ ⟶ Y \land \forall n \in ℕ {(A D f (n))}^{2} \leq S^{2} + (\frac{1}{n}))) \to f : ℕ ⟶ Y$
115		simprr	$⊢ (φ \land (f : ℕ ⟶ Y \land \forall n \in ℕ {(A D f (n))}^{2} \leq S^{2} + (\frac{1}{n}))) \to \forall n \in ℕ {(A D f (n))}^{2} \leq S^{2} + (\frac{1}{n})$
116		fveq2	$⊢ n = k \to f (n) = f (k)$
117	116	oveq2d	$⊢ n = k \to A D f (n) = A D f (k)$
118	117	oveq1d	$⊢ n = k \to {(A D f (n))}^{2} = {(A D f (k))}^{2}$
119		oveq2	$⊢ n = k \to \frac{1}{n} = \frac{1}{k}$
120	119	oveq2d	$⊢ n = k \to S^{2} + (\frac{1}{n}) = S^{2} + (\frac{1}{k})$
121	118 120	breq12d	$⊢ n = k \to ({(A D f (n))}^{2} \leq S^{2} + (\frac{1}{n}) \leftrightarrow {(A D f (k))}^{2} \leq S^{2} + (\frac{1}{k}))$
122	121	rspccva	$⊢ (\forall n \in ℕ {(A D f (n))}^{2} \leq S^{2} + (\frac{1}{n}) \land k \in ℕ) \to {(A D f (k))}^{2} \leq S^{2} + (\frac{1}{k})$
123	115 122	sylan	$⊢ ((φ \land (f : ℕ ⟶ Y \land \forall n \in ℕ {(A D f (n))}^{2} \leq S^{2} + (\frac{1}{n}))) \land k \in ℕ) \to {(A D f (k))}^{2} \leq S^{2} + (\frac{1}{k})$
124		eqid	$⊢ \frac{1}{{(\frac{(A D \underset{t}{⇝} (J) (f)) + S}{2})}^{2} - S^{2}} = \frac{1}{{(\frac{(A D \underset{t}{⇝} (J) (f)) + S}{2})}^{2} - S^{2}}$
125	1 2 3 4 111 112 113 8 9 10 11 114 123 124	minvecolem4	$⊢ (φ \land (f : ℕ ⟶ Y \land \forall n \in ℕ {(A D f (n))}^{2} \leq S^{2} + (\frac{1}{n}))) \to \exists x \in Y \forall y \in Y N (A M x) \leq N (A M y)$
126	110 125	exlimddv	$⊢ φ \to \exists x \in Y \forall y \in Y N (A M x) \leq N (A M y)$

Metamath Proof Explorer

Theorem minvecolem5

Proof