Metamath Proof Explorer - mmtheorems51

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 - 5001-5100 - Page 51 of 58

Type	Label	Description
Statement
Theorem	hvsubval 5001	Value of vector subtraction definition.
⊢ A ∈ ℋ    &   ⊢ B ∈ ℋ    ⇒   ⊢ (A −v B) = (A +v (-1 ·s B))
Theorem	hvsubcl 5002	Closure of vector subtraction.
⊢ A ∈ ℋ    &   ⊢ B ∈ ℋ    ⇒   ⊢ (A −v B) ∈ ℋ
Theorem	hvaddid2t 5003	Addition with the zero vector.
⊢ (A ∈ ℋ → (0v +v A) = A)
Theorem	hvmul0t 5004	Scalar multiplication with the zero vector.
⊢ (A ∈ ℂ → (A ·s 0v) = 0v)
Theorem	hvsubidt 5005	Subtraction of a vector from itself.
⊢ (A ∈ ℋ → (A −v A) = 0v)
Theorem	hvnegidt 5006	Addition of negative of a vector to itself.
⊢ (A ∈ ℋ → (A +v (-1 ·s A)) = 0v)
Theorem	hvm1negt 5007	Convert minus one times a scalar product to the negative of the scalar.
⊢ ((A ∈ ℂ ∧ B ∈ ℋ ) → (-1 ·s (A ·s B)) = (-A ·s B))
Theorem	hvaddid2 5008	Addition with the zero vector.
⊢ A ∈ ℋ    ⇒   ⊢ (0v +v A) = A
Theorem	hvnegid 5009	Addition of negative of a vector to itself.
⊢ A ∈ ℋ    ⇒   ⊢ (A +v (-1 ·s A)) = 0v
Theorem	hv2neg 5010	Two ways of expressing negative.
⊢ A ∈ ℋ    ⇒   ⊢ (0v −v A) = (-1 ·s A)
Theorem	hvadd23t 5011	Commutative/associative law.
⊢ ((A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ) → ((A +v B) +v C) = ((A +v C) +v B))
Theorem	hvadd12t 5012	Commutative/associative law.
⊢ ((A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ) → (A +v (B +v C)) = (B +v (A +v C)))
Theorem	hvadd4t 5013	Hilbert vector space addition law.
⊢ (((A ∈ ℋ ∧ B ∈ ℋ ) ∧ (C ∈ ℋ ∧ D ∈ ℋ )) → ((A +v B) +v (C +v D)) = ((A +v C) +v (B +v D)))
Theorem	hvsub4t 5014	Hilbert vector space addition/subtraction law.
⊢ (((A ∈ ℋ ∧ B ∈ ℋ ) ∧ (C ∈ ℋ ∧ D ∈ ℋ )) → ((A +v B) −v (C +v D)) = ((A −v C) +v (B −v D)))
Theorem	hvaddsub12t 5015	Commutative/associative law.
⊢ ((A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ) → (A +v (B −v C)) = (B +v (A −v C)))
Theorem	hvsubcan1t 5016	Addition/subtraction cancellation law for vectors in Hilbert space.
⊢ ((A ∈ ℋ ∧ B ∈ ℋ ) → ((A +v B) −v B) = A)
Theorem	hvsubcan2t 5017	Addition/subtraction cancellation law for vectors in Hilbert space.
⊢ ((A ∈ ℋ ∧ B ∈ ℋ ) → ((A +v B) −v A) = B)
Theorem	hvaddsubasst 5018	Associativity of sum and difference of Hilbert space vectors.
⊢ ((A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ) → ((A +v B) −v C) = (A +v (B −v C)))
Theorem	hvsubaddeqt 5019	Subtraction and addition of equal Hilbert space vectors..
⊢ ((A ∈ ℋ ∧ B ∈ ℋ ) → (A +v (B −v A)) = B)
Theorem	hvmulass 5020	Scalar multiplication associative law.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    &   ⊢ C ∈ ℋ    ⇒   ⊢ ((A · B) ·s C) = (A ·s (B ·s C))
Theorem	hvmulcom 5021	Scalar multiplication commutative law.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    &   ⊢ C ∈ ℋ    ⇒   ⊢ (A ·s (B ·s C)) = (B ·s (A ·s C))
Theorem	hvmul2neg 5022	Double negative in scalar multiplication.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    &   ⊢ C ∈ ℋ    ⇒   ⊢ (-A ·s (-B ·s C)) = (A ·s (B ·s C))
Theorem	hvdistr1 5023	Scalar multiplication distributive law.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℋ    &   ⊢ C ∈ ℋ    ⇒   ⊢ (A ·s (B +v C)) = ((A ·s B) +v (A ·s C))
Theorem	hvsubdistr1 5024	Scalar multiplication distributive law.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℋ    &   ⊢ C ∈ ℋ    ⇒   ⊢ (A ·s (B −v C)) = ((A ·s B) −v (A ·s C))
Theorem	hvass 5025	Hilbert vector space associative law.
⊢ A ∈ ℋ    &   ⊢ B ∈ ℋ    &   ⊢ C ∈ ℋ    ⇒   ⊢ ((A +v B) +v C) = (A +v (B +v C))
Theorem	hvadd23 5026	Hilbert vector space commutative/associative law.
⊢ A ∈ ℋ    &   ⊢ B ∈ ℋ    &   ⊢ C ∈ ℋ    ⇒   ⊢ ((A +v B) +v C) = ((A +v C) +v B)
Theorem	hvsubass 5027	Hilbert vector space associative law for subtraction.
⊢ A ∈ ℋ    &   ⊢ B ∈ ℋ    &   ⊢ C ∈ ℋ    ⇒   ⊢ ((A −v B) −v C) = (A −v (B +v C))
Theorem	hvsub23 5028	Hilbert vector space commutative/associative law.
⊢ A ∈ ℋ    &   ⊢ B ∈ ℋ    &   ⊢ C ∈ ℋ    ⇒   ⊢ ((A −v B) −v C) = ((A −v C) −v B)
Theorem	hvadd12 5029	Hilbert vector space commutative/associative law.
⊢ A ∈ ℋ    &   ⊢ B ∈ ℋ    &   ⊢ C ∈ ℋ    ⇒   ⊢ (A +v (B +v C)) = (B +v (A +v C))
Theorem	hvadd4 5030	Hilbert vector space addition law.
⊢ A ∈ ℋ    &   ⊢ B ∈ ℋ    &   ⊢ C ∈ ℋ    &   ⊢ D ∈ ℋ    ⇒   ⊢ ((A +v B) +v (C +v D)) = ((A +v C) +v (B +v D))
Theorem	hvsubsub4 5031	Hilbert vector space addition law.
⊢ A ∈ ℋ    &   ⊢ B ∈ ℋ    &   ⊢ C ∈ ℋ    &   ⊢ D ∈ ℋ    ⇒   ⊢ ((A −v B) −v (C −v D)) = ((A −v C) −v (B −v D))
Theorem	hvsubsub4t 5032	Hilbert vector space addition/subtraction law.
⊢ (((A ∈ ℋ ∧ B ∈ ℋ ) ∧ (C ∈ ℋ ∧ D ∈ ℋ )) → ((A −v B) −v (C −v D)) = ((A −v C) −v (B −v D)))
Theorem	hv2times 5033	Two times a vector.
⊢ A ∈ ℋ    ⇒   ⊢ (2 ·s A) = (A +v A)
Theorem	hvnegdi 5034	Distribution of negative over subtraction.
⊢ A ∈ ℋ    &   ⊢ B ∈ ℋ    ⇒   ⊢ (-1 ·s (A −v B)) = (B −v A)
Theorem	hvsubeq0 5035	If the difference between two vectors is zero, they are equal.
⊢ A ∈ ℋ    &   ⊢ B ∈ ℋ    ⇒   ⊢ ((A −v B) = 0v ↔ A = B)
Theorem	hvsubcan2 5036	Vector cancellation law.
⊢ A ∈ ℋ    &   ⊢ B ∈ ℋ    ⇒   ⊢ ((A +v B) +v (A −v B)) = (2 ·s A)
Theorem	hvaddcan 5037	Cancellation law for vector addition.
⊢ A ∈ ℋ    &   ⊢ B ∈ ℋ    &   ⊢ C ∈ ℋ    ⇒   ⊢ ((A +v B) = (A +v C) ↔ B = C)
Theorem	hvsubadd 5038	Relationship between vector subtraction and addition.
⊢ A ∈ ℋ    &   ⊢ B ∈ ℋ    &   ⊢ C ∈ ℋ    ⇒   ⊢ ((A −v B) = C ↔ (B +v C) = A)
Theorem	hvnegdit 5039	Distribution of negative over subtraction.
⊢ ((A ∈ ℋ ∧ B ∈ ℋ ) → (-1 ·s (A −v B)) = (B −v A))
Theorem	hvsubeq0t 5040	If the difference between two vectors is zero, they are equal.
⊢ ((A ∈ ℋ ∧ B ∈ ℋ ) → ((A −v B) = 0v ↔ A = B))
Theorem	hvsub0t 5041	Subtraction of a zero vector.
⊢ (A ∈ ℋ → (A −v 0v) = A)
Theorem	hvsubaddt 5042	Relationship between vector subtraction and addition.
⊢ ((A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ) → ((A −v B) = C ↔ (B +v C) = A))
Axiom	ax-hicl 5043	Closure of inner product.
⊢ ((A ∈ ℋ ∧ B ∈ ℋ ) → (A ·i B) ∈ ℂ)
Theorem	hicl 5044	Closure inference for inner product.
⊢ A ∈ ℋ    &   ⊢ B ∈ ℋ    ⇒   ⊢ (A ·i B) ∈ ℂ
Axiom	ax-his1 5045	Conjugate law for inner product. Postulate (S1) of [Beran] p. 95. Note that ∗ ‘x is the complex conjugate cjvalt 4799 of x. In the literature, the inner product of A and B is usually written ⟨A, B⟩ but our operation notation allows us to use existing theorems about operations and also eliminates ambiguity with the definition of an ordered pair df-op 1815.
⊢ ((A ∈ ℋ ∧ B ∈ ℋ ) → (A ·i B) = (∗ ‘(B ·i A)))
Axiom	ax-his2 5046	Distributive law for inner product. Postulate (S2) of [Beran] p. 95.
⊢ ((A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ) → ((A +v B) ·i C) = ((A ·i C) + (B ·i C)))
Axiom	ax-his3 5047	Associative law for inner product. Postulate (S3) of [Beran] p. 95.
⊢ ((A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ ) → ((A ·s B) ·i C) = (A · (B ·i C)))
Axiom	ax-his4 5048	Identity law for inner product. Postulate (S4) of [Beran] p. 95.
⊢ ((A ∈ ℋ ∧ A ≠ 0v) → 0 < (A ·i A))
Theorem	axhis42 5049	Identity law for inner product. Postulate (S4) of [Beran] p. 95.
⊢ ((A ∈ ℋ ∧ ¬ A = 0v) → 0 < (A ·i A))
Theorem	his5 5050	Associative law for inner product. Lemma 3.1(S5) of [Beran] p. 95.
⊢ ((A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ ) → (B ·i (A ·s C)) = ((∗ ‘A) · (B ·i C)))
Theorem	his7 5051	Distributive law for inner product. Lemma 3.1(S7) of [Beran] p. 95.
⊢ ((A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ) → (A ·i (B +v C)) = ((A ·i B) + (A ·i C)))
Theorem	his2subt 5052	Distributive law for inner product of vector subtraction.
⊢ ((A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ) → ((A −v B) ·i C) = ((A ·i C) − (B ·i C)))
Theorem	hiidrclt 5053	Real closure of inner product with self.
⊢ (A ∈ ℋ → (A ·i A) ∈ ℝ)
Theorem	hizer1t 5054	Inner product with the 0 vector.
⊢ (A ∈ ℋ → (0v ·i A) = 0)
Theorem	hizer2t 5055	Inner product with the 0 vector.
⊢ (A ∈ ℋ → (A ·i 0v) = 0)
Theorem	hiidge0t 5056	Inner product with self is not negative.
⊢ (A ∈ ℋ → 0 ≤ (A ·i A))
Theorem	his6 5057	Zero inner product with self means vector is zero. Lemma 3.1(S6) of [Beran] p. 95.
⊢ (A ∈ ℋ → ((A ·i A) = 0 ↔ A = 0v))
Theorem	hial0 5058	A vector whose inner product is always zero is zero.
⊢ (A ∈ ℋ → (∀x ∈ ℋ (A ·i x) = 0 ↔ A = 0v))
Theorem	hi2eqt 5059	Lemma used to prove equality of vectors.
⊢ ((A ∈ ℋ ∧ B ∈ ℋ ) → ((A ·i (A −v B)) = (B ·i (A −v B)) ↔ A = B))
Theorem	hial2eqt 5060	Two vectors whose inner product is always equal are equal.
⊢ ((A ∈ ℋ ∧ B ∈ ℋ ) → (∀x ∈ ℋ (A ·i x) = (B ·i x) ↔ A = B))
Theorem	orthcom 5061	Orthogonality commutes.
⊢ ((A ∈ ℋ ∧ B ∈ ℋ ) → ((A ·i B) = 0 ↔ (B ·i A) = 0))
Theorem	normlem0 5062	Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97.
⊢ S ∈ ℂ    &   ⊢ F ∈ ℋ    &   ⊢ G ∈ ℋ    ⇒   ⊢ ((F −v (S ·s G)) ·i (F −v (S ·s G))) = (((F ·i F) + (-(∗ ‘S) · (F ·i G))) + ((-S · (G ·i F)) + ((S · (∗ ‘S)) · (G ·i G))))
Theorem	normlem1 5063	Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97.
⊢ S ∈ ℂ    &   ⊢ F ∈ ℋ    &   ⊢ G ∈ ℋ    &   ⊢ R ∈ ℝ    &   ⊢ (abs ‘S) = 1    ⇒   ⊢ ((F −v ((S · R) ·s G)) ·i (F −v ((S · R) ·s G))) = (((F ·i F) + (((∗ ‘S) · -R) · (F ·i G))) + (((S · -R) · (G ·i F)) + ((R↑2) · (G ·i G))))
Theorem	normlem2 5064	Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97.
⊢ S ∈ ℂ    &   ⊢ F ∈ ℋ    &   ⊢ G ∈ ℋ    &   ⊢ B = -(((∗ ‘S) · (F ·i G)) + (S · (G ·i F)))    ⇒   ⊢ B ∈ ℝ
Theorem	normlem3 5065	Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97.
⊢ S ∈ ℂ    &   ⊢ F ∈ ℋ    &   ⊢ G ∈ ℋ    &   ⊢ B = -(((∗ ‘S) · (F ·i G)) + (S · (G ·i F)))    &   ⊢ A = (G ·i G)    &   ⊢ C = (F ·i F)    &   ⊢ R ∈ ℝ    ⇒   ⊢ (((A · (R↑2)) + (B · R)) + C) = (((F ·i F) + (((∗ ‘S) · -R) · (F ·i G))) + (((S · -R) · (G ·i F)) + ((R↑2) · (G ·i G))))
Theorem	normlem4 5066	Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97.
⊢ S ∈ ℂ    &   ⊢ F ∈ ℋ    &   ⊢ G ∈ ℋ    &   ⊢ B = -(((∗ ‘S) · (F ·i G)) + (S · (G ·i F)))    &   ⊢ A = (G ·i G)    &   ⊢ C = (F ·i F)    &   ⊢ R ∈ ℝ    &   ⊢ (abs ‘S) = 1    ⇒   ⊢ ((F −v ((S · R) ·s G)) ·i (F −v ((S · R) ·s G))) = (((A · (R↑2)) + (B · R)) + C)
Theorem	normlem5 5067	Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97.
⊢ S ∈ ℂ    &   ⊢ F ∈ ℋ    &   ⊢ G ∈ ℋ    &   ⊢ B = -(((∗ ‘S) · (F ·i G)) + (S · (G ·i F)))    &   ⊢ A = (G ·i G)    &   ⊢ C = (F ·i F)    &   ⊢ R ∈ ℝ    &   ⊢ (abs ‘S) = 1    ⇒   ⊢ 0 ≤ (((A · (R↑2)) + (B · R)) + C)
Theorem	normlem6 5068	Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97.
⊢ S ∈ ℂ    &   ⊢ F ∈ ℋ    &   ⊢ G ∈ ℋ    &   ⊢ B = -(((∗ ‘S) · (F ·i G)) + (S · (G ·i F)))    &   ⊢ A = (G ·i G)    &   ⊢ C = (F ·i F)    &   ⊢ (abs ‘S) = 1    ⇒   ⊢ (abs ‘B) ≤ (2 · ((√ ‘A) · (√ ‘C)))
Theorem	normlem7 5069	Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97.
⊢ S ∈ ℂ    &   ⊢ F ∈ ℋ    &   ⊢ G ∈ ℋ    &   ⊢ (abs ‘S) = 1    ⇒   ⊢ (((∗ ‘S) · (F ·i G)) + (S · (G ·i F))) ≤ (2 · ((√ ‘(G ·i G)) · (√ ‘(F ·i F))))
Theorem	normlem9 5070	Lemma used to derive properties of norm. Part of Remark 3.4(B) of [Beran] p. 98.
⊢ A ∈ ℋ    &   ⊢ B ∈ ℋ    ⇒   ⊢ ((A +v B) ·i (A +v B)) = (((A ·i A) + (B ·i B)) + ((A ·i B) + (B ·i A)))
Theorem	normlem8 5071	Lemma used to derive properties of norm. Part of Remark 3.4(B) of [Beran] p. 98.
⊢ A ∈ ℋ    &   ⊢ B ∈ ℋ    ⇒   ⊢ ((A −v B) ·i (A −v B)) = (((A ·i A) + (B ·i B)) − ((A ·i B) + (B ·i A)))
Theorem	normlem7t 5072	Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97.
⊢ A ∈ ℋ    &   ⊢ B ∈ ℋ    ⇒   ⊢ ((S ∈ ℂ ∧ (abs ‘S) = 1) → (((∗ ‘S) · (A ·i B)) + (S · (B ·i A))) ≤ (2 · ((√ ‘(B ·i B)) · (√ ‘(A ·i A)))))
Theorem	bcseq 5073	Equality case of Bunjakovaskij-Cauchy-Schwarz inequality. Specifically, in the equality case the two vectors are collinear. Compare bcs 5101.
⊢ A ∈ ℋ    &   ⊢ B ∈ ℋ    ⇒   ⊢ (((A ·i B) · (B ·i A)) = ((A ·i A) · (B ·i B)) ↔ ((B ·i B) ·s A) = ((A ·i B) ·s B))
Definition	df-hnorm 5074	Define the function for the norm of a vector of Hilbert space. See normvalt 5075 for its value and normclt 5076 for its closure. Theorems norm-i 5083, norm-ii 5086, and norm-iii 5087 show it has the expected properties of a norm. In the literature, the norm of A is usually written "|| A ||", but we use function notation to take advantage of our existing theorems about functions. Definition of norm in [Beran] p. 96.
⊢ norm = {⟨x, y⟩∣(x ∈ ℋ ∧ y = (√ ‘(x ·i x)))}
Theorem	normvalt 5075	The value of the norm of a vector in Hilbert space. Definition of norm in [Beran] p. 96. In the literature, the norm of A is usually written as "|| A ||", but we use function value notation to take advantage of our existing theorems about functions.
⊢ (A ∈ ℋ → (norm ‘A) = (√ ‘(A ·i A)))
Theorem	normclt 5076	Real closure of the norm of a vector.
⊢ (A ∈ ℋ → (norm ‘A) ∈ ℝ)
Theorem	normge0t 5077	The norm of a vector is nonnegative.
⊢ (A ∈ ℋ → 0 ≤ (norm ‘A))
Theorem	normgt0t 5078	The norm of non-zero vector is positive.
⊢ (A ∈ ℋ → (¬ A = 0v ↔ 0 < (norm ‘A)))
Theorem	norm0 5079	The norm of a zero vector.
⊢ (norm ‘0v) = 0
Theorem	norm-it 5080	Theorem 3.3(i) of [Beran] p. 97.
⊢ (A ∈ ℋ → ((norm ‘A) = 0 ↔ A = 0v))
Theorem	normcl 5081	Real closure of the norm of a vector.
⊢ A ∈ ℋ    ⇒   ⊢ (norm ‘A) ∈ ℝ
Theorem	normsq 5082	The square of a norm.
⊢ A ∈ ℋ    ⇒   ⊢ ((norm ‘A)↑2) = (A ·i A)
Theorem	norm-i 5083	Theorem 3.3(i) of [Beran] p. 97.
⊢ A ∈ ℋ    ⇒   ⊢ ((norm ‘A) = 0 ↔ A = 0v)
Theorem	normsub0 5084	Two vectors are equal iff the norm of their difference is zero.
⊢ A ∈ ℋ    &   ⊢ B ∈ ℋ    ⇒   ⊢ ((norm ‘(A −v B)) = 0 ↔ A = B)
Theorem	normsub0t 5085	Two vectors are equal iff the norm of their difference is zero.
⊢ ((A ∈ ℋ ∧ B ∈ ℋ ) → ((norm ‘(A −v B)) = 0 ↔ A = B))
Theorem	norm-ii 5086	Triangle inequality for norms. Theorem 3.3(ii) of [Beran] p. 97.
⊢ A ∈ ℋ    &   ⊢ B ∈ ℋ    ⇒   ⊢ (norm ‘(A +v B)) ≤ ((norm ‘A) + (norm ‘B))
Theorem	norm-iii 5087	Theorem 3.3(iii) of [Beran] p. 97.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℋ    ⇒   ⊢ (norm ‘(A ·s B)) = ((abs ‘A) · (norm ‘B))
Theorem	norm-iiit 5088	Theorem 3.3(iii) of [Beran] p. 97.
⊢ ((A ∈ ℂ ∧ B ∈ ℋ ) → (norm ‘(A ·s B)) = ((abs ‘A) · (norm ‘B)))
Theorem	normsub 5089	Negative doesn't change the norm of a Hilbert space vector.
⊢ A ∈ ℋ    &   ⊢ B ∈ ℋ    ⇒   ⊢ (norm ‘(A −v B)) = (norm ‘(B −v A))
Theorem	normpyth 5090	Analogy to Pythagorean theorem for orthogonal vectors. Remark 3.4(C) of [Beran] p. 98.
⊢ A ∈ ℋ    &   ⊢ B ∈ ℋ    ⇒   ⊢ ((A ·i B) = 0 → ((norm ‘(A +v B))↑2) = (((norm ‘A)↑2) + ((norm ‘B)↑2)))
Theorem	normsubt 5091	Swapping order of subtraction doesn't change the norm of a vector.
⊢ ((A ∈ ℋ ∧ B ∈ ℋ ) → (norm ‘(A −v B)) = (norm ‘(B −v A)))
Theorem	normpytht 5092	Analogy to Pythagorean theorem for orthogonal vectors. Remark 3.4(C) of [Beran] p. 98.
⊢ ((A ∈ ℋ ∧ B ∈ ℋ ) → ((A ·i B) = 0 → ((norm ‘(A +v B))↑2) = (((norm ‘A)↑2) + ((norm ‘B)↑2))))
Theorem	normpyct 5093	Corollary to Pythagorean theorem for orthogonal vectors. Remark 3.4(C) of [Beran] p. 98.
⊢ ((A ∈ ℋ ∧ B ∈ ℋ ) → ((A ·i B) = 0 → (norm ‘A) ≤ (norm ‘(A +v B))))
Theorem	norm3dif 5094	Norm of differences around common element. Part of Lemma 3.6 of [Beran] p. 101.
⊢ A ∈ ℋ    &   ⊢ B ∈ ℋ    &   ⊢ C ∈ ℋ    ⇒   ⊢ (norm ‘(A −v B)) ≤ ((norm ‘(A −v C)) + (norm ‘(C −v B)))
Theorem	norm3adif 5095	Norm of differences around common element. Part of Lemma 3.6 of [Beran] p. 101.
⊢ A ∈ ℋ    &   ⊢ B ∈ ℋ    &   ⊢ C ∈ ℋ    ⇒   ⊢ (abs ‘((norm ‘(A −v C)) − (norm ‘(B −v C)))) ≤ (norm ‘(A −v B))
Theorem	norm3lem 5096	Lemma involving norm of differences in Hilbert space.
⊢ A ∈ ℋ    &   ⊢ B ∈ ℋ    &   ⊢ C ∈ ℋ    &   ⊢ D ∈ ℝ    ⇒   ⊢ (((norm ‘(A −v C)) < (D / 2) ∧ (norm ‘(C −v B)) < (D / 2)) → (norm ‘(A −v B)) < D)
Theorem	norm3lemt 5097	Lemma involving norm of differences in Hilbert space.
⊢ (((A ∈ ℋ ∧ B ∈ ℋ ) ∧ (C ∈ ℋ ∧ D ∈ ℝ)) → (((norm ‘(A −v C)) < (D / 2) ∧ (norm ‘(C −v B)) < (D / 2)) → (norm ‘(A −v B)) < D))
Theorem	norm3adift 5098	Norm of differences around common element. Part of Lemma 3.6 of [Beran] p. 101.
⊢ C ∈ ℋ    ⇒   ⊢ ((A ∈ ℋ ∧ B ∈ ℋ ) → (abs ‘((norm ‘(A −v C)) − (norm ‘(B −v C)))) ≤ (norm ‘(A −v B)))
Theorem	normpar 5099	Parallelogram law for norms. Remark 3.4(B) of [Beran] p. 98.
⊢ A ∈ ℋ    &   ⊢ B ∈ ℋ    ⇒   ⊢ (((norm ‘(A −v B))↑2) + ((norm ‘(A +v B))↑2)) = ((2 · ((norm ‘A)↑2)) + (2 · ((norm ‘B)↑2)))
Theorem	normpar2 5100	Corollary of parallelogram law for norms. Part of Lemma 3.6 of [Beran] p. 100.
⊢ A ∈ ℋ    &   ⊢ B ∈ ℋ    &   ⊢ C ∈ ℋ    ⇒   ⊢ ((norm ‘(A −v B))↑2) = (((2 · ((norm ‘(A −v C))↑2)) + (2 · ((norm ‘(B −v C))↑2))) − ((norm ‘((A +v B) −v (2 ·s C)))↑2))