HomeTheorem List (p. 281 of 435)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 281 of 435) | < 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-28326) |
Hilbert Space Explorer
(28327-29851) |
Users' Mathboxes
(29852-43457) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Definition | df-va 28001 | Define vector addition on a normed complex vector space. (Contributed by NM, 23-Apr-2007.) (New usage is discouraged.) |
| ⊢ +𝑣 = (1st ∘ 1st ) | ||
| Definition | df-ba 28002 | Define the base set of a normed complex vector space. (Contributed by NM, 23-Apr-2007.) (New usage is discouraged.) |
| ⊢ BaseSet = (𝑥 ∈ V ↦ ran ( +𝑣 ‘𝑥)) | ||
| Definition | df-sm 28003 | Define scalar multiplication on a normed complex vector space. (Contributed by NM, 24-Apr-2007.) (New usage is discouraged.) |
| ⊢ ·𝑠OLD = (2nd ∘ 1st ) | ||
| Definition | df-0v 28004 | Define the zero vector in a normed complex vector space. (Contributed by NM, 24-Apr-2007.) (New usage is discouraged.) |
| ⊢ 0vec = (GId ∘ +𝑣 ) | ||
| Definition | df-vs 28005 | Define vector subtraction on a normed complex vector space. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.) |
| ⊢ −𝑣 = ( /𝑔 ∘ +𝑣 ) | ||
| Definition | df-nmcv 28006 | Define the norm function in a normed complex vector space. (Contributed by NM, 25-Apr-2007.) (New usage is discouraged.) |
| ⊢ normCV = 2nd | ||
| Definition | df-ims 28007 | Define the induced metric on a normed complex vector space. (Contributed by NM, 11-Sep-2007.) (New usage is discouraged.) |
| ⊢ IndMet = (𝑢 ∈ NrmCVec ↦ ((normCV‘𝑢) ∘ ( −𝑣 ‘𝑢))) | ||
| Theorem | nvrel 28008 | The class of all normed complex vectors spaces is a relation. (Contributed by NM, 14-Nov-2006.) (New usage is discouraged.) |
| ⊢ Rel NrmCVec | ||
| Theorem | vafval 28009 | Value of the function for the vector addition (group) operation on a normed complex vector space. (Contributed by NM, 23-Apr-2007.) (New usage is discouraged.) |
| ⊢ 𝐺 = ( +𝑣 ‘𝑈) ⇒ ⊢ 𝐺 = (1st ‘(1st ‘𝑈)) | ||
| Theorem | bafval 28010 | Value of the function for the base set of a normed complex vector space. (Contributed by NM, 23-Apr-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) ⇒ ⊢ 𝑋 = ran 𝐺 | ||
| Theorem | smfval 28011 | Value of the function for the scalar multiplication operation on a normed complex vector space. (Contributed by NM, 24-Apr-2007.) (New usage is discouraged.) |
| ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) ⇒ ⊢ 𝑆 = (2nd ‘(1st ‘𝑈)) | ||
| Theorem | 0vfval 28012 | Value of the function for the zero vector on a normed complex vector space. (Contributed by NM, 24-Apr-2007.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.) |
| ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑍 = (0vec‘𝑈) ⇒ ⊢ (𝑈 ∈ 𝑉 → 𝑍 = (GId‘𝐺)) | ||
| Theorem | nmcvfval 28013 | Value of the norm function in a normed complex vector space. (Contributed by NM, 25-Apr-2007.) (New usage is discouraged.) |
| ⊢ 𝑁 = (normCV‘𝑈) ⇒ ⊢ 𝑁 = (2nd ‘𝑈) | ||
| Theorem | nvop2 28014 | A normed complex vector space is an ordered pair of a vector space and a norm operation. (Contributed by NM, 28-Nov-2006.) (New usage is discouraged.) |
| ⊢ 𝑊 = (1st ‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) ⇒ ⊢ (𝑈 ∈ NrmCVec → 𝑈 = ⟨𝑊, 𝑁⟩) | ||
| Theorem | nvvop 28015 | The vector space component of a normed complex vector space is an ordered pair of the underlying group and a scalar product. (Contributed by NM, 28-Nov-2006.) (New usage is discouraged.) |
| ⊢ 𝑊 = (1st ‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) ⇒ ⊢ (𝑈 ∈ NrmCVec → 𝑊 = ⟨𝐺, 𝑆⟩) | ||
| Theorem | isnvlem 28016* | Lemma for isnv 28018. (Contributed by NM, 11-Nov-2006.) (New usage is discouraged.) |
| ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ ((𝐺 ∈ V ∧ 𝑆 ∈ V ∧ 𝑁 ∈ V) → (⟨⟨𝐺, 𝑆⟩, 𝑁⟩ ∈ NrmCVec ↔ (⟨𝐺, 𝑆⟩ ∈ CVecOLD ∧ 𝑁:𝑋⟶ℝ ∧ ∀𝑥 ∈ 𝑋 (((𝑁‘𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑁‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑁‘𝑥)) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦)))))) | ||
| Theorem | nvex 28017 | The components of a normed complex vector space are sets. (Contributed by NM, 5-Jun-2008.) (Revised by Mario Carneiro, 1-May-2015.) (New usage is discouraged.) |
| ⊢ (⟨⟨𝐺, 𝑆⟩, 𝑁⟩ ∈ NrmCVec → (𝐺 ∈ V ∧ 𝑆 ∈ V ∧ 𝑁 ∈ V)) | ||
| Theorem | isnv 28018* | The predicate "is a normed complex vector space." (Contributed by NM, 5-Jun-2008.) (New usage is discouraged.) |
| ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ (⟨⟨𝐺, 𝑆⟩, 𝑁⟩ ∈ NrmCVec ↔ (⟨𝐺, 𝑆⟩ ∈ CVecOLD ∧ 𝑁:𝑋⟶ℝ ∧ ∀𝑥 ∈ 𝑋 (((𝑁‘𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑁‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑁‘𝑥)) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))))) | ||
| Theorem | isnvi 28019* | Properties that determine a normed complex vector space. (Contributed by NM, 15-Apr-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑍 = (GId‘𝐺) & ⊢ ⟨𝐺, 𝑆⟩ ∈ CVecOLD & ⊢ 𝑁:𝑋⟶ℝ & ⊢ ((𝑥 ∈ 𝑋 ∧ (𝑁‘𝑥) = 0) → 𝑥 = 𝑍) & ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝑋) → (𝑁‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑁‘𝑥))) & ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))) & ⊢ 𝑈 = ⟨⟨𝐺, 𝑆⟩, 𝑁⟩ ⇒ ⊢ 𝑈 ∈ NrmCVec | ||
| Theorem | nvi 28020* | The properties of a normed complex vector space, which is a vector space accompanied by a norm. (Contributed by NM, 11-Nov-2006.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑍 = (0vec‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) ⇒ ⊢ (𝑈 ∈ NrmCVec → (⟨𝐺, 𝑆⟩ ∈ CVecOLD ∧ 𝑁:𝑋⟶ℝ ∧ ∀𝑥 ∈ 𝑋 (((𝑁‘𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑁‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑁‘𝑥)) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))))) | ||
| Theorem | nvvc 28021 | The vector space component of a normed complex vector space. (Contributed by NM, 28-Nov-2006.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.) |
| ⊢ 𝑊 = (1st ‘𝑈) ⇒ ⊢ (𝑈 ∈ NrmCVec → 𝑊 ∈ CVecOLD) | ||
| Theorem | nvablo 28022 | The vector addition operation of a normed complex vector space is an Abelian group. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.) |
| ⊢ 𝐺 = ( +𝑣 ‘𝑈) ⇒ ⊢ (𝑈 ∈ NrmCVec → 𝐺 ∈ AbelOp) | ||
| Theorem | nvgrp 28023 | The vector addition operation of a normed complex vector space is a group. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.) |
| ⊢ 𝐺 = ( +𝑣 ‘𝑈) ⇒ ⊢ (𝑈 ∈ NrmCVec → 𝐺 ∈ GrpOp) | ||
| Theorem | nvgf 28024 | Mapping for the vector addition operation. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) ⇒ ⊢ (𝑈 ∈ NrmCVec → 𝐺:(𝑋 × 𝑋)⟶𝑋) | ||
| Theorem | nvsf 28025 | Mapping for the scalar multiplication operation. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) ⇒ ⊢ (𝑈 ∈ NrmCVec → 𝑆:(ℂ × 𝑋)⟶𝑋) | ||
| Theorem | nvgcl 28026 | 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 28027 | The vector addition (group) operation is commutative. (Contributed by NM, 4-Dec-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐺𝐵) = (𝐵𝐺𝐴)) | ||
| Theorem | nvass 28028 | The vector addition (group) operation is associative. (Contributed by NM, 4-Dec-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐺𝐶) = (𝐴𝐺(𝐵𝐺𝐶))) | ||
| Theorem | nvadd32 28029 | Commutative/associative law for vector addition. (Contributed by NM, 27-Dec-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐺𝐶) = ((𝐴𝐺𝐶)𝐺𝐵)) | ||
| Theorem | nvrcan 28030 | Right cancellation law for vector addition. (Contributed by NM, 4-Dec-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐶) = (𝐵𝐺𝐶) ↔ 𝐴 = 𝐵)) | ||
| Theorem | nvadd4 28031 | Rearrangement of 4 terms in a vector sum. (Contributed by NM, 8-Feb-2008.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐺(𝐶𝐺𝐷)) = ((𝐴𝐺𝐶)𝐺(𝐵𝐺𝐷))) | ||
| Theorem | nvscl 28032 | 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 28033 | 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 28034 | 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 28035 | 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 28036 | 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 28037 | 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 28038 | 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 28039 | 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 28040 | 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 28041 | 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 28042 | 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 28043 | 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 28044 | 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 28045 | 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 28046 | 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 28047 | Vector subtraction in terms of group division operation. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑀 = ( −𝑣 ‘𝑈) & ⊢ 𝑁 = ( /𝑔 ‘𝐺) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑀𝐵) = (𝐴𝑁𝐵)) | ||
| Theorem | nvmval 28048 | 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 28049 | 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 28050* | 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 28051 | 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 28052 | 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 28053 | Cancellation law for vector subtraction. (nnncan1 10645 analog.) (Contributed by NM, 7-Mar-2008.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑀 = ( −𝑣 ‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝑀𝐵)𝑀(𝐴𝑀𝐶)) = (𝐶𝑀𝐵)) | ||
| Theorem | nvmdi 28054 | Distributive law for scalar product over subtraction. (Contributed by NM, 14-Feb-2008.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑀 = ( −𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝑆(𝐵𝑀𝐶)) = ((𝐴𝑆𝐵)𝑀(𝐴𝑆𝐶))) | ||
| Theorem | nvnegneg 28055 | Double negative of a vector. (Contributed by NM, 4-Dec-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (-1𝑆(-1𝑆𝐴)) = 𝐴) | ||
| Theorem | nvmul0or 28056 | 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 28057 | 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 28058 | 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 28059 | Cancellation law for vector subtraction. (Contributed by NM, 27-Dec-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑀 = ( −𝑣 ‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴𝐺𝐵)𝑀𝐴) = 𝐵) | ||
| Theorem | nvpncan 28060 | Cancellation law for vector subtraction. (Contributed by NM, 24-Jan-2008.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑀 = ( −𝑣 ‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴𝐺𝐵)𝑀𝐵) = 𝐴) | ||
| Theorem | nvaddsub 28061 | Commutative/associative law for vector addition and subtraction. (Contributed by NM, 24-Jan-2008.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑀 = ( −𝑣 ‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝑀𝐶) = ((𝐴𝑀𝐶)𝐺𝐵)) | ||
| Theorem | nvnpcan 28062 | Cancellation law for a normed complex vector space. (Contributed by NM, 24-Jan-2008.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑀 = ( −𝑣 ‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴𝑀𝐵)𝐺𝐵) = 𝐴) | ||
| Theorem | nvaddsub4 28063 | 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 28064 | 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 28065 | A vector minus itself is the zero vector. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑀 = ( −𝑣 ‘𝑈) & ⊢ 𝑍 = (0vec‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝐴𝑀𝐴) = 𝑍) | ||
| Theorem | nvf 28066 | Mapping for the norm function. (Contributed by NM, 11-Nov-2006.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) ⇒ ⊢ (𝑈 ∈ NrmCVec → 𝑁:𝑋⟶ℝ) | ||
| Theorem | nvcl 28067 | 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 28068 | 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 28069 | 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 28070 | 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 28071 | 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 28072 | 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 28073 | 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 28074 | The norm of a zero vector is zero. (Contributed by NM, 24-Nov-2006.) (New usage is discouraged.) |
| ⊢ 𝑍 = (0vec‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) ⇒ ⊢ (𝑈 ∈ NrmCVec → (𝑁‘𝑍) = 0) | ||
| Theorem | nvz 28075 | 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 28076 | 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 28077 | Triangle inequality for the norm of a vector difference. (Contributed by NM, 27-Dec-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑀 = ( −𝑣 ‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑁‘(𝐴𝑀𝐵)) ≤ ((𝑁‘𝐴) + (𝑁‘𝐵))) | ||
| Theorem | nvabs 28078 | 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 28079 | 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 28080 | A nonzero norm is positive. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑍 = (0vec‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝐴 ≠ 𝑍 ↔ 0 < (𝑁‘𝐴))) | ||
| Theorem | nv1 28081 | 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 28082 | 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 28083 | 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 28084 | 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 28085 | 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 28086 | 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 28087 | 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 28088 | 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 28089 | 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 28090 | 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 28091 | 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 28092 | 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 28093 | 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 28094 | 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 28095 | 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 28096 | Lemma for imsmet 28097. (Contributed by NM, 29-Nov-2006.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑀 = (inv‘𝐺) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑍 = (0vec‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝐷 = (IndMet‘𝑈) & ⊢ 𝑈 ∈ NrmCVec ⇒ ⊢ 𝐷 ∈ (Met‘𝑋) | ||
| Theorem | imsmet 28097 | 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 28098 | 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 28099 | The metric induced on the complex numbers. cnmet 22952 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 28100 | 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 𝐽)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |