Home | Metamath
Proof Explorer Theorem List (p. 285 of 449) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-28689) |
Hilbert Space Explorer
(28690-30212) |
Users' Mathboxes
(30213-44900) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | nvdi 28401 | 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 28402 | 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 28403 | 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 28404 | 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 28405 | 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 28406 | 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 28407 | 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 28408 | 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 28409 | 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 28410 | 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 28411 | 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 28412 | Vector subtraction in terms of group division operation. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑀 = ( −𝑣 ‘𝑈) & ⊢ 𝑁 = ( /𝑔 ‘𝐺) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑀𝐵) = (𝐴𝑁𝐵)) | ||
Theorem | nvmval 28413 | 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 28414 | 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 28415* | 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 28416 | 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 28417 | 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 28418 | Cancellation law for vector subtraction. (nnncan1 10916 analog.) (Contributed by NM, 7-Mar-2008.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑀 = ( −𝑣 ‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝑀𝐵)𝑀(𝐴𝑀𝐶)) = (𝐶𝑀𝐵)) | ||
Theorem | nvmdi 28419 | Distributive law for scalar product over subtraction. (Contributed by NM, 14-Feb-2008.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑀 = ( −𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝑆(𝐵𝑀𝐶)) = ((𝐴𝑆𝐵)𝑀(𝐴𝑆𝐶))) | ||
Theorem | nvnegneg 28420 | Double negative of a vector. (Contributed by NM, 4-Dec-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (-1𝑆(-1𝑆𝐴)) = 𝐴) | ||
Theorem | nvmul0or 28421 | 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 28422 | 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 28423 | 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 28424 | Cancellation law for vector subtraction. (Contributed by NM, 27-Dec-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑀 = ( −𝑣 ‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴𝐺𝐵)𝑀𝐴) = 𝐵) | ||
Theorem | nvpncan 28425 | Cancellation law for vector subtraction. (Contributed by NM, 24-Jan-2008.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑀 = ( −𝑣 ‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴𝐺𝐵)𝑀𝐵) = 𝐴) | ||
Theorem | nvaddsub 28426 | Commutative/associative law for vector addition and subtraction. (Contributed by NM, 24-Jan-2008.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑀 = ( −𝑣 ‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝑀𝐶) = ((𝐴𝑀𝐶)𝐺𝐵)) | ||
Theorem | nvnpcan 28427 | Cancellation law for a normed complex vector space. (Contributed by NM, 24-Jan-2008.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑀 = ( −𝑣 ‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴𝑀𝐵)𝐺𝐵) = 𝐴) | ||
Theorem | nvaddsub4 28428 | 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 28429 | 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 28430 | A vector minus itself is the zero vector. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑀 = ( −𝑣 ‘𝑈) & ⊢ 𝑍 = (0vec‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝐴𝑀𝐴) = 𝑍) | ||
Theorem | nvf 28431 | Mapping for the norm function. (Contributed by NM, 11-Nov-2006.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) ⇒ ⊢ (𝑈 ∈ NrmCVec → 𝑁:𝑋⟶ℝ) | ||
Theorem | nvcl 28432 | 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 28433 | 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 28434 | 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 28435 | 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 28436 | 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 28437 | 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 28438 | 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 28439 | The norm of a zero vector is zero. (Contributed by NM, 24-Nov-2006.) (New usage is discouraged.) |
⊢ 𝑍 = (0vec‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) ⇒ ⊢ (𝑈 ∈ NrmCVec → (𝑁‘𝑍) = 0) | ||
Theorem | nvz 28440 | 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 28441 | 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 28442 | Triangle inequality for the norm of a vector difference. (Contributed by NM, 27-Dec-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑀 = ( −𝑣 ‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑁‘(𝐴𝑀𝐵)) ≤ ((𝑁‘𝐴) + (𝑁‘𝐵))) | ||
Theorem | nvabs 28443 | 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 28444 | 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 28445 | A nonzero norm is positive. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑍 = (0vec‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝐴 ≠ 𝑍 ↔ 0 < (𝑁‘𝐴))) | ||
Theorem | nv1 28446 | 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 28447 | A complex inner product space in terms of ordered pair components. (Contributed by NM, 11-Sep-2007.) (New usage is discouraged.) |
⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) ⇒ ⊢ (𝑈 ∈ NrmCVec → 𝑈 = 〈〈𝐺, 𝑆〉, 𝑁〉) | ||
Theorem | cnnv 28448 | 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 28449 | 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 28450 | 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 28451 | 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 28452 | 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 28453 | 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 28454 | 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 28455 | 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 | ||
Theorem | imsval 28456 | 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 28457 | 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 28458 | 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 28459 | 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 28460 | 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 28461 | Lemma for imsmet 28462. (Contributed by NM, 29-Nov-2006.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑀 = (inv‘𝐺) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑍 = (0vec‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝐷 = (IndMet‘𝑈) & ⊢ 𝑈 ∈ NrmCVec ⇒ ⊢ 𝐷 ∈ (Met‘𝑋) | ||
Theorem | imsmet 28462 | 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 28463 | 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 28464 | The metric induced on the complex numbers. cnmet 23374 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 28465 | 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 28466 | 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 28467 | The norm of a normed complex vector space is a continuous function to ℂ. (For ℝ, see nmcvcn 28466.) (Contributed by NM, 12-Aug-2007.) (New usage is discouraged.) |
⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝐶 = (IndMet‘𝑈) & ⊢ 𝐽 = (MetOpen‘𝐶) & ⊢ 𝐾 = (TopOpen‘ℂfld) ⇒ ⊢ (𝑈 ∈ NrmCVec → 𝑁 ∈ (𝐽 Cn 𝐾)) | ||
Theorem | smcnlem 28468* | Lemma for smcn 28469. (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 28469 | 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 28470 | Vector subtraction is jointly continuous in both arguments. (Contributed by Mario Carneiro, 6-May-2014.) (New usage is discouraged.) |
⊢ 𝐶 = (IndMet‘𝑈) & ⊢ 𝐽 = (MetOpen‘𝐶) & ⊢ 𝑀 = ( −𝑣 ‘𝑈) ⇒ ⊢ (𝑈 ∈ NrmCVec → 𝑀 ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) | ||
Syntax | cdip 28471 | Extend class notation with the class inner product functions. |
class ·𝑖OLD | ||
Definition | df-dip 28472* | 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 28473* | 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 28474* | 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 28475 | Lemma for ipval3 28480. (Contributed by NM, 1-Feb-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) ⇒ ⊢ (((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝐶 ∈ ℂ) → ((𝑁‘(𝐴𝐺(𝐶𝑆𝐵)))↑2) ∈ ℝ) | ||
Theorem | ipval2lem3 28476 | Lemma for ipval3 28480. (Contributed by NM, 1-Feb-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑁‘(𝐴𝐺𝐵))↑2) ∈ ℝ) | ||
Theorem | ipval2lem4 28477 | Lemma for ipval3 28480. (Contributed by NM, 1-Feb-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) ⇒ ⊢ (((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝐶 ∈ ℂ) → ((𝑁‘(𝐴𝐺(𝐶𝑆𝐵)))↑2) ∈ ℂ) | ||
Theorem | ipval2 28478 | Expansion of the inner product value ipval 28474. (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 28479 | Four times the inner product value ipval3 28480, 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 28480 | Expansion of the inner product value ipval 28474. (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 28481 | 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 28482 | Norm expressed in terms of inner product. (Contributed by NM, 11-Sep-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) = (√‘(𝐴𝑃𝐴))) | ||
Theorem | dipcl 28483 | 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 28484 | 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 28485 | 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 28486 | An inner product times its conjugate. (Contributed by NM, 23-Nov-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴𝑃𝐵) · (𝐵𝑃𝐴)) = ((abs‘(𝐴𝑃𝐵))↑2)) | ||
Theorem | diporthcom 28487 | 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 28488 | Inner product with a zero second argument. (Contributed by NM, 5-Feb-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑍 = (0vec‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝐴𝑃𝑍) = 0) | ||
Theorem | dip0l 28489 | 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 28490 | 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 28491 | 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 𝐾)) | ||
Syntax | css 28492 | Extend class notation with the class of all subspaces of normed complex vector spaces. |
class SubSp | ||
Definition | df-ssp 28493* | 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 28494* | 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 28495 | The predicate "is a subspace." (Contributed by NM, 26-Jan-2008.) (New usage is discouraged.) |
⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝐹 = ( +𝑣 ‘𝑊) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑅 = ( ·𝑠OLD ‘𝑊) & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝑀 = (normCV‘𝑊) & ⊢ 𝐻 = (SubSp‘𝑈) ⇒ ⊢ (𝑈 ∈ NrmCVec → (𝑊 ∈ 𝐻 ↔ (𝑊 ∈ NrmCVec ∧ (𝐹 ⊆ 𝐺 ∧ 𝑅 ⊆ 𝑆 ∧ 𝑀 ⊆ 𝑁)))) | ||
Theorem | sspid 28496 | A normed complex vector space is a subspace of itself. (Contributed by NM, 8-Apr-2008.) (New usage is discouraged.) |
⊢ 𝐻 = (SubSp‘𝑈) ⇒ ⊢ (𝑈 ∈ NrmCVec → 𝑈 ∈ 𝐻) | ||
Theorem | sspnv 28497 | A subspace is a normed complex vector space. (Contributed by NM, 27-Jan-2008.) (New usage is discouraged.) |
⊢ 𝐻 = (SubSp‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝑊 ∈ NrmCVec) | ||
Theorem | sspba 28498 | 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 28499 | 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 28500 | 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 ∧ 𝑊 ∈ 𝐻) ∧ (𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌)) → (𝐴𝐹𝐵) = (𝐴𝐺𝐵)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |