P. 311 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 31001-31100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	his35 31001	Move scalar multiplication to outside of inner product. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → ((𝐴 ·ℎ 𝐶) ·ih (𝐵 ·ℎ 𝐷)) = ((𝐴 · (∗‘𝐵)) · (𝐶 ·ih 𝐷)))
Theorem	his35i 31002	Move scalar multiplication to outside of inner product. (Contributed by NM, 1-Jul-2005.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℋ    &   ⊢ 𝐷 ∈ ℋ    ⇒   ⊢ ((𝐴 ·ℎ 𝐶) ·ih (𝐵 ·ℎ 𝐷)) = ((𝐴 · (∗‘𝐵)) · (𝐶 ·ih 𝐷))
Theorem	his7 31003	Distributive law for inner product. Lemma 3.1(S7) of [Beran] p. 95. (Contributed by NM, 31-Jul-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐴 ·ih (𝐵 +ℎ 𝐶)) = ((𝐴 ·ih 𝐵) + (𝐴 ·ih 𝐶)))
Theorem	hiassdi 31004	Distributive/associative law for inner product, useful for linearity proofs. (Contributed by NM, 10-May-2005.) (New usage is discouraged.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → (((𝐴 ·ℎ 𝐵) +ℎ 𝐶) ·ih 𝐷) = ((𝐴 · (𝐵 ·ih 𝐷)) + (𝐶 ·ih 𝐷)))
Theorem	his2sub 31005	Distributive law for inner product of vector subtraction. (Contributed by NM, 16-Nov-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 −ℎ 𝐵) ·ih 𝐶) = ((𝐴 ·ih 𝐶) − (𝐵 ·ih 𝐶)))
Theorem	his2sub2 31006	Distributive law for inner product of vector subtraction. (Contributed by NM, 13-Feb-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐴 ·ih (𝐵 −ℎ 𝐶)) = ((𝐴 ·ih 𝐵) − (𝐴 ·ih 𝐶)))
Theorem	hire 31007	A necessary and sufficient condition for an inner product to be real. (Contributed by NM, 2-Jul-2005.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝐴 ·ih 𝐵) ∈ ℝ ↔ (𝐴 ·ih 𝐵) = (𝐵 ·ih 𝐴)))
Theorem	hiidrcl 31008	Real closure of inner product with self. (Contributed by NM, 29-May-1999.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (𝐴 ·ih 𝐴) ∈ ℝ)
Theorem	hi01 31009	Inner product with the 0 vector. (Contributed by NM, 29-May-1999.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (0ℎ ·ih 𝐴) = 0)
Theorem	hi02 31010	Inner product with the 0 vector. (Contributed by NM, 13-Oct-1999.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (𝐴 ·ih 0ℎ) = 0)
Theorem	hiidge0 31011	Inner product with self is not negative. (Contributed by NM, 29-May-1999.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → 0 ≤ (𝐴 ·ih 𝐴))
Theorem	his6 31012	Zero inner product with self means vector is zero. Lemma 3.1(S6) of [Beran] p. 95. (Contributed by NM, 27-Jul-1999.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → ((𝐴 ·ih 𝐴) = 0 ↔ 𝐴 = 0ℎ))
Theorem	his1i 31013	Conjugate law for inner product. Postulate (S1) of [Beran] p. 95. (Contributed by NM, 15-May-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ (𝐴 ·ih 𝐵) = (∗‘(𝐵 ·ih 𝐴))
Theorem	abshicom 31014	Commuted inner products have the same absolute values. (Contributed by NM, 26-May-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (abs‘(𝐴 ·ih 𝐵)) = (abs‘(𝐵 ·ih 𝐴)))
Theorem	hial0 31015*	A vector whose inner product is always zero is zero. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (∀𝑥 ∈ ℋ (𝐴 ·ih 𝑥) = 0 ↔ 𝐴 = 0ℎ))
Theorem	hial02 31016*	A vector whose inner product is always zero is zero. (Contributed by NM, 28-Jan-2006.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (∀𝑥 ∈ ℋ (𝑥 ·ih 𝐴) = 0 ↔ 𝐴 = 0ℎ))
Theorem	hisubcomi 31017	Two vector subtractions simultaneously commute in an inner product. (Contributed by NM, 1-Jul-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    &   ⊢ 𝐶 ∈ ℋ    &   ⊢ 𝐷 ∈ ℋ    ⇒   ⊢ ((𝐴 −ℎ 𝐵) ·ih (𝐶 −ℎ 𝐷)) = ((𝐵 −ℎ 𝐴) ·ih (𝐷 −ℎ 𝐶))
Theorem	hi2eq 31018	Lemma used to prove equality of vectors. (Contributed by NM, 16-Nov-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝐴 ·ih (𝐴 −ℎ 𝐵)) = (𝐵 ·ih (𝐴 −ℎ 𝐵)) ↔ 𝐴 = 𝐵))
Theorem	hial2eq 31019*	Two vectors whose inner product is always equal are equal. (Contributed by NM, 16-Nov-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (∀𝑥 ∈ ℋ (𝐴 ·ih 𝑥) = (𝐵 ·ih 𝑥) ↔ 𝐴 = 𝐵))
Theorem	hial2eq2 31020*	Two vectors whose inner product is always equal are equal. (Contributed by NM, 28-Jan-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (∀𝑥 ∈ ℋ (𝑥 ·ih 𝐴) = (𝑥 ·ih 𝐵) ↔ 𝐴 = 𝐵))
Theorem	orthcom 31021	Orthogonality commutes. (Contributed by NM, 10-Oct-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝐴 ·ih 𝐵) = 0 ↔ (𝐵 ·ih 𝐴) = 0))
Theorem	normlem0 31022	Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 7-Oct-1999.) (New usage is discouraged.)
⊢ 𝑆 ∈ ℂ    &   ⊢ 𝐹 ∈ ℋ    &   ⊢ 𝐺 ∈ ℋ    ⇒   ⊢ ((𝐹 −ℎ (𝑆 ·ℎ 𝐺)) ·ih (𝐹 −ℎ (𝑆 ·ℎ 𝐺))) = (((𝐹 ·ih 𝐹) + (-(∗‘𝑆) · (𝐹 ·ih 𝐺))) + ((-𝑆 · (𝐺 ·ih 𝐹)) + ((𝑆 · (∗‘𝑆)) · (𝐺 ·ih 𝐺))))
Theorem	normlem1 31023	Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 22-Aug-1999.) (New usage is discouraged.)
⊢ 𝑆 ∈ ℂ    &   ⊢ 𝐹 ∈ ℋ    &   ⊢ 𝐺 ∈ ℋ    &   ⊢ 𝑅 ∈ ℝ    &   ⊢ (abs‘𝑆) = 1    ⇒   ⊢ ((𝐹 −ℎ ((𝑆 · 𝑅) ·ℎ 𝐺)) ·ih (𝐹 −ℎ ((𝑆 · 𝑅) ·ℎ 𝐺))) = (((𝐹 ·ih 𝐹) + (((∗‘𝑆) · -𝑅) · (𝐹 ·ih 𝐺))) + (((𝑆 · -𝑅) · (𝐺 ·ih 𝐹)) + ((𝑅↑2) · (𝐺 ·ih 𝐺))))
Theorem	normlem2 31024	Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 27-Jul-1999.) (New usage is discouraged.)
⊢ 𝑆 ∈ ℂ    &   ⊢ 𝐹 ∈ ℋ    &   ⊢ 𝐺 ∈ ℋ    &   ⊢ 𝐵 = -(((∗‘𝑆) · (𝐹 ·ih 𝐺)) + (𝑆 · (𝐺 ·ih 𝐹)))    ⇒   ⊢ 𝐵 ∈ ℝ
Theorem	normlem3 31025	Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 21-Aug-1999.) (New usage is discouraged.)
⊢ 𝑆 ∈ ℂ    &   ⊢ 𝐹 ∈ ℋ    &   ⊢ 𝐺 ∈ ℋ    &   ⊢ 𝐵 = -(((∗‘𝑆) · (𝐹 ·ih 𝐺)) + (𝑆 · (𝐺 ·ih 𝐹)))    &   ⊢ 𝐴 = (𝐺 ·ih 𝐺)    &   ⊢ 𝐶 = (𝐹 ·ih 𝐹)    &   ⊢ 𝑅 ∈ ℝ    ⇒   ⊢ (((𝐴 · (𝑅↑2)) + (𝐵 · 𝑅)) + 𝐶) = (((𝐹 ·ih 𝐹) + (((∗‘𝑆) · -𝑅) · (𝐹 ·ih 𝐺))) + (((𝑆 · -𝑅) · (𝐺 ·ih 𝐹)) + ((𝑅↑2) · (𝐺 ·ih 𝐺))))
Theorem	normlem4 31026	Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 29-Jul-1999.) (New usage is discouraged.)
⊢ 𝑆 ∈ ℂ    &   ⊢ 𝐹 ∈ ℋ    &   ⊢ 𝐺 ∈ ℋ    &   ⊢ 𝐵 = -(((∗‘𝑆) · (𝐹 ·ih 𝐺)) + (𝑆 · (𝐺 ·ih 𝐹)))    &   ⊢ 𝐴 = (𝐺 ·ih 𝐺)    &   ⊢ 𝐶 = (𝐹 ·ih 𝐹)    &   ⊢ 𝑅 ∈ ℝ    &   ⊢ (abs‘𝑆) = 1    ⇒   ⊢ ((𝐹 −ℎ ((𝑆 · 𝑅) ·ℎ 𝐺)) ·ih (𝐹 −ℎ ((𝑆 · 𝑅) ·ℎ 𝐺))) = (((𝐴 · (𝑅↑2)) + (𝐵 · 𝑅)) + 𝐶)
Theorem	normlem5 31027	Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 10-Aug-1999.) (New usage is discouraged.)
⊢ 𝑆 ∈ ℂ    &   ⊢ 𝐹 ∈ ℋ    &   ⊢ 𝐺 ∈ ℋ    &   ⊢ 𝐵 = -(((∗‘𝑆) · (𝐹 ·ih 𝐺)) + (𝑆 · (𝐺 ·ih 𝐹)))    &   ⊢ 𝐴 = (𝐺 ·ih 𝐺)    &   ⊢ 𝐶 = (𝐹 ·ih 𝐹)    &   ⊢ 𝑅 ∈ ℝ    &   ⊢ (abs‘𝑆) = 1    ⇒   ⊢ 0 ≤ (((𝐴 · (𝑅↑2)) + (𝐵 · 𝑅)) + 𝐶)
Theorem	normlem6 31028	Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 2-Aug-1999.) (Revised by Mario Carneiro, 4-Jun-2014.) (New usage is discouraged.)
⊢ 𝑆 ∈ ℂ    &   ⊢ 𝐹 ∈ ℋ    &   ⊢ 𝐺 ∈ ℋ    &   ⊢ 𝐵 = -(((∗‘𝑆) · (𝐹 ·ih 𝐺)) + (𝑆 · (𝐺 ·ih 𝐹)))    &   ⊢ 𝐴 = (𝐺 ·ih 𝐺)    &   ⊢ 𝐶 = (𝐹 ·ih 𝐹)    &   ⊢ (abs‘𝑆) = 1    ⇒   ⊢ (abs‘𝐵) ≤ (2 · ((√‘𝐴) · (√‘𝐶)))
Theorem	normlem7 31029	Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 11-Aug-1999.) (New usage is discouraged.)
⊢ 𝑆 ∈ ℂ    &   ⊢ 𝐹 ∈ ℋ    &   ⊢ 𝐺 ∈ ℋ    &   ⊢ (abs‘𝑆) = 1    ⇒   ⊢ (((∗‘𝑆) · (𝐹 ·ih 𝐺)) + (𝑆 · (𝐺 ·ih 𝐹))) ≤ (2 · ((√‘(𝐺 ·ih 𝐺)) · (√‘(𝐹 ·ih 𝐹))))
Theorem	normlem8 31030	Lemma used to derive properties of norm. (Contributed by NM, 30-Jun-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    &   ⊢ 𝐶 ∈ ℋ    &   ⊢ 𝐷 ∈ ℋ    ⇒   ⊢ ((𝐴 +ℎ 𝐵) ·ih (𝐶 +ℎ 𝐷)) = (((𝐴 ·ih 𝐶) + (𝐵 ·ih 𝐷)) + ((𝐴 ·ih 𝐷) + (𝐵 ·ih 𝐶)))
Theorem	normlem9 31031	Lemma used to derive properties of norm. (Contributed by NM, 30-Jun-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    &   ⊢ 𝐶 ∈ ℋ    &   ⊢ 𝐷 ∈ ℋ    ⇒   ⊢ ((𝐴 −ℎ 𝐵) ·ih (𝐶 −ℎ 𝐷)) = (((𝐴 ·ih 𝐶) + (𝐵 ·ih 𝐷)) − ((𝐴 ·ih 𝐷) + (𝐵 ·ih 𝐶)))
Theorem	normlem7tALT 31032	Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 11-Oct-1999.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ ((𝑆 ∈ ℂ ∧ (abs‘𝑆) = 1) → (((∗‘𝑆) · (𝐴 ·ih 𝐵)) + (𝑆 · (𝐵 ·ih 𝐴))) ≤ (2 · ((√‘(𝐵 ·ih 𝐵)) · (√‘(𝐴 ·ih 𝐴)))))
Theorem	bcseqi 31033	Equality case of Bunjakovaskij-Cauchy-Schwarz inequality. Specifically, in the equality case the two vectors are collinear. Compare bcsiHIL 31093. (Contributed by NM, 16-Jul-2001.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ (((𝐴 ·ih 𝐵) · (𝐵 ·ih 𝐴)) = ((𝐴 ·ih 𝐴) · (𝐵 ·ih 𝐵)) ↔ ((𝐵 ·ih 𝐵) ·ℎ 𝐴) = ((𝐴 ·ih 𝐵) ·ℎ 𝐵))
Theorem	normlem9at 31034	Lemma used to derive properties of norm. Part of Remark 3.4(B) of [Beran] p. 98. (Contributed by NM, 10-May-2005.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝐴 −ℎ 𝐵) ·ih (𝐴 −ℎ 𝐵)) = (((𝐴 ·ih 𝐴) + (𝐵 ·ih 𝐵)) − ((𝐴 ·ih 𝐵) + (𝐵 ·ih 𝐴))))
20.2.2  Norms
Theorem	dfhnorm2 31035	Alternate definition of the norm of a vector of Hilbert space. Definition of norm in [Beran] p. 96. (Contributed by NM, 6-Jun-2008.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.)
⊢ normℎ = (𝑥 ∈ ℋ ↦ (√‘(𝑥 ·ih 𝑥)))
Theorem	normf 31036	The norm function maps from Hilbert space to reals. (Contributed by NM, 6-Sep-2007.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.)
⊢ normℎ: ℋ⟶ℝ
Theorem	normval 31037	The value of the norm of a vector in Hilbert space. Definition of norm in [Beran] p. 96. In the literature, the norm of 𝐴 is usually written as "|| 𝐴 ||", but we use function value notation to take advantage of our existing theorems about functions. (Contributed by NM, 29-May-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (normℎ‘𝐴) = (√‘(𝐴 ·ih 𝐴)))
Theorem	normcl 31038	Real closure of the norm of a vector. (Contributed by NM, 29-May-1999.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (normℎ‘𝐴) ∈ ℝ)
Theorem	normge0 31039	The norm of a vector is nonnegative. (Contributed by NM, 29-May-1999.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → 0 ≤ (normℎ‘𝐴))
Theorem	normgt0 31040	The norm of nonzero vector is positive. (Contributed by NM, 10-Apr-2006.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (𝐴 ≠ 0ℎ ↔ 0 < (normℎ‘𝐴)))
Theorem	norm0 31041	The norm of a zero vector. (Contributed by NM, 30-May-1999.) (New usage is discouraged.)
⊢ (normℎ‘0ℎ) = 0
Theorem	norm-i 31042	Theorem 3.3(i) of [Beran] p. 97. (Contributed by NM, 29-Jul-1999.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → ((normℎ‘𝐴) = 0 ↔ 𝐴 = 0ℎ))
Theorem	normne0 31043	A norm is nonzero iff its argument is a nonzero vector. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → ((normℎ‘𝐴) ≠ 0 ↔ 𝐴 ≠ 0ℎ))
Theorem	normcli 31044	Real closure of the norm of a vector. (Contributed by NM, 30-Sep-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    ⇒   ⊢ (normℎ‘𝐴) ∈ ℝ
Theorem	normsqi 31045	The square of a norm. (Contributed by NM, 21-Aug-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    ⇒   ⊢ ((normℎ‘𝐴)↑2) = (𝐴 ·ih 𝐴)
Theorem	norm-i-i 31046	Theorem 3.3(i) of [Beran] p. 97. (Contributed by NM, 5-Sep-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    ⇒   ⊢ ((normℎ‘𝐴) = 0 ↔ 𝐴 = 0ℎ)
Theorem	normsq 31047	The square of a norm. (Contributed by NM, 12-May-2005.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → ((normℎ‘𝐴)↑2) = (𝐴 ·ih 𝐴))
Theorem	normsub0i 31048	Two vectors are equal iff the norm of their difference is zero. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ ((normℎ‘(𝐴 −ℎ 𝐵)) = 0 ↔ 𝐴 = 𝐵)
Theorem	normsub0 31049	Two vectors are equal iff the norm of their difference is zero. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((normℎ‘(𝐴 −ℎ 𝐵)) = 0 ↔ 𝐴 = 𝐵))
Theorem	norm-ii-i 31050	Triangle inequality for norms. Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 11-Aug-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ (normℎ‘(𝐴 +ℎ 𝐵)) ≤ ((normℎ‘𝐴) + (normℎ‘𝐵))
Theorem	norm-ii 31051	Triangle inequality for norms. Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (normℎ‘(𝐴 +ℎ 𝐵)) ≤ ((normℎ‘𝐴) + (normℎ‘𝐵)))
Theorem	norm-iii-i 31052	Theorem 3.3(iii) of [Beran] p. 97. (Contributed by NM, 29-Jul-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ (normℎ‘(𝐴 ·ℎ 𝐵)) = ((abs‘𝐴) · (normℎ‘𝐵))
Theorem	norm-iii 31053	Theorem 3.3(iii) of [Beran] p. 97. (Contributed by NM, 25-Oct-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (normℎ‘(𝐴 ·ℎ 𝐵)) = ((abs‘𝐴) · (normℎ‘𝐵)))
Theorem	normsubi 31054	Negative doesn't change the norm of a Hilbert space vector. (Contributed by NM, 11-Aug-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ (normℎ‘(𝐴 −ℎ 𝐵)) = (normℎ‘(𝐵 −ℎ 𝐴))
Theorem	normpythi 31055	Analogy to Pythagorean theorem for orthogonal vectors. Remark 3.4(C) of [Beran] p. 98. (Contributed by NM, 17-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ ((𝐴 ·ih 𝐵) = 0 → ((normℎ‘(𝐴 +ℎ 𝐵))↑2) = (((normℎ‘𝐴)↑2) + ((normℎ‘𝐵)↑2)))
Theorem	normsub 31056	Swapping order of subtraction doesn't change the norm of a vector. (Contributed by NM, 14-Aug-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (normℎ‘(𝐴 −ℎ 𝐵)) = (normℎ‘(𝐵 −ℎ 𝐴)))
Theorem	normneg 31057	The norm of a vector equals the norm of its negative. (Contributed by NM, 23-May-2005.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (normℎ‘(-1 ·ℎ 𝐴)) = (normℎ‘𝐴))
Theorem	normpyth 31058	Analogy to Pythagorean theorem for orthogonal vectors. Remark 3.4(C) of [Beran] p. 98. (Contributed by NM, 17-Oct-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝐴 ·ih 𝐵) = 0 → ((normℎ‘(𝐴 +ℎ 𝐵))↑2) = (((normℎ‘𝐴)↑2) + ((normℎ‘𝐵)↑2))))
Theorem	normpyc 31059	Corollary to Pythagorean theorem for orthogonal vectors. Remark 3.4(C) of [Beran] p. 98. (Contributed by NM, 26-Oct-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝐴 ·ih 𝐵) = 0 → (normℎ‘𝐴) ≤ (normℎ‘(𝐴 +ℎ 𝐵))))
Theorem	norm3difi 31060	Norm of differences around common element. Part of Lemma 3.6 of [Beran] p. 101. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    &   ⊢ 𝐶 ∈ ℋ    ⇒   ⊢ (normℎ‘(𝐴 −ℎ 𝐵)) ≤ ((normℎ‘(𝐴 −ℎ 𝐶)) + (normℎ‘(𝐶 −ℎ 𝐵)))
Theorem	norm3adifii 31061	Norm of differences around common element. Part of Lemma 3.6 of [Beran] p. 101. (Contributed by NM, 30-Sep-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    &   ⊢ 𝐶 ∈ ℋ    ⇒   ⊢ (abs‘((normℎ‘(𝐴 −ℎ 𝐶)) − (normℎ‘(𝐵 −ℎ 𝐶)))) ≤ (normℎ‘(𝐴 −ℎ 𝐵))
Theorem	norm3lem 31062	Lemma involving norm of differences in Hilbert space. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    &   ⊢ 𝐶 ∈ ℋ    &   ⊢ 𝐷 ∈ ℝ    ⇒   ⊢ (((normℎ‘(𝐴 −ℎ 𝐶)) < (𝐷 / 2) ∧ (normℎ‘(𝐶 −ℎ 𝐵)) < (𝐷 / 2)) → (normℎ‘(𝐴 −ℎ 𝐵)) < 𝐷)
Theorem	norm3dif 31063	Norm of differences around common element. Part of Lemma 3.6 of [Beran] p. 101. (Contributed by NM, 20-Apr-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (normℎ‘(𝐴 −ℎ 𝐵)) ≤ ((normℎ‘(𝐴 −ℎ 𝐶)) + (normℎ‘(𝐶 −ℎ 𝐵))))
Theorem	norm3dif2 31064	Norm of differences around common element. (Contributed by NM, 18-Apr-2007.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (normℎ‘(𝐴 −ℎ 𝐵)) ≤ ((normℎ‘(𝐶 −ℎ 𝐴)) + (normℎ‘(𝐶 −ℎ 𝐵))))
Theorem	norm3lemt 31065	Lemma involving norm of differences in Hilbert space. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.)
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℝ)) → (((normℎ‘(𝐴 −ℎ 𝐶)) < (𝐷 / 2) ∧ (normℎ‘(𝐶 −ℎ 𝐵)) < (𝐷 / 2)) → (normℎ‘(𝐴 −ℎ 𝐵)) < 𝐷))
Theorem	norm3adifi 31066	Norm of differences around common element. Part of Lemma 3.6 of [Beran] p. 101. (Contributed by NM, 3-Oct-1999.) (New usage is discouraged.)
⊢ 𝐶 ∈ ℋ    ⇒   ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (abs‘((normℎ‘(𝐴 −ℎ 𝐶)) − (normℎ‘(𝐵 −ℎ 𝐶)))) ≤ (normℎ‘(𝐴 −ℎ 𝐵)))
Theorem	normpari 31067	Parallelogram law for norms. Remark 3.4(B) of [Beran] p. 98. (Contributed by NM, 21-Aug-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ (((normℎ‘(𝐴 −ℎ 𝐵))↑2) + ((normℎ‘(𝐴 +ℎ 𝐵))↑2)) = ((2 · ((normℎ‘𝐴)↑2)) + (2 · ((normℎ‘𝐵)↑2)))
Theorem	normpar 31068	Parallelogram law for norms. Remark 3.4(B) of [Beran] p. 98. (Contributed by NM, 15-Apr-2007.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (((normℎ‘(𝐴 −ℎ 𝐵))↑2) + ((normℎ‘(𝐴 +ℎ 𝐵))↑2)) = ((2 · ((normℎ‘𝐴)↑2)) + (2 · ((normℎ‘𝐵)↑2))))
Theorem	normpar2i 31069	Corollary of parallelogram law for norms. Part of Lemma 3.6 of [Beran] p. 100. (Contributed by NM, 5-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    &   ⊢ 𝐶 ∈ ℋ    ⇒   ⊢ ((normℎ‘(𝐴 −ℎ 𝐵))↑2) = (((2 · ((normℎ‘(𝐴 −ℎ 𝐶))↑2)) + (2 · ((normℎ‘(𝐵 −ℎ 𝐶))↑2))) − ((normℎ‘((𝐴 +ℎ 𝐵) −ℎ (2 ·ℎ 𝐶)))↑2))
Theorem	polid2i 31070	Generalized polarization identity. Generalization of Exercise 4(a) of [ReedSimon] p. 63. (Contributed by NM, 30-Jun-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    &   ⊢ 𝐶 ∈ ℋ    &   ⊢ 𝐷 ∈ ℋ    ⇒   ⊢ (𝐴 ·ih 𝐵) = (((((𝐴 +ℎ 𝐶) ·ih (𝐷 +ℎ 𝐵)) − ((𝐴 −ℎ 𝐶) ·ih (𝐷 −ℎ 𝐵))) + (i · (((𝐴 +ℎ (i ·ℎ 𝐶)) ·ih (𝐷 +ℎ (i ·ℎ 𝐵))) − ((𝐴 −ℎ (i ·ℎ 𝐶)) ·ih (𝐷 −ℎ (i ·ℎ 𝐵)))))) / 4)
Theorem	polidi 31071	Polarization identity. Recovers inner product from norm. Exercise 4(a) of [ReedSimon] p. 63. The outermost operation is + instead of - due to our mathematicians' (rather than physicists') version of Axiom ax-his3 30997. (Contributed by NM, 30-Jun-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ (𝐴 ·ih 𝐵) = (((((normℎ‘(𝐴 +ℎ 𝐵))↑2) − ((normℎ‘(𝐴 −ℎ 𝐵))↑2)) + (i · (((normℎ‘(𝐴 +ℎ (i ·ℎ 𝐵)))↑2) − ((normℎ‘(𝐴 −ℎ (i ·ℎ 𝐵)))↑2)))) / 4)
Theorem	polid 31072	Polarization identity. Recovers inner product from norm. Exercise 4(a) of [ReedSimon] p. 63. The outermost operation is + instead of - due to our mathematicians' (rather than physicists') version of Axiom ax-his3 30997. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 ·ih 𝐵) = (((((normℎ‘(𝐴 +ℎ 𝐵))↑2) − ((normℎ‘(𝐴 −ℎ 𝐵))↑2)) + (i · (((normℎ‘(𝐴 +ℎ (i ·ℎ 𝐵)))↑2) − ((normℎ‘(𝐴 −ℎ (i ·ℎ 𝐵)))↑2)))) / 4))
20.2.3  Relate Hilbert space to normed complex vector spaces
Theorem	hilablo 31073	Hilbert space vector addition is an Abelian group operation. (Contributed by NM, 15-Apr-2007.) (New usage is discouraged.)
⊢ +ℎ ∈ AbelOp
Theorem	hilid 31074	The group identity element of Hilbert space vector addition is the zero vector. (Contributed by NM, 16-Apr-2007.) (New usage is discouraged.)
⊢ (GId‘ +ℎ ) = 0ℎ
Theorem	hilvc 31075	Hilbert space is a complex vector space. Vector addition is +ℎ, and scalar product is ·ℎ. (Contributed by NM, 15-Apr-2007.) (New usage is discouraged.)
⊢ ⟨ +ℎ , ·ℎ ⟩ ∈ CVecOLD
Theorem	hilnormi 31076	Hilbert space norm in terms of vector space norm. (Contributed by NM, 11-Sep-2007.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)
⊢ ℋ = (BaseSet‘𝑈)    &   ⊢ ·ih = (·𝑖OLD‘𝑈)    &   ⊢ 𝑈 ∈ NrmCVec    ⇒   ⊢ normℎ = (normCV‘𝑈)
Theorem	hilhhi 31077	Deduce the structure of Hilbert space from its components. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.)
⊢ ℋ = (BaseSet‘𝑈)    &   ⊢ +ℎ = ( +𝑣 ‘𝑈)    &   ⊢ ·ℎ = ( ·𝑠OLD ‘𝑈)    &   ⊢ ·ih = (·𝑖OLD‘𝑈)    &   ⊢ 𝑈 ∈ NrmCVec    ⇒   ⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩
Theorem	hhnv 31078	Hilbert space is a normed complex vector space. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    ⇒   ⊢ 𝑈 ∈ NrmCVec
Theorem	hhva 31079	The group (addition) operation of Hilbert space. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    ⇒   ⊢ +ℎ = ( +𝑣 ‘𝑈)
Theorem	hhba 31080	The base set of Hilbert space. This theorem provides an independent proof of df-hba 30882 (see comments in that definition). (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    ⇒   ⊢ ℋ = (BaseSet‘𝑈)
Theorem	hh0v 31081	The zero vector of Hilbert space. (Contributed by NM, 17-Nov-2007.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    ⇒   ⊢ 0ℎ = (0vec‘𝑈)
Theorem	hhsm 31082	The scalar product operation of Hilbert space. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    ⇒   ⊢ ·ℎ = ( ·𝑠OLD ‘𝑈)
Theorem	hhvs 31083	The vector subtraction operation of Hilbert space. (Contributed by NM, 13-Dec-2007.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    ⇒   ⊢ −ℎ = ( −𝑣 ‘𝑈)
Theorem	hhnm 31084	The norm function of Hilbert space. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    ⇒   ⊢ normℎ = (normCV‘𝑈)
Theorem	hhims 31085	The induced metric of Hilbert space. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝐷 = (normℎ ∘ −ℎ )    ⇒   ⊢ 𝐷 = (IndMet‘𝑈)
Theorem	hhims2 31086	Hilbert space distance metric. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝐷 = (IndMet‘𝑈)    ⇒   ⊢ 𝐷 = (normℎ ∘ −ℎ )
Theorem	hhmet 31087	The induced metric of Hilbert space. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝐷 = (IndMet‘𝑈)    ⇒   ⊢ 𝐷 ∈ (Met‘ ℋ)
Theorem	hhxmet 31088	The induced metric of Hilbert space. (Contributed by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝐷 = (IndMet‘𝑈)    ⇒   ⊢ 𝐷 ∈ (∞Met‘ ℋ)
Theorem	hhmetdval 31089	Value of the distance function of the metric space of Hilbert space. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    &   ⊢ 𝐷 = (IndMet‘𝑈)    ⇒   ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴𝐷𝐵) = (normℎ‘(𝐴 −ℎ 𝐵)))
Theorem	hhip 31090	The inner product operation of Hilbert space. (Contributed by NM, 17-Nov-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    ⇒   ⊢ ·ih = (·𝑖OLD‘𝑈)
Theorem	hhph 31091	The Hilbert space of the Hilbert Space Explorer is an inner product space. (Contributed by NM, 24-Nov-2007.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩    ⇒   ⊢ 𝑈 ∈ CPreHilOLD
20.2.4  Bunjakovaskij-Cauchy-Schwarz inequality
Theorem	bcsiALT 31092	Bunjakovaskij-Cauchy-Schwarz inequality. Remark 3.4 of [Beran] p. 98. (Contributed by NM, 11-Oct-1999.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ (abs‘(𝐴 ·ih 𝐵)) ≤ ((normℎ‘𝐴) · (normℎ‘𝐵))
Theorem	bcsiHIL 31093	Bunjakovaskij-Cauchy-Schwarz inequality. Remark 3.4 of [Beran] p. 98. (Proved from ZFC version.) (Contributed by NM, 24-Nov-2007.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ (abs‘(𝐴 ·ih 𝐵)) ≤ ((normℎ‘𝐴) · (normℎ‘𝐵))
Theorem	bcs 31094	Bunjakovaskij-Cauchy-Schwarz inequality. Remark 3.4 of [Beran] p. 98. (Contributed by NM, 16-Feb-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (abs‘(𝐴 ·ih 𝐵)) ≤ ((normℎ‘𝐴) · (normℎ‘𝐵)))
Theorem	bcs2 31095	Corollary of the Bunjakovaskij-Cauchy-Schwarz inequality bcsiHIL 31093. (Contributed by NM, 24-May-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ (normℎ‘𝐴) ≤ 1) → (abs‘(𝐴 ·ih 𝐵)) ≤ (normℎ‘𝐵))
Theorem	bcs3 31096	Corollary of the Bunjakovaskij-Cauchy-Schwarz inequality bcsiHIL 31093. (Contributed by NM, 26-May-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ (normℎ‘𝐵) ≤ 1) → (abs‘(𝐴 ·ih 𝐵)) ≤ (normℎ‘𝐴))
20.3  Cauchy sequences and completeness axiom
20.3.1  Cauchy sequences and limits
Theorem	hcau 31097*	Member of the set of Cauchy sequences on a Hilbert space. Definition for Cauchy sequence in [Beran] p. 96. (Contributed by NM, 16-Aug-1999.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.)
⊢ (𝐹 ∈ Cauchy ↔ (𝐹:ℕ⟶ ℋ ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ≥‘𝑦)(normℎ‘((𝐹‘𝑦) −ℎ (𝐹‘𝑧))) < 𝑥))
Theorem	hcauseq 31098	A Cauchy sequences on a Hilbert space is a sequence. (Contributed by NM, 16-Aug-1999.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.)
⊢ (𝐹 ∈ Cauchy → 𝐹:ℕ⟶ ℋ)
Theorem	hcaucvg 31099*	A Cauchy sequence on a Hilbert space converges. (Contributed by NM, 16-Aug-1999.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.)
⊢ ((𝐹 ∈ Cauchy ∧ 𝐴 ∈ ℝ+) → ∃𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ≥‘𝑦)(normℎ‘((𝐹‘𝑦) −ℎ (𝐹‘𝑧))) < 𝐴)
Theorem	seq1hcau 31100*	A sequence on a Hilbert space is a Cauchy sequence if it converges. (Contributed by NM, 16-Aug-1999.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.)
⊢ (𝐹:ℕ⟶ ℋ → (𝐹 ∈ Cauchy ↔ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ≥‘𝑦)(normℎ‘((𝐹‘𝑦) −ℎ (𝐹‘𝑧))) < 𝑥))