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	nvgcl 31001	Closure law for the vector addition (group) operation of a normed complex vector space. (Contributed by NM, 23-Apr-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐺𝐵) ∈ 𝑋)
Theorem	nvcom 31002	The vector addition (group) operation is commutative. (Contributed by NM, 4-Dec-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐺𝐵) = (𝐵𝐺𝐴))
Theorem	nvass 31003	The vector addition (group) operation is associative. (Contributed by NM, 4-Dec-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐺𝐶) = (𝐴𝐺(𝐵𝐺𝐶)))
Theorem	nvadd32 31004	Commutative/associative law for vector addition. (Contributed by NM, 27-Dec-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐺𝐶) = ((𝐴𝐺𝐶)𝐺𝐵))
Theorem	nvrcan 31005	Right cancellation law for vector addition. (Contributed by NM, 4-Dec-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐶) = (𝐵𝐺𝐶) ↔ 𝐴 = 𝐵))
Theorem	nvadd4 31006	Rearrangement of 4 terms in a vector sum. (Contributed by NM, 8-Feb-2008.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐺(𝐶𝐺𝐷)) = ((𝐴𝐺𝐶)𝐺(𝐵𝐺𝐷)))
Theorem	nvscl 31007	Closure law for the scalar product operation of a normed complex vector space. (Contributed by NM, 1-Feb-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋) → (𝐴𝑆𝐵) ∈ 𝑋)
Theorem	nvsid 31008	Identity element for the scalar product of a normed complex vector space. (Contributed by NM, 4-Dec-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (1𝑆𝐴) = 𝐴)
Theorem	nvsass 31009	Associative law for the scalar product of a normed complex vector space. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋)) → ((𝐴 · 𝐵)𝑆𝐶) = (𝐴𝑆(𝐵𝑆𝐶)))
Theorem	nvscom 31010	Commutative law for the scalar product of a normed complex vector space. (Contributed by NM, 14-Feb-2008.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋)) → (𝐴𝑆(𝐵𝑆𝐶)) = (𝐵𝑆(𝐴𝑆𝐶)))
Theorem	nvdi 31011	Distributive law for the scalar product of a complex vector space. (Contributed by NM, 4-Dec-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝑆(𝐵𝐺𝐶)) = ((𝐴𝑆𝐵)𝐺(𝐴𝑆𝐶)))
Theorem	nvdir 31012	Distributive law for the scalar product of a complex vector space. (Contributed by NM, 4-Dec-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋)) → ((𝐴 + 𝐵)𝑆𝐶) = ((𝐴𝑆𝐶)𝐺(𝐵𝑆𝐶)))
Theorem	nv2 31013	A vector plus itself is two times the vector. (Contributed by NM, 9-Feb-2008.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝐴𝐺𝐴) = (2𝑆𝐴))
Theorem	vsfval 31014	Value of the function for the vector subtraction operation on a normed complex vector space. (Contributed by NM, 15-Feb-2008.) (Revised by Mario Carneiro, 27-Dec-2014.) (New usage is discouraged.)
⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    ⇒   ⊢ 𝑀 = ( /𝑔 ‘𝐺)
Theorem	nvzcl 31015	Closure law for the zero vector of a normed complex vector space. (Contributed by NM, 27-Nov-2007.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑈)    ⇒   ⊢ (𝑈 ∈ NrmCVec → 𝑍 ∈ 𝑋)
Theorem	nv0rid 31016	The zero vector is a right identity element. (Contributed by NM, 28-Nov-2007.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝐴𝐺𝑍) = 𝐴)
Theorem	nv0lid 31017	The zero vector is a left identity element. (Contributed by NM, 28-Nov-2007.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝑍𝐺𝐴) = 𝐴)
Theorem	nv0 31018	Zero times a vector is the zero vector. (Contributed by NM, 27-Nov-2007.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (0𝑆𝐴) = 𝑍)
Theorem	nvsz 31019	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 31020	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 31021	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 31022	Vector subtraction in terms of group division operation. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    &   ⊢ 𝑁 = ( /𝑔 ‘𝐺)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑀𝐵) = (𝐴𝑁𝐵))
Theorem	nvmval 31023	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 31024	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 31025*	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 31026	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 31027	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 31028	Cancellation law for vector subtraction. (nnncan1 11505 analog.) (Contributed by NM, 7-Mar-2008.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝑀𝐵)𝑀(𝐴𝑀𝐶)) = (𝐶𝑀𝐵))
Theorem	nvmdi 31029	Distributive law for scalar product over subtraction. (Contributed by NM, 14-Feb-2008.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝑆(𝐵𝑀𝐶)) = ((𝐴𝑆𝐵)𝑀(𝐴𝑆𝐶)))
Theorem	nvnegneg 31030	Double negative of a vector. (Contributed by NM, 4-Dec-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (-1𝑆(-1𝑆𝐴)) = 𝐴)
Theorem	nvmul0or 31031	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 31032	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 31033	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 31034	Cancellation law for vector subtraction. (Contributed by NM, 27-Dec-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴𝐺𝐵)𝑀𝐴) = 𝐵)
Theorem	nvpncan 31035	Cancellation law for vector subtraction. (Contributed by NM, 24-Jan-2008.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴𝐺𝐵)𝑀𝐵) = 𝐴)
Theorem	nvaddsub 31036	Commutative/associative law for vector addition and subtraction. (Contributed by NM, 24-Jan-2008.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝑀𝐶) = ((𝐴𝑀𝐶)𝐺𝐵))
Theorem	nvnpcan 31037	Cancellation law for a normed complex vector space. (Contributed by NM, 24-Jan-2008.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴𝑀𝐵)𝐺𝐵) = 𝐴)
Theorem	nvaddsub4 31038	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 31039	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 31040	A vector minus itself is the zero vector. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝐴𝑀𝐴) = 𝑍)
Theorem	nvf 31041	Mapping for the norm function. (Contributed by NM, 11-Nov-2006.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    ⇒   ⊢ (𝑈 ∈ NrmCVec → 𝑁:𝑋⟶ℝ)
Theorem	nvcl 31042	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 31043	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 31044	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 31045	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 31046	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 31047	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 31048	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 31049	The norm of a zero vector is zero. (Contributed by NM, 24-Nov-2006.) (New usage is discouraged.)
⊢ 𝑍 = (0vec‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    ⇒   ⊢ (𝑈 ∈ NrmCVec → (𝑁‘𝑍) = 0)
Theorem	nvz 31050	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 31051	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 31052	Triangle inequality for the norm of a vector difference. (Contributed by NM, 27-Dec-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑁‘(𝐴𝑀𝐵)) ≤ ((𝑁‘𝐴) + (𝑁‘𝐵)))
Theorem	nvabs 31053	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 31054	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 31055	A nonzero norm is positive. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝐴 ≠ 𝑍 ↔ 0 < (𝑁‘𝐴)))
Theorem	nv1 31056	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 31057	A complex inner product space in terms of ordered pair components. (Contributed by NM, 11-Sep-2007.) (New usage is discouraged.)
⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    ⇒   ⊢ (𝑈 ∈ NrmCVec → 𝑈 = ⟨⟨𝐺, 𝑆⟩, 𝑁⟩)
19.3.2  Examples of normed complex vector spaces
Theorem	cnnv 31058	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 31059	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 31060	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 31061	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 31062	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 31063	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 31064	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 31065	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
19.3.3  Induced metric of a normed complex vector space
Theorem	imsval 31066	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 31067	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 31068	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 31069	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 31070	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 31071	Lemma for imsmet 31072. (Contributed by NM, 29-Nov-2006.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑀 = (inv‘𝐺)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝐷 = (IndMet‘𝑈)    &   ⊢ 𝑈 ∈ NrmCVec    ⇒   ⊢ 𝐷 ∈ (Met‘𝑋)
Theorem	imsmet 31072	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 31073	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 31074	The metric induced on the complex numbers. cnmet 24957 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 31075	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 31076	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 31077	The norm of a normed complex vector space is a continuous function to ℂ. (For ℝ, see nmcvcn 31076.) (Contributed by NM, 12-Aug-2007.) (New usage is discouraged.)
⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝐶 = (IndMet‘𝑈)    &   ⊢ 𝐽 = (MetOpen‘𝐶)    &   ⊢ 𝐾 = (TopOpen‘ℂfld)    ⇒   ⊢ (𝑈 ∈ NrmCVec → 𝑁 ∈ (𝐽 Cn 𝐾))
Theorem	smcnlem 31078*	Lemma for smcn 31079. (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 31079	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 31080	Vector subtraction is jointly continuous in both arguments. (Contributed by Mario Carneiro, 6-May-2014.) (New usage is discouraged.)
⊢ 𝐶 = (IndMet‘𝑈)    &   ⊢ 𝐽 = (MetOpen‘𝐶)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    ⇒   ⊢ (𝑈 ∈ NrmCVec → 𝑀 ∈ ((𝐽 ×t 𝐽) Cn 𝐽))
19.3.4  Inner product
Syntax	cdip 31081	Extend class notation with the class inner product functions.
class ·𝑖OLD
Definition	df-dip 31082*	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 31083*	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 31084*	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 31085	Lemma for ipval3 31090. (Contributed by NM, 1-Feb-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ (((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝐶 ∈ ℂ) → ((𝑁‘(𝐴𝐺(𝐶𝑆𝐵)))↑2) ∈ ℝ)
Theorem	ipval2lem3 31086	Lemma for ipval3 31090. (Contributed by NM, 1-Feb-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑁‘(𝐴𝐺𝐵))↑2) ∈ ℝ)
Theorem	ipval2lem4 31087	Lemma for ipval3 31090. (Contributed by NM, 1-Feb-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ (((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝐶 ∈ ℂ) → ((𝑁‘(𝐴𝐺(𝐶𝑆𝐵)))↑2) ∈ ℂ)
Theorem	ipval2 31088	Expansion of the inner product value ipval 31084. (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 31089	Four times the inner product value ipval3 31090, 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 31090	Expansion of the inner product value ipval 31084. (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 31091	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 31092	Norm expressed in terms of inner product. (Contributed by NM, 11-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) = (√‘(𝐴𝑃𝐴)))
Theorem	dipcl 31093	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 31094	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 31095	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 31096	An inner product times its conjugate. (Contributed by NM, 23-Nov-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴𝑃𝐵) · (𝐵𝑃𝐴)) = ((abs‘(𝐴𝑃𝐵))↑2))
Theorem	diporthcom 31097	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 31098	Inner product with a zero second argument. (Contributed by NM, 5-Feb-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝐴𝑃𝑍) = 0)
Theorem	dip0l 31099	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 31100	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 ↔ 𝐴 = 𝑍))