Metamath Proof Explorer - mmtheorems52

Jump to page: 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5787

Statement List for Metamath Proof Explorer - 5101-5200 - Page 52 of 58

Type	Label	Description
Statement
Theorem	bcs 5101	Bunjakovaskij-Cauchy-Schwarz inequality. Remark 3.4 of [Beran] p. 98.
⊢ A ∈ ℋ    &   ⊢ B ∈ ℋ    ⇒   ⊢ (abs ‘(A ·i B)) ≤ ((norm ‘A) · (norm ‘B))
Definition	df-cauchy 5102	Define the set of Cauchy sequences on a Hilbert space. See hcauchy 5103 for its membership relation. Note that f:ℕ–→ ℋ is an infinite sequence of vectors, i.e. a mapping from integers to vectors. Definition of Cauchy sequence in [Beran] p. 96.
⊢ Cauchy = {f∣(f:ℕ–→ ℋ ∧ ∀x ∈ ℝ (0 < x → ∃y ∈ ℕ ∀z ∈ ℕ ∀w ∈ ℕ ((y ≤ z ∧ y ≤ w) → (norm ‘((F ‘z) −v (F ‘w))) < x)))}
Theorem	hcauchy 5103	Member of the set of Cauchy sequences on a Hilbert space. Definition for Cauchy sequence in [Beran] p. 96.
⊢ (F ∈ Cauchy ↔ (F:ℕ–→ ℋ ∧ ∀x ∈ ℝ (0 < x → ∃y ∈ ℕ ∀z ∈ ℕ ∀w ∈ ℕ ((y ≤ z ∧ y ≤ w) → (norm ‘((F ‘z) −v (F ‘w))) < x))))
Theorem	cauchyseq 5104	A Cauchy sequences on a Hilbert space is a sequence.
⊢ (F ∈ Cauchy → F:ℕ–→ ℋ )
Theorem	cauchyconv 5105	A Cauchy sequence on a Hilbert space converges.
⊢ (F ∈ Cauchy → ∀x ∈ ℝ (0 < x → ∃y ∈ ℕ ∀z ∈ ℕ ∀w ∈ ℕ ((y ≤ z ∧ y ≤ w) → (norm ‘((F ‘z) −v (F ‘w))) < x)))
Theorem	seqcauchy 5106	A sequence on a Hilbert space is a Cauchy sequence if it converges.
⊢ (F:ℕ–→ ℋ → (F ∈ Cauchy ↔ ∀x ∈ ℝ (0 < x → ∃y ∈ ℕ ∀z ∈ ℕ ∀w ∈ ℕ ((y ≤ z ∧ y ≤ w) → (norm ‘((F ‘z) −v (F ‘w))) < x))))
Definition	df-hlim 5107	Define the limit relation for Hilbert space. See hlim 5108 for its relational expression. Note that f:ℕ–→ ℋ is an infinite sequence of vectors, i.e. a mapping from integers to vectors. Definition of converge in [Beran] p. 96.
⊢ ⇝v = {⟨f, w⟩∣((f:ℕ–→ ℋ ∧ w ∈ ℋ ) ∧ ∀x ∈ ℝ (0 < x → ∃y ∈ ℕ ∀z ∈ ℕ (y ≤ z → (norm ‘((f ‘z) −v w)) < x)))}
Theorem	hlim 5108	Express the predicate: The limit of vector sequence F in a Hilbert space is A, i.e. F converges to A. This means that for any real x, no matter how small, there always exists an integer y such that the norm of any later vector in the sequence minus the limit is less than x. Definition of converge in [Beran] p. 96.
⊢ F ∈ V    &   ⊢ A ∈ V    ⇒   ⊢ (F ⇝v A ↔ ((F:ℕ–→ ℋ ∧ A ∈ ℋ ) ∧ ∀x ∈ ℝ (0 < x → ∃y ∈ ℕ ∀z ∈ ℕ (y ≤ z → (norm ‘((F ‘z) −v A)) < x))))
Theorem	hlimseq 5109	A sequence with a limit on a Hilbert space is a sequence.
⊢ F ∈ V    &   ⊢ A ∈ V    ⇒   ⊢ (F ⇝v A → F:ℕ–→ ℋ )
Theorem	hlimvec 5110	Closure of the limit of a sequence on Hilbert space.
⊢ F ∈ V    &   ⊢ A ∈ V    ⇒   ⊢ (F ⇝v A → A ∈ ℋ )
Theorem	hlimconv 5111	Convergence of a sequence on a Hilbert space.
⊢ F ∈ V    &   ⊢ A ∈ V    ⇒   ⊢ (F ⇝v A → ∀x ∈ ℝ (0 < x → ∃y ∈ ℕ ∀z ∈ ℕ (y ≤ z → (norm ‘((F ‘z) −v A)) < x)))
Theorem	hlim2 5112	The limit of a sequence on a Hilbert space.
⊢ ((F:ℕ–→ ℋ ∧ A ∈ ℋ ) → (F ⇝v A ↔ ∀x ∈ ℝ (0 < x → ∃y ∈ ℕ ∀z ∈ ℕ (y ≤ z → (norm ‘((F ‘z) −v A)) < x))))
Axiom	ax-hcompl 5113	Completeness of a Hilbert space.
⊢ (F ∈ Cauchy → ∃x ∈ ℋ F ⇝v x)
Definition	df-sh 5114	Define the set of subspaces of a Hilbert space. See sh 5116 for its membership relation. Basically, a subspace is a subset of a Hilbert space that acts like a vector space. From Definition of [Beran] p. 95.
⊢ Sℋ = {h∣((h ⊆ ℋ ∧ 0v ∈ h) ∧ (∀x ∈ h ∀y ∈ h (x +v y) ∈ h ∧ ∀x ∈ ℂ ∀y ∈ h (x ·s y) ∈ h))}
Theorem	shex 5115	The set of subspaces of a Hilbert space exists (is a set).
⊢ Sℋ ∈ V
Theorem	sh 5116	Subspace H of a Hilbert space. A subspace is a subset of Hilbert space which contains the zero vector and is closed under vector addition and scalar multiplication. Definition of [Beran] p. 95.
⊢ (H ∈ Sℋ ↔ ((H ⊆ ℋ ∧ 0v ∈ H) ∧ (∀x ∈ H ∀y ∈ H (x +v y) ∈ H ∧ ∀x ∈ ℂ ∀y ∈ H (x ·s y) ∈ H)))
Theorem	shss 5117	A subspace is a subset of Hilbert space.
⊢ (H ∈ Sℋ → H ⊆ ℋ )
Theorem	shelt 5118	A member of a subspace of a Hilbert space is a vector.
⊢ ((H ∈ Sℋ ∧ A ∈ H) → A ∈ ℋ )
Theorem	shssi 5119	A closed subspace of a Hilbert space is a subset of Hilbert space.
⊢ H ∈ Sℋ    ⇒   ⊢ H ⊆ ℋ
Theorem	shel 5120	A member of a subspace of a Hilbert space is a vector.
⊢ H ∈ Sℋ    ⇒   ⊢ (A ∈ H → A ∈ ℋ )
Theorem	sheli 5121	A member of a subspace of a Hilbert space is a vector.
⊢ H ∈ Sℋ    &   ⊢ A ∈ H    ⇒   ⊢ A ∈ ℋ
Theorem	sh0 5122	The zero vector belongs to any subspace of a Hilbert space.
⊢ (H ∈ Sℋ → 0v ∈ H)
Theorem	shaddclt 5123	Closure of vector addition in a subspace of a Hilbert space.
⊢ (H ∈ Sℋ → ((A ∈ H ∧ B ∈ H) → (A +v B) ∈ H))
Theorem	shmulclt 5124	Closure of vector scalar multiplication in a subspace of a Hilbert space.
⊢ (H ∈ Sℋ → ((A ∈ ℂ ∧ B ∈ H) → (A ·s B) ∈ H))
Theorem	shsubclt 5125	Closure of vector subtraction in a subspace of a Hilbert space.
⊢ (H ∈ Sℋ → ((A ∈ H ∧ B ∈ H) → (A −v B) ∈ H))
Theorem	sh2 5126	Subspace H of a Hilbert space.
⊢ (H ⊆ ℋ → (H ∈ Sℋ ↔ (0v ∈ H ∧ (∀x ∈ H ∀y ∈ H (x +v y) ∈ H ∧ ∀x ∈ ℂ ∀y ∈ H (x ·s y) ∈ H))))
Definition	df-ch 5127	Define the set of closed subspaces of a Hilbert space. A closed subspace is one in which the limit of every convergent sequence in the subspace belongs to the subspace. For its membership relation, see closedsub 5128. From Definition of [Beran] p. 107. Alternate definitions are given by chcmh 5148 and dfch2 5254.
⊢ Cℋ = {h∣(h ∈ Sℋ ∧ ∀f∀x((f:ℕ–→h ∧ f ⇝v x) → x ∈ h))}
Theorem	closedsub 5128	Closed subspace H of a Hilbert space. Definition of [Beran] p. 107.
⊢ (H ∈ Cℋ ↔ (H ∈ Sℋ ∧ ∀f∀x((f:ℕ–→H ∧ f ⇝v x) → x ∈ H)))
Theorem	chsssh 5129	Closed subspaces are subspaces in a Hilbert space.
⊢ Cℋ ⊆ Sℋ
Theorem	chex 5130	The set of closed subspaces of a Hilbert space exists (is a set).
⊢ Cℋ ∈ V
Theorem	chsh 5131	A closed subspace is a subspace.
⊢ (H ∈ Cℋ → H ∈ Sℋ )
Theorem	chshi 5132	A closed subspace is a subspace.
⊢ H ∈ Cℋ    ⇒   ⊢ H ∈ Sℋ
Theorem	ch0 5133	The zero vector belongs to any closed subspace of a Hilbert space.
⊢ (H ∈ Cℋ → 0v ∈ H)
Theorem	chss 5134	A closed subspace of a Hilbert space is a subset of Hilbert space.
⊢ (H ∈ Cℋ → H ⊆ ℋ )
Theorem	chelt 5135	A member of a closed subspace of a Hilbert space is a vector.
⊢ ((H ∈ Cℋ ∧ A ∈ H) → A ∈ ℋ )
Theorem	chssi 5136	A closed subspace of a Hilbert space is a subset of Hilbert space.
⊢ H ∈ Cℋ    ⇒   ⊢ H ⊆ ℋ
Theorem	chel 5137	A member of a closed subspace of a Hilbert space is a vector.
⊢ H ∈ Cℋ    ⇒   ⊢ (A ∈ H → A ∈ ℋ )
Theorem	cheli 5138	A member of a closed subspace of a Hilbert space is a vector.
⊢ H ∈ Cℋ    &   ⊢ A ∈ H    ⇒   ⊢ A ∈ ℋ
Theorem	chlim 5139	The limit property of a closed subspace of a Hilbert space.
⊢ A ∈ V    ⇒   ⊢ (H ∈ Cℋ → ((F:ℕ–→H ∧ F ⇝v A) → A ∈ H))
Theorem	hlim0 5140	The zero sequence in Hilbert space converges to the zero vector.
⊢ (ℕ × {0v}) ⇝v 0v
Theorem	hlimcaui 5141	If a sequence in Hilbert space subset converges to a limit, it is a Cauchy sequence.
⊢ A ∈ V    &   ⊢ F ∈ V    &   ⊢ F ⇝v A    ⇒   ⊢ F ∈ Cauchy
Theorem	hlimcau 5142	If a sequence in Hilbert space subset converges to a limit, it is a Cauchy sequence.
⊢ A ∈ V    &   ⊢ F ∈ V    ⇒   ⊢ (F ⇝v A → F ∈ Cauchy)
Theorem	hlimunii 5143	A Hilbert space sequence converges to at most one limit.
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ F ∈ V    &   ⊢ (F ⇝v A ∧ F ⇝v B)    ⇒   ⊢ A = B
Theorem	hlimuni 5144	A Hilbert space sequence converges to at most one limit.
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ F ∈ V    ⇒   ⊢ ((F ⇝v A ∧ F ⇝v B) → A = B)
Theorem	hlimreu 5145	The limit of a Hilbert space sequence is unique.
⊢ F ∈ V    ⇒   ⊢ (∃x ∈ H F ⇝v x ↔ ∃!x ∈ H F ⇝v x)
Theorem	hlimeu 5146	The limit of a Hilbert space sequence is unique.
⊢ F ∈ V    ⇒   ⊢ (∃x F ⇝v x ↔ ∃!x F ⇝v x)
Theorem	chsscm 5147	The hypothesis defines the set of complete subspaces of Hilbert space. A complete subspace is one in which every Cauchy sequence of vectors in the subspace converges to a member of the subspace (Definition of complete subspace in [Beran] p. 96). Any closed subspace of a Hilbert space is complete. Part of Remark 3.12 of [Beran] p. 107.
⊢ C = {h∣(h ∈ Sℋ ∧ ∀f ∈ Cauchy (f:ℕ–→h → ∃x ∈ h f ⇝v x))}    ⇒   ⊢ Cℋ ⊆ C
Theorem	chcmh 5148	The hypothesis defines the set of complete subspaces of Hilbert space (see chsscm 5147). A Hilbert subspace is closed iff it is complete. Remark 3.12(C) of [Beran] p. 107.
⊢ C = {h∣(h ∈ Sℋ ∧ ∀f ∈ Cauchy (f:ℕ–→h → ∃x ∈ h f ⇝v x))}    ⇒   ⊢ Cℋ = C
Theorem	ch2 5149	A Hilbert subspace is closed iff it is complete. Remark 3.12(C) of [Beran] p. 107.
⊢ (H ∈ Cℋ ↔ (H ∈ Sℋ ∧ ∀f ∈ Cauchy (f:ℕ–→H → ∃x ∈ H f ⇝v x)))
Theorem	chcompl 5150	Completeness of a closed subspace of Hilbert space.
⊢ (H ∈ Cℋ → ((F ∈ Cauchy ∧ F:ℕ–→H) → ∃x ∈ H F ⇝v x))
Theorem	helch 5151	The unit Hilbert lattice element (which is all of Hilbert space) belongs to the Hilbert lattice. Part of Proposition 1 of [Kalmbach] p. 65.
⊢ ℋ ∈ Cℋ
Theorem	helsh 5152	Hilbert space is a subspace of Hilbert space.
⊢ ℋ ∈ Sℋ
Theorem	shsspwh 5153	Subspaces are subsets of Hilbert space.
⊢ Sℋ ⊆ ℘ ℋ
Theorem	chsspwh 5154	Closed subspaces are subsets of Hilbert space.
⊢ Cℋ ⊆ ℘ ℋ
Theorem	hsn0elch 5155	The zero subspace belongs to the set of closed subspaces of Hilbert space.
⊢ {0v} ∈ Cℋ
Definition	df-oc 5156	Define orthogonal complement of a subset (usually a subspace) of Hilbert space. The orthogonal complement is the set of all vectors orthogonal to all vectors in the subset. See ocvalt 5161 and chocval 5178 for its value. Textbooks usually denote this unary operation with the symbol ⊥ as a small superscript, although Mittelstaedt uses the symbol as a prefix operation. Here we define a function (prefix operation) ⊥ rather than introducing a new syntactical form. This lets us take advantage of the theorems about functions that we already have proved under set theory. Definition of [Mittelstaedt] p. 9.
⊢ ⊥ = {⟨x, y⟩∣(x ⊆ ℋ ∧ y = {z ∈ ℋ ∣∀w ∈ x (z ·i w) = 0})}
Definition	df-ch0 5157	Define the zero for closed subspaces of Hilbert space. See h0elch 5159 for closure law.
⊢ 0ℋ = {0v}
Theorem	elch0 5158	Membership in zero for closed subspaces of Hilbert space.
⊢ (A ∈ 0ℋ ↔ A = 0v)
Theorem	h0elch 5159	The zero subspace is a closed subspace. Part of Proposition 1 of [Kalmbach] p. 65.
⊢ 0ℋ ∈ Cℋ
Theorem	h0elsh 5160	The zero subspace is a subspace of Hilbert space.
⊢ 0ℋ ∈ Sℋ
Theorem	ocvalt 5161	Value of orthogonal complement of a subset of Hilbert space.
⊢ (H ⊆ ℋ → (⊥ ‘H) = {x ∈ ℋ ∣∀y ∈ H (x ·i y) = 0})
Theorem	ocelt 5162	Membership in orthogonal complement of H subset.
⊢ (H ⊆ ℋ → (A ∈ (⊥ ‘H) ↔ (A ∈ ℋ ∧ ∀x ∈ H (A ·i x) = 0)))
Theorem	shocelt 5163	Membership in orthogonal complement of H subspace.
⊢ (H ∈ Sℋ → (A ∈ (⊥ ‘H) ↔ (A ∈ ℋ ∧ ∀x ∈ H (A ·i x) = 0)))
Theorem	ocsh 5164	The orthogonal complement of a subspace is a subspace. Part of Remark 3.12 of [Beran] p. 107.
⊢ (A ⊆ ℋ → (⊥ ‘A) ∈ Sℋ )
Theorem	shocsh 5165	The orthogonal complement of a subspace is a subspace. Part of Remark 3.12 of [Beran] p. 107.
⊢ (A ∈ Sℋ → (⊥ ‘A) ∈ Sℋ )
Theorem	ocss 5166	An orthogonal complement is a subset of Hilbert space.
⊢ (A ⊆ ℋ → (⊥ ‘A) ⊆ ℋ )
Theorem	shocss 5167	An orthogonal complement is a subset of Hilbert space.
⊢ (A ∈ Sℋ → (⊥ ‘A) ⊆ ℋ )
Theorem	occont 5168	Contraposition law for orthogonal complement.
⊢ ((A ⊆ ℋ ∧ B ⊆ ℋ ) → (A ⊆ B → (⊥ ‘B) ⊆ (⊥ ‘A)))
Theorem	occon2t 5169	Double contraposition for orthogonal complement.
⊢ ((A ⊆ ℋ ∧ B ⊆ ℋ ) → (A ⊆ B → (⊥ ‘(⊥ ‘A)) ⊆ (⊥ ‘(⊥ ‘B))))
Theorem	occon2 5170	Double contraposition for orthogonal complement.
⊢ A ⊆ ℋ    &   ⊢ B ⊆ ℋ    ⇒   ⊢ (A ⊆ B → (⊥ ‘(⊥ ‘A)) ⊆ (⊥ ‘(⊥ ‘B)))
Theorem	oc0 5171	The zero vector belongs to an orthogonal complement of a Hilbert subspace.
⊢ (H ∈ Sℋ → 0v ∈ (⊥ ‘H))
Theorem	ocorth 5172	Members of a subset and its complement are orthogonal.
⊢ (H ⊆ ℋ → ((A ∈ H ∧ B ∈ (⊥ ‘H)) → (A ·i B) = 0))
Theorem	shocorth 5173	Members of a subspace and its complement are orthogonal.
⊢ (H ∈ Sℋ → ((A ∈ H ∧ B ∈ (⊥ ‘H)) → (A ·i B) = 0))
Theorem	ococss 5174	Inclusion in complement of complement. Part of Proposition 1 of [Kalmbach] p. 65.
⊢ (A ⊆ ℋ → A ⊆ (⊥ ‘(⊥ ‘A)))
Theorem	shococss 5175	Inclusion in complement of complement. Part of Proposition 1 of [Kalmbach] p. 65.
⊢ (A ∈ Sℋ → A ⊆ (⊥ ‘(⊥ ‘A)))
Theorem	shorth 5176	Members of orthogonal subspaces are orthogonal.
⊢ (H ∈ Sℋ → (G ⊆ (⊥ ‘H) → ((A ∈ G ∧ B ∈ H) → (A ·i B) = 0)))
Theorem	ocin 5177	Intersection of a Hilbert subspace and its complement. Part of Proposition 1 of [Kalmbach] p. 65.
⊢ (A ∈ Sℋ → (A ∩ (⊥ ‘A)) = 0ℋ)
Theorem	chocval 5178	Value of the orthogonal complement of a Hilbert lattice element. The orthogonal complement of A is the set of vectors that are orthogonal to all vectors in A.
⊢ A ∈ Cℋ    ⇒   ⊢ (⊥ ‘A) = {x ∈ ℋ ∣∀y ∈ A (x ·i y) = 0}
Theorem	chocuni 5179	Lemma for uniqueness part of Projection Theorem. Theorem 3.7(i) of [Beran] p. 102 (uniqueness part).
⊢ H ∈ Cℋ    ⇒   ⊢ (((A ∈ H ∧ B ∈ (⊥ ‘H)) ∧ (C ∈ H ∧ D ∈ (⊥ ‘H))) → ((R = (A +v B) ∧ R = (C +v D)) → (A = C ∧ B = D)))
Theorem	occllem1 5180	Lemma for closure of complement of Hilbert subspace. Part of Remark 3.12 of [Beran] p. 107.
⊢ A ∈ ℋ    &   ⊢ B ∈ ℋ    &   ⊢ S ∈ ℋ    ⇒   ⊢ (abs ‘((B ·i S) − (A ·i S))) ≤ ((norm ‘(B −v A)) · (norm ‘S))
Theorem	occllem2 5181	Lemma for closure of complement of Hilbert subspace. Part of Remark 3.12 of [Beran] p. 107.
⊢ S ∈ ℋ    ⇒   ⊢ ((A ∈ ℋ ∧ B ∈ ℋ ) → (abs ‘((B ·i S) − (A ·i S))) ≤ ((norm ‘(B −v A)) · (norm ‘S)))
Theorem	occllem3 5182	Lemma for closure of complement of Hilbert subspace. Part of Remark 3.12 of [Beran] p. 107.
⊢ G = {⟨x, y⟩∣(x ∈ ℕ ∧ y = ((F ‘x) ·i S))}    ⇒   ⊢ (D ∈ ℕ → (G ‘D) = ((F ‘D) ·i S))
Theorem	occllem4 5183	Lemma for closure of complement of Hilbert subspace. Part of Remark 3.12 of [Beran] p. 107.
⊢ G = {⟨x, y⟩∣(x ∈ ℕ ∧ y = ((F ‘x) ·i S))}    &   ⊢ S ∈ ℋ    ⇒   ⊢ (F:ℕ–→ ℋ → G:ℕ–→ℂ)
Theorem	occllem5 5184	Lemma for closure of complement of Hilbert subspace. Part of Remark 3.12 of [Beran] p. 107.
⊢ G = {⟨x, y⟩∣(x ∈ ℕ ∧ y = ((F ‘x) ·i S))}    ⇒   ⊢ (∀z ∈ ℕ ((F ‘z) ·i S) = 0 → G ⇝ 0)
Theorem	occllem6 5185	Lemma for closure of complement of Hilbert subspace. Part of Remark 3.12 of [Beran] p. 107.
⊢ G = {⟨x, y⟩∣(x ∈ ℕ ∧ y = ((F ‘x) ·i S))}    &   ⊢ A ∈ ℋ    &   ⊢ S ∈ ℋ    &   ⊢ F ∈ V    ⇒   ⊢ (¬ S = 0v → (F ⇝v A → G ⇝ (A ·i S)))
Theorem	occllem7 5186	Lemma for closure of complement of Hilbert subspace. Part of Remark 3.12 of [Beran] p. 107.
⊢ A ∈ ℋ    &   ⊢ S ∈ ℋ    &   ⊢ F ∈ V    ⇒   ⊢ ((F ⇝v A ∧ ∀x ∈ ℕ ((F ‘x) ·i S) = 0) → (A ·i S) = 0)
Theorem	occllem8 5187	Lemma for closure of complement of Hilbert subspace. Part of Remark 3.12 of [Beran] p. 107.
⊢ F ∈ V    ⇒   ⊢ ((A ∈ ℋ ∧ S ∈ ℋ ) → ((F ⇝v A ∧ ∀x ∈ ℕ ((F ‘x) ·i S) = 0) → (A ·i S) = 0))
Theorem	occl 5188	Closure of complement of Hilbert subset. Part of Remark 3.12 of [Beran] p. 107.
⊢ A ⊆ ℋ    ⇒   ⊢ (⊥ ‘A) ∈ Cℋ
Theorem	occlt 5189	Closure of complement of Hilbert subset. Part of Remark 3.12 of [Beran] p. 107.
⊢ (A ⊆ ℋ → (⊥ ‘A) ∈ Cℋ )
Theorem	shocclt 5190	Closure of complement of Hilbert subspace. Part of Remark 3.12 of [Beran] p. 107.
⊢ (A ∈ Sℋ → (⊥ ‘A) ∈ Cℋ )
Theorem	choclt 5191	Closure of complement of Hilbert subspace. Part of Remark 3.12 of [Beran] p. 107.
⊢ (A ∈ Cℋ → (⊥ ‘A) ∈ Cℋ )
Theorem	chocl 5192	Closure of Cℋ orthocomplement.
⊢ A ∈ Cℋ    ⇒   ⊢ (⊥ ‘A) ∈ Cℋ
Theorem	projlem1 5193	Part of Lemma 3.6 of [Beran] p. 100: "Choose e > 0. Let n0 be a natural number satisfying the inequality n0 > 4(2i0 + 1) · e ↑ -1." Used by projlem2 5194.
⊢ R ∈ ℝ    &   ⊢ D ∈ ℝ    ⇒   ⊢ (0 < D → ∃z ∈ ℕ ((4 · ((2 · R) + 1)) / z) < (D↑2))
Theorem	projlem2 5194	Part of Lemma 3.6 of [Beran] p. 100. We need the square root for the norm limit. Used by projlem28 5220.
⊢ R ∈ ℝ    &   ⊢ D ∈ ℝ    &   ⊢ 0 ≤ R    ⇒   ⊢ (0 < D → ∃z ∈ ℕ (√ ‘((4 · ((2 · R) + 1)) / z)) < D)
Theorem	projlem3 5195	Part of Lemma 3.6 of [Beran] p. 100, bottom inequality. Used by projlem6 5198.
⊢ R ∈ ℝ    &   ⊢ D ∈ ℕ    &   ⊢ G ∈ ℕ    ⇒   ⊢ (((2 · ((R + (1 / D))↑2)) + (2 · ((R + (1 / G))↑2))) − (4 · (R↑2))) ≤ (((4 · R) + 2) · ((1 / D) + (1 / G)))
Theorem	projlem4 5196	Part of Lemma 3.6 of [Beran] p. 101, top. Used by projlem6 5198.
⊢ R ∈ ℝ    &   ⊢ 0 ≤ R    &   ⊢ D ∈ ℕ    &   ⊢ G ∈ ℕ    &   ⊢ B ∈ ℕ    ⇒   ⊢ ((B ≤ D ∧ B ≤ G) → (((4 · R) + 2) · ((1 / D) + (1 / G))) ≤ ((4 · ((2 · R) + 1)) / B))
Theorem	projlem5 5197	Part of Lemma 3.6 of [Beran] p. 100, bottom. Used by projlem6 5198.
⊢ A ∈ ℋ    &   ⊢ B ∈ ℋ    &   ⊢ C ∈ ℋ    &   ⊢ R ∈ ℝ    &   ⊢ 0 ≤ R    &   ⊢ (4 · (R↑2)) ≤ ((norm ‘((B +v C) −v (2 ·s A)))↑2)    &   ⊢ D ∈ ℕ    &   ⊢ G ∈ ℕ    &   ⊢ N ∈ ℕ    &   ⊢ (norm ‘(B −v A)) < (R + (1 / D))    &   ⊢ (norm ‘(C −v A)) < (R + (1 / G))    ⇒   ⊢ ((norm ‘(B −v C))↑2) < (((2 · ((R + (1 / D))↑2)) + (2 · ((R + (1 / G))↑2))) − (4 · (R↑2)))
Theorem	projlem6 5198	Part of Lemma 3.6 of [Beran] p. 101. Used by projlem7 5199.
⊢ A ∈ ℋ    &   ⊢ B ∈ ℋ    &   ⊢ C ∈ ℋ    &   ⊢ R ∈ ℝ    &   ⊢ 0 ≤ R    &   ⊢ (4 · (R↑2)) ≤ ((norm ‘((B +v C) −v (2 ·s A)))↑2)    &   ⊢ D ∈ ℕ    &   ⊢ G ∈ ℕ    &   ⊢ N ∈ ℕ    &   ⊢ (norm ‘(B −v A)) < (R + (1 / D))    &   ⊢ (norm ‘(C −v A)) < (R + (1 / G))    ⇒   ⊢ ((N ≤ D ∧ N ≤ G) → (norm ‘(B −v C)) < (√ ‘((4 · ((2 · R) + 1)) / N)))
Theorem	projlem7 5199	Part of Lemma 3.6 of [Beran] p. 101. Applies weak deduction theorem to projlem6 5198. Used by projlem19 5211.
⊢ A ∈ ℋ    &   ⊢ B ∈ ℋ    &   ⊢ C ∈ ℋ    &   ⊢ R ∈ ℝ    &   ⊢ 0 ≤ R    &   ⊢ (4 · (R↑2)) ≤ ((norm ‘((B +v C) −v (2 ·s A)))↑2)    &   ⊢ D ∈ ℕ    &   ⊢ G ∈ ℕ    &   ⊢ N ∈ ℕ    ⇒   ⊢ (((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))) → ((N ≤ D ∧ N ≤ G) → (norm ‘(B −v C)) < (√ ‘((4 · ((2 · R) + 1)) / N))))
Theorem	projlem8 5200	Part of Lemma 3.6 of [Beran] p. 100. The set S is a non-empty set of reals with an upper bound. Part of Lemma 3.6 of [Beran] p. 100. Used by projlem9 5201 projlem12 5204 projlem13 5205 projlem15 5207. Note we use 'supremum'; its negative is the infimum.
⊢ A ∈ ℋ    &   ⊢ H ∈ Cℋ    &   ⊢ S = {u ∈ ℝ∣∃v ∈ H u = -(norm ‘(v −v A))}    ⇒   ⊢ (S ⊆ ℝ ∧ ¬ S = ∅ ∧ ∃z ∈ ℝ ∀w ∈ S w ≤ z)