P. 290 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 28901-29000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nvsz 28901	Anything times the zero vector is the zero vector. (Contributed by NM, 28-Nov-2007.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.)
⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ ℂ) → (𝐴𝑆𝑍) = 𝑍)
Theorem	nvinv 28902	Minus 1 times a vector is the underlying group's inverse element. Equation 2 of [Kreyszig] p. 51. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑀 = (inv‘𝐺)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (-1𝑆𝐴) = (𝑀‘𝐴))
Theorem	nvinvfval 28903	Function for the negative of a vector on a normed complex vector space, in terms of the underlying addition group inverse. (We currently do not have a separate notation for the negative of a vector.) (Contributed by NM, 27-Mar-2008.) (New usage is discouraged.)
⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑁 = (𝑆 ∘ ◡(2nd ↾ ({-1} × V)))    ⇒   ⊢ (𝑈 ∈ NrmCVec → 𝑁 = (inv‘𝐺))
Theorem	nvm 28904	Vector subtraction in terms of group division operation. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    &   ⊢ 𝑁 = ( /𝑔 ‘𝐺)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑀𝐵) = (𝐴𝑁𝐵))
Theorem	nvmval 28905	Value of vector subtraction on a normed complex vector space. (Contributed by NM, 11-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑀𝐵) = (𝐴𝐺(-1𝑆𝐵)))
Theorem	nvmval2 28906	Value of vector subtraction on a normed complex vector space. (Contributed by Mario Carneiro, 19-Nov-2013.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑀𝐵) = ((-1𝑆𝐵)𝐺𝐴))
Theorem	nvmfval 28907*	Value of the function for the vector subtraction operation on a normed complex vector space. (Contributed by NM, 11-Sep-2007.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    ⇒   ⊢ (𝑈 ∈ NrmCVec → 𝑀 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (𝑥𝐺(-1𝑆𝑦))))
Theorem	nvmf 28908	Mapping for the vector subtraction operation. (Contributed by NM, 11-Sep-2007.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    ⇒   ⊢ (𝑈 ∈ NrmCVec → 𝑀:(𝑋 × 𝑋)⟶𝑋)
Theorem	nvmcl 28909	Closure law for the vector subtraction operation of a normed complex vector space. (Contributed by NM, 11-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑀𝐵) ∈ 𝑋)
Theorem	nvnnncan1 28910	Cancellation law for vector subtraction. (nnncan1 11187 analog.) (Contributed by NM, 7-Mar-2008.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝑀𝐵)𝑀(𝐴𝑀𝐶)) = (𝐶𝑀𝐵))
Theorem	nvmdi 28911	Distributive law for scalar product over subtraction. (Contributed by NM, 14-Feb-2008.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝑆(𝐵𝑀𝐶)) = ((𝐴𝑆𝐵)𝑀(𝐴𝑆𝐶)))
Theorem	nvnegneg 28912	Double negative of a vector. (Contributed by NM, 4-Dec-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (-1𝑆(-1𝑆𝐴)) = 𝐴)
Theorem	nvmul0or 28913	If a scalar product is zero, one of its factors must be zero. (Contributed by NM, 6-Dec-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋) → ((𝐴𝑆𝐵) = 𝑍 ↔ (𝐴 = 0 ∨ 𝐵 = 𝑍)))
Theorem	nvrinv 28914	A vector minus itself. (Contributed by NM, 4-Dec-2007.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝐴𝐺(-1𝑆𝐴)) = 𝑍)
Theorem	nvlinv 28915	Minus a vector plus itself. (Contributed by NM, 4-Dec-2007.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → ((-1𝑆𝐴)𝐺𝐴) = 𝑍)
Theorem	nvpncan2 28916	Cancellation law for vector subtraction. (Contributed by NM, 27-Dec-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴𝐺𝐵)𝑀𝐴) = 𝐵)
Theorem	nvpncan 28917	Cancellation law for vector subtraction. (Contributed by NM, 24-Jan-2008.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴𝐺𝐵)𝑀𝐵) = 𝐴)
Theorem	nvaddsub 28918	Commutative/associative law for vector addition and subtraction. (Contributed by NM, 24-Jan-2008.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝑀𝐶) = ((𝐴𝑀𝐶)𝐺𝐵))
Theorem	nvnpcan 28919	Cancellation law for a normed complex vector space. (Contributed by NM, 24-Jan-2008.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴𝑀𝐵)𝐺𝐵) = 𝐴)
Theorem	nvaddsub4 28920	Rearrangement of 4 terms in a mixed vector addition and subtraction. (Contributed by NM, 8-Feb-2008.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝑀(𝐶𝐺𝐷)) = ((𝐴𝑀𝐶)𝐺(𝐵𝑀𝐷)))
Theorem	nvmeq0 28921	The difference between two vectors is zero iff they are equal. (Contributed by NM, 24-Jan-2008.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴𝑀𝐵) = 𝑍 ↔ 𝐴 = 𝐵))
Theorem	nvmid 28922	A vector minus itself is the zero vector. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝐴𝑀𝐴) = 𝑍)
Theorem	nvf 28923	Mapping for the norm function. (Contributed by NM, 11-Nov-2006.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    ⇒   ⊢ (𝑈 ∈ NrmCVec → 𝑁:𝑋⟶ℝ)
Theorem	nvcl 28924	The norm of a normed complex vector space is a real number. (Contributed by NM, 24-Nov-2006.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) ∈ ℝ)
Theorem	nvcli 28925	The norm of a normed complex vector space is a real number. (Contributed by NM, 20-Apr-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑈 ∈ NrmCVec    &   ⊢ 𝐴 ∈ 𝑋    ⇒   ⊢ (𝑁‘𝐴) ∈ ℝ
Theorem	nvs 28926	Proportionality property of the norm of a scalar product in a normed complex vector space. (Contributed by NM, 11-Nov-2006.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋) → (𝑁‘(𝐴𝑆𝐵)) = ((abs‘𝐴) · (𝑁‘𝐵)))
Theorem	nvsge0 28927	The norm of a scalar product with a nonnegative real. (Contributed by NM, 1-Jan-2008.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝐵 ∈ 𝑋) → (𝑁‘(𝐴𝑆𝐵)) = (𝐴 · (𝑁‘𝐵)))
Theorem	nvm1 28928	The norm of the negative of a vector. (Contributed by NM, 28-Nov-2006.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝑁‘(-1𝑆𝐴)) = (𝑁‘𝐴))
Theorem	nvdif 28929	The norm of the difference between two vectors. (Contributed by NM, 1-Dec-2006.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑁‘(𝐴𝐺(-1𝑆𝐵))) = (𝑁‘(𝐵𝐺(-1𝑆𝐴))))
Theorem	nvpi 28930	The norm of a vector plus the imaginary scalar product of another. (Contributed by NM, 2-Feb-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑁‘(𝐴𝐺(i𝑆𝐵))) = (𝑁‘(𝐵𝐺(-i𝑆𝐴))))
Theorem	nvz0 28931	The norm of a zero vector is zero. (Contributed by NM, 24-Nov-2006.) (New usage is discouraged.)
⊢ 𝑍 = (0vec‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    ⇒   ⊢ (𝑈 ∈ NrmCVec → (𝑁‘𝑍) = 0)
Theorem	nvz 28932	The norm of a vector is zero iff the vector is zero. First part of Problem 2 of [Kreyszig] p. 64. (Contributed by NM, 24-Nov-2006.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → ((𝑁‘𝐴) = 0 ↔ 𝐴 = 𝑍))
Theorem	nvtri 28933	Triangle inequality for the norm of a normed complex vector space. (Contributed by NM, 11-Nov-2006.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑁‘(𝐴𝐺𝐵)) ≤ ((𝑁‘𝐴) + (𝑁‘𝐵)))
Theorem	nvmtri 28934	Triangle inequality for the norm of a vector difference. (Contributed by NM, 27-Dec-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑁‘(𝐴𝑀𝐵)) ≤ ((𝑁‘𝐴) + (𝑁‘𝐵)))
Theorem	nvabs 28935	Norm difference property of a normed complex vector space. Problem 3 of [Kreyszig] p. 64. (Contributed by NM, 4-Dec-2006.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (abs‘((𝑁‘𝐴) − (𝑁‘𝐵))) ≤ (𝑁‘(𝐴𝐺(-1𝑆𝐵))))
Theorem	nvge0 28936	The norm of a normed complex vector space is nonnegative. Second part of Problem 2 of [Kreyszig] p. 64. (Contributed by NM, 28-Nov-2006.) (Proof shortened by AV, 10-Jul-2022.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → 0 ≤ (𝑁‘𝐴))
Theorem	nvgt0 28937	A nonzero norm is positive. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝐴 ≠ 𝑍 ↔ 0 < (𝑁‘𝐴)))
Theorem	nv1 28938	From any nonzero vector, construct a vector whose norm is one. (Contributed by NM, 6-Dec-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ 𝑍) → (𝑁‘((1 / (𝑁‘𝐴))𝑆𝐴)) = 1)
Theorem	nvop 28939	A complex inner product space in terms of ordered pair components. (Contributed by NM, 11-Sep-2007.) (New usage is discouraged.)
⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    ⇒   ⊢ (𝑈 ∈ NrmCVec → 𝑈 = ⟨⟨𝐺, 𝑆⟩, 𝑁⟩)
18.3.2  Examples of normed complex vector spaces
Theorem	cnnv 28940	The set of complex numbers is a normed complex vector space. The vector operation is +, the scalar product is ·, and the norm function is abs. (Contributed by Steve Rodriguez, 3-Dec-2006.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ + , · ⟩, abs⟩    ⇒   ⊢ 𝑈 ∈ NrmCVec
Theorem	cnnvg 28941	The vector addition (group) operation of the normed complex vector space of complex numbers. (Contributed by NM, 12-Jan-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ + , · ⟩, abs⟩    ⇒   ⊢ + = ( +𝑣 ‘𝑈)
Theorem	cnnvba 28942	The base set of the normed complex vector space of complex numbers. (Contributed by NM, 7-Nov-2007.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ + , · ⟩, abs⟩    ⇒   ⊢ ℂ = (BaseSet‘𝑈)
Theorem	cnnvs 28943	The scalar product operation of the normed complex vector space of complex numbers. (Contributed by NM, 12-Jan-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ + , · ⟩, abs⟩    ⇒   ⊢ · = ( ·𝑠OLD ‘𝑈)
Theorem	cnnvnm 28944	The norm operation of the normed complex vector space of complex numbers. (Contributed by NM, 12-Jan-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ + , · ⟩, abs⟩    ⇒   ⊢ abs = (normCV‘𝑈)
Theorem	cnnvm 28945	The vector subtraction operation of the normed complex vector space of complex numbers. (Contributed by NM, 12-Jan-2008.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ + , · ⟩, abs⟩    ⇒   ⊢ − = ( −𝑣 ‘𝑈)
Theorem	elimnv 28946	Hypothesis elimination lemma for normed complex vector spaces to assist weak deduction theorem. (Contributed by NM, 16-May-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑈)    &   ⊢ 𝑈 ∈ NrmCVec    ⇒   ⊢ if(𝐴 ∈ 𝑋, 𝐴, 𝑍) ∈ 𝑋
Theorem	elimnvu 28947	Hypothesis elimination lemma for normed complex vector spaces to assist weak deduction theorem. (Contributed by NM, 16-May-2007.) (New usage is discouraged.)
⊢ if(𝑈 ∈ NrmCVec, 𝑈, ⟨⟨ + , · ⟩, abs⟩) ∈ NrmCVec
18.3.3  Induced metric of a normed complex vector space
Theorem	imsval 28948	Value of the induced metric of a normed complex vector space. (Contributed by NM, 11-Sep-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
⊢ 𝑀 = ( −𝑣 ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝐷 = (IndMet‘𝑈)    ⇒   ⊢ (𝑈 ∈ NrmCVec → 𝐷 = (𝑁 ∘ 𝑀))
Theorem	imsdval 28949	Value of the induced metric (distance function) of a normed complex vector space. Equation 1 of [Kreyszig] p. 59. (Contributed by NM, 11-Sep-2007.) (Revised by Mario Carneiro, 27-Dec-2014.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝐷 = (IndMet‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = (𝑁‘(𝐴𝑀𝐵)))
Theorem	imsdval2 28950	Value of the distance function of the induced metric of a normed complex vector space. Equation 1 of [Kreyszig] p. 59. (Contributed by NM, 28-Nov-2006.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝐷 = (IndMet‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = (𝑁‘(𝐴𝐺(-1𝑆𝐵))))
Theorem	nvnd 28951	The norm of a normed complex vector space expressed in terms of the distance function of its induced metric. Problem 1 of [Kreyszig] p. 63. (Contributed by NM, 4-Dec-2006.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝐷 = (IndMet‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) = (𝐴𝐷𝑍))
Theorem	imsdf 28952	Mapping for the induced metric distance function of a normed complex vector space. (Contributed by NM, 29-Nov-2006.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐷 = (IndMet‘𝑈)    ⇒   ⊢ (𝑈 ∈ NrmCVec → 𝐷:(𝑋 × 𝑋)⟶ℝ)
Theorem	imsmetlem 28953	Lemma for imsmet 28954. (Contributed by NM, 29-Nov-2006.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑀 = (inv‘𝐺)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝐷 = (IndMet‘𝑈)    &   ⊢ 𝑈 ∈ NrmCVec    ⇒   ⊢ 𝐷 ∈ (Met‘𝑋)
Theorem	imsmet 28954	The induced metric of a normed complex vector space is a metric space. Part of Definition 2.2-1 of [Kreyszig] p. 58. (Contributed by NM, 4-Dec-2006.) (Revised by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐷 = (IndMet‘𝑈)    ⇒   ⊢ (𝑈 ∈ NrmCVec → 𝐷 ∈ (Met‘𝑋))
Theorem	imsxmet 28955	The induced metric of a normed complex vector space is an extended metric space. (Contributed by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐷 = (IndMet‘𝑈)    ⇒   ⊢ (𝑈 ∈ NrmCVec → 𝐷 ∈ (∞Met‘𝑋))
Theorem	cnims 28956	The metric induced on the complex numbers. cnmet 23841 proves that it is a metric. (Contributed by Steve Rodriguez, 5-Dec-2006.) (Revised by NM, 15-Jan-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ + , · ⟩, abs⟩    &   ⊢ 𝐷 = (abs ∘ − )    ⇒   ⊢ 𝐷 = (IndMet‘𝑈)
Theorem	vacn 28957	Vector addition is jointly continuous in both arguments. (Contributed by Jeff Hankins, 16-Jun-2009.) (Revised by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.)
⊢ 𝐶 = (IndMet‘𝑈)    &   ⊢ 𝐽 = (MetOpen‘𝐶)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    ⇒   ⊢ (𝑈 ∈ NrmCVec → 𝐺 ∈ ((𝐽 ×t 𝐽) Cn 𝐽))
Theorem	nmcvcn 28958	The norm of a normed complex vector space is a continuous function. (Contributed by NM, 16-May-2007.) (Proof shortened by Mario Carneiro, 10-Jan-2014.) (New usage is discouraged.)
⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝐶 = (IndMet‘𝑈)    &   ⊢ 𝐽 = (MetOpen‘𝐶)    &   ⊢ 𝐾 = (topGen‘ran (,))    ⇒   ⊢ (𝑈 ∈ NrmCVec → 𝑁 ∈ (𝐽 Cn 𝐾))
Theorem	nmcnc 28959	The norm of a normed complex vector space is a continuous function to ℂ. (For ℝ, see nmcvcn 28958.) (Contributed by NM, 12-Aug-2007.) (New usage is discouraged.)
⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝐶 = (IndMet‘𝑈)    &   ⊢ 𝐽 = (MetOpen‘𝐶)    &   ⊢ 𝐾 = (TopOpen‘ℂfld)    ⇒   ⊢ (𝑈 ∈ NrmCVec → 𝑁 ∈ (𝐽 Cn 𝐾))
Theorem	smcnlem 28960*	Lemma for smcn 28961. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.)
⊢ 𝐶 = (IndMet‘𝑈)    &   ⊢ 𝐽 = (MetOpen‘𝐶)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝐾 = (TopOpen‘ℂfld)    &   ⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑈 ∈ NrmCVec    &   ⊢ 𝑇 = (1 / (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)))    ⇒   ⊢ 𝑆 ∈ ((𝐾 ×t 𝐽) Cn 𝐽)
Theorem	smcn 28961	Scalar multiplication is jointly continuous in both arguments. (Contributed by NM, 16-Jun-2009.) (Revised by Mario Carneiro, 5-May-2014.) (New usage is discouraged.)
⊢ 𝐶 = (IndMet‘𝑈)    &   ⊢ 𝐽 = (MetOpen‘𝐶)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝐾 = (TopOpen‘ℂfld)    ⇒   ⊢ (𝑈 ∈ NrmCVec → 𝑆 ∈ ((𝐾 ×t 𝐽) Cn 𝐽))
Theorem	vmcn 28962	Vector subtraction is jointly continuous in both arguments. (Contributed by Mario Carneiro, 6-May-2014.) (New usage is discouraged.)
⊢ 𝐶 = (IndMet‘𝑈)    &   ⊢ 𝐽 = (MetOpen‘𝐶)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    ⇒   ⊢ (𝑈 ∈ NrmCVec → 𝑀 ∈ ((𝐽 ×t 𝐽) Cn 𝐽))
18.3.4  Inner product
Syntax	cdip 28963	Extend class notation with the class inner product functions.
class ·𝑖OLD
Definition	df-dip 28964*	Define a function that maps a normed complex vector space to its inner product operation in case its norm satisfies the parallelogram identity (otherwise the operation is still defined, but not meaningful). Based on Exercise 4(a) of [ReedSimon] p. 63 and Theorem 6.44 of [Ponnusamy] p. 361. Vector addition is (1st ‘𝑤), the scalar product is (2nd ‘𝑤), and the norm is 𝑛. (Contributed by NM, 10-Apr-2007.) (New usage is discouraged.)
⊢ ·𝑖OLD = (𝑢 ∈ NrmCVec ↦ (𝑥 ∈ (BaseSet‘𝑢), 𝑦 ∈ (BaseSet‘𝑢) ↦ (Σ𝑘 ∈ (1...4)((i↑𝑘) · (((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD ‘𝑢)𝑦)))↑2)) / 4)))
Theorem	dipfval 28965*	The inner product function on a normed complex vector space. The definition is meaningful for vector spaces that are also inner product spaces, i.e. satisfy the parallelogram law. (Contributed by NM, 10-Apr-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ (𝑈 ∈ NrmCVec → 𝑃 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (Σ𝑘 ∈ (1...4)((i↑𝑘) · ((𝑁‘(𝑥𝐺((i↑𝑘)𝑆𝑦)))↑2)) / 4)))
Theorem	ipval 28966*	Value of the inner product. The definition is meaningful for normed complex vector spaces that are also inner product spaces, i.e. satisfy the parallelogram law, although for convenience we define it for any normed complex vector space. The vector (group) addition operation is 𝐺, the scalar product is 𝑆, the norm is 𝑁, and the set of vectors is 𝑋. Equation 6.45 of [Ponnusamy] p. 361. (Contributed by NM, 31-Jan-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑃𝐵) = (Σ𝑘 ∈ (1...4)((i↑𝑘) · ((𝑁‘(𝐴𝐺((i↑𝑘)𝑆𝐵)))↑2)) / 4))
Theorem	ipval2lem2 28967	Lemma for ipval3 28972. (Contributed by NM, 1-Feb-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ (((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝐶 ∈ ℂ) → ((𝑁‘(𝐴𝐺(𝐶𝑆𝐵)))↑2) ∈ ℝ)
Theorem	ipval2lem3 28968	Lemma for ipval3 28972. (Contributed by NM, 1-Feb-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑁‘(𝐴𝐺𝐵))↑2) ∈ ℝ)
Theorem	ipval2lem4 28969	Lemma for ipval3 28972. (Contributed by NM, 1-Feb-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ (((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝐶 ∈ ℂ) → ((𝑁‘(𝐴𝐺(𝐶𝑆𝐵)))↑2) ∈ ℂ)
Theorem	ipval2 28970	Expansion of the inner product value ipval 28966. (Contributed by NM, 31-Jan-2007.) (Revised by Mario Carneiro, 5-May-2014.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑃𝐵) = (((((𝑁‘(𝐴𝐺𝐵))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐵)))↑2)) + (i · (((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐵)))↑2)))) / 4))
Theorem	4ipval2 28971	Four times the inner product value ipval3 28972, useful for simplifying certain proofs. (Contributed by NM, 10-Apr-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (4 · (𝐴𝑃𝐵)) = ((((𝑁‘(𝐴𝐺𝐵))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐵)))↑2)) + (i · (((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐵)))↑2)))))
Theorem	ipval3 28972	Expansion of the inner product value ipval 28966. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑃𝐵) = (((((𝑁‘(𝐴𝐺𝐵))↑2) − ((𝑁‘(𝐴𝑀𝐵))↑2)) + (i · (((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2) − ((𝑁‘(𝐴𝑀(i𝑆𝐵)))↑2)))) / 4))
Theorem	ipidsq 28973	The inner product of a vector with itself is the square of the vector's norm. Equation I4 of [Ponnusamy] p. 362. (Contributed by NM, 1-Feb-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝐴𝑃𝐴) = ((𝑁‘𝐴)↑2))
Theorem	ipnm 28974	Norm expressed in terms of inner product. (Contributed by NM, 11-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) = (√‘(𝐴𝑃𝐴)))
Theorem	dipcl 28975	An inner product is a complex number. (Contributed by NM, 1-Feb-2007.) (Revised by Mario Carneiro, 5-May-2014.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑃𝐵) ∈ ℂ)
Theorem	ipf 28976	Mapping for the inner product operation. (Contributed by NM, 28-Jan-2008.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ (𝑈 ∈ NrmCVec → 𝑃:(𝑋 × 𝑋)⟶ℂ)
Theorem	dipcj 28977	The complex conjugate of an inner product reverses its arguments. Equation I1 of [Ponnusamy] p. 362. (Contributed by NM, 1-Feb-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (∗‘(𝐴𝑃𝐵)) = (𝐵𝑃𝐴))
Theorem	ipipcj 28978	An inner product times its conjugate. (Contributed by NM, 23-Nov-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴𝑃𝐵) · (𝐵𝑃𝐴)) = ((abs‘(𝐴𝑃𝐵))↑2))
Theorem	diporthcom 28979	Orthogonality (meaning inner product is 0) is commutative. (Contributed by NM, 17-Apr-2008.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴𝑃𝐵) = 0 ↔ (𝐵𝑃𝐴) = 0))
Theorem	dip0r 28980	Inner product with a zero second argument. (Contributed by NM, 5-Feb-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝐴𝑃𝑍) = 0)
Theorem	dip0l 28981	Inner product with a zero first argument. Part of proof of Theorem 6.44 of [Ponnusamy] p. 361. (Contributed by NM, 5-Feb-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝑍𝑃𝐴) = 0)
Theorem	ipz 28982	The inner product of a vector with itself is zero iff the vector is zero. Part of Definition 3.1-1 of [Kreyszig] p. 129. (Contributed by NM, 24-Jan-2008.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → ((𝐴𝑃𝐴) = 0 ↔ 𝐴 = 𝑍))
Theorem	dipcn 28983	Inner product is jointly continuous in both arguments. (Contributed by NM, 21-Aug-2007.) (Revised by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.)
⊢ 𝑃 = (·𝑖OLD‘𝑈)    &   ⊢ 𝐶 = (IndMet‘𝑈)    &   ⊢ 𝐽 = (MetOpen‘𝐶)    &   ⊢ 𝐾 = (TopOpen‘ℂfld)    ⇒   ⊢ (𝑈 ∈ NrmCVec → 𝑃 ∈ ((𝐽 ×t 𝐽) Cn 𝐾))
18.3.5  Subspaces
Syntax	css 28984	Extend class notation with the class of all subspaces of normed complex vector spaces.
class SubSp
Definition	df-ssp 28985*	Define the class of all subspaces of normed complex vector spaces. (Contributed by NM, 26-Jan-2008.) (New usage is discouraged.)
⊢ SubSp = (𝑢 ∈ NrmCVec ↦ {𝑤 ∈ NrmCVec ∣ (( +𝑣 ‘𝑤) ⊆ ( +𝑣 ‘𝑢) ∧ ( ·𝑠OLD ‘𝑤) ⊆ ( ·𝑠OLD ‘𝑢) ∧ (normCV‘𝑤) ⊆ (normCV‘𝑢))})
Theorem	sspval 28986*	The set of all subspaces of a normed complex vector space. (Contributed by NM, 26-Jan-2008.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝐻 = (SubSp‘𝑈)    ⇒   ⊢ (𝑈 ∈ NrmCVec → 𝐻 = {𝑤 ∈ NrmCVec ∣ (( +𝑣 ‘𝑤) ⊆ 𝐺 ∧ ( ·𝑠OLD ‘𝑤) ⊆ 𝑆 ∧ (normCV‘𝑤) ⊆ 𝑁)})
Theorem	isssp 28987	The predicate "is a subspace." (Contributed by NM, 26-Jan-2008.) (New usage is discouraged.)
⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝐹 = ( +𝑣 ‘𝑊)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑅 = ( ·𝑠OLD ‘𝑊)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑀 = (normCV‘𝑊)    &   ⊢ 𝐻 = (SubSp‘𝑈)    ⇒   ⊢ (𝑈 ∈ NrmCVec → (𝑊 ∈ 𝐻 ↔ (𝑊 ∈ NrmCVec ∧ (𝐹 ⊆ 𝐺 ∧ 𝑅 ⊆ 𝑆 ∧ 𝑀 ⊆ 𝑁))))
Theorem	sspid 28988	A normed complex vector space is a subspace of itself. (Contributed by NM, 8-Apr-2008.) (New usage is discouraged.)
⊢ 𝐻 = (SubSp‘𝑈)    ⇒   ⊢ (𝑈 ∈ NrmCVec → 𝑈 ∈ 𝐻)
Theorem	sspnv 28989	A subspace is a normed complex vector space. (Contributed by NM, 27-Jan-2008.) (New usage is discouraged.)
⊢ 𝐻 = (SubSp‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝑊 ∈ NrmCVec)
Theorem	sspba 28990	The base set of a subspace is included in the parent base set. (Contributed by NM, 27-Jan-2008.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝐻 = (SubSp‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝑌 ⊆ 𝑋)
Theorem	sspg 28991	Vector addition on a subspace is a restriction of vector addition on the parent space. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.)
⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝐹 = ( +𝑣 ‘𝑊)    &   ⊢ 𝐻 = (SubSp‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝐹 = (𝐺 ↾ (𝑌 × 𝑌)))
Theorem	sspgval 28992	Vector addition on a subspace in terms of vector addition on the parent space. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.)
⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝐹 = ( +𝑣 ‘𝑊)    &   ⊢ 𝐻 = (SubSp‘𝑈)    ⇒   ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) ∧ (𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌)) → (𝐴𝐹𝐵) = (𝐴𝐺𝐵))
Theorem	ssps 28993	Scalar multiplication on a subspace is a restriction of scalar multiplication on the parent space. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.)
⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑅 = ( ·𝑠OLD ‘𝑊)    &   ⊢ 𝐻 = (SubSp‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝑅 = (𝑆 ↾ (ℂ × 𝑌)))
Theorem	sspsval 28994	Scalar multiplication on a subspace in terms of scalar multiplication on the parent space. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.)
⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑅 = ( ·𝑠OLD ‘𝑊)    &   ⊢ 𝐻 = (SubSp‘𝑈)    ⇒   ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑌)) → (𝐴𝑅𝐵) = (𝐴𝑆𝐵))
Theorem	sspmlem 28995*	Lemma for sspm 28997 and others. (Contributed by NM, 1-Feb-2008.) (New usage is discouraged.)
⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝐻 = (SubSp‘𝑈)    &   ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌)) → (𝑥𝐹𝑦) = (𝑥𝐺𝑦))    &   ⊢ (𝑊 ∈ NrmCVec → 𝐹:(𝑌 × 𝑌)⟶𝑅)    &   ⊢ (𝑈 ∈ NrmCVec → 𝐺:((BaseSet‘𝑈) × (BaseSet‘𝑈))⟶𝑆)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝐹 = (𝐺 ↾ (𝑌 × 𝑌)))
Theorem	sspmval 28996	Vector addition on a subspace in terms of vector addition on the parent space. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.)
⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    &   ⊢ 𝐿 = ( −𝑣 ‘𝑊)    &   ⊢ 𝐻 = (SubSp‘𝑈)    ⇒   ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) ∧ (𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌)) → (𝐴𝐿𝐵) = (𝐴𝑀𝐵))
Theorem	sspm 28997	Vector subtraction on a subspace is a restriction of vector subtraction on the parent space. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.)
⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    &   ⊢ 𝐿 = ( −𝑣 ‘𝑊)    &   ⊢ 𝐻 = (SubSp‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝐿 = (𝑀 ↾ (𝑌 × 𝑌)))
Theorem	sspz 28998	The zero vector of a subspace is the same as the parent's. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.)
⊢ 𝑍 = (0vec‘𝑈)    &   ⊢ 𝑄 = (0vec‘𝑊)    &   ⊢ 𝐻 = (SubSp‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝑄 = 𝑍)
Theorem	sspn 28999	The norm on a subspace is a restriction of the norm on the parent space. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.)
⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑀 = (normCV‘𝑊)    &   ⊢ 𝐻 = (SubSp‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝑀 = (𝑁 ↾ 𝑌))
Theorem	sspnval 29000	The norm on a subspace in terms of the norm on the parent space. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.)
⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑀 = (normCV‘𝑊)    &   ⊢ 𝐻 = (SubSp‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ∧ 𝐴 ∈ 𝑌) → (𝑀‘𝐴) = (𝑁‘𝐴))