Home | Metamath
Proof Explorer Theorem List (p. 284 of 450) | < 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-28697) |
Hilbert Space Explorer
(28698-30220) |
Users' Mathboxes
(30221-44913) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | grpoinvfval 28301* | The inverse function of a group. (Contributed by NM, 26-Oct-2006.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐺) & ⊢ 𝑁 = (inv‘𝐺) ⇒ ⊢ (𝐺 ∈ GrpOp → 𝑁 = (𝑥 ∈ 𝑋 ↦ (℩𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑈))) | ||
Theorem | grpoinvval 28302* | The inverse of a group element. (Contributed by NM, 26-Oct-2006.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐺) & ⊢ 𝑁 = (inv‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) = (℩𝑦 ∈ 𝑋 (𝑦𝐺𝐴) = 𝑈)) | ||
Theorem | grpoinvcl 28303 | A group element's inverse is a group element. (Contributed by NM, 27-Oct-2006.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑁 = (inv‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) ∈ 𝑋) | ||
Theorem | grpoinv 28304 | The properties of a group element's inverse. (Contributed by NM, 27-Oct-2006.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐺) & ⊢ 𝑁 = (inv‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) → (((𝑁‘𝐴)𝐺𝐴) = 𝑈 ∧ (𝐴𝐺(𝑁‘𝐴)) = 𝑈)) | ||
Theorem | grpolinv 28305 | The left inverse of a group element. (Contributed by NM, 27-Oct-2006.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐺) & ⊢ 𝑁 = (inv‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) → ((𝑁‘𝐴)𝐺𝐴) = 𝑈) | ||
Theorem | grporinv 28306 | The right inverse of a group element. (Contributed by NM, 27-Oct-2006.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐺) & ⊢ 𝑁 = (inv‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) → (𝐴𝐺(𝑁‘𝐴)) = 𝑈) | ||
Theorem | grpoinvid1 28307 | The inverse of a group element expressed in terms of the identity element. (Contributed by NM, 27-Oct-2006.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐺) & ⊢ 𝑁 = (inv‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑁‘𝐴) = 𝐵 ↔ (𝐴𝐺𝐵) = 𝑈)) | ||
Theorem | grpoinvid2 28308 | The inverse of a group element expressed in terms of the identity element. (Contributed by NM, 27-Oct-2006.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐺) & ⊢ 𝑁 = (inv‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑁‘𝐴) = 𝐵 ↔ (𝐵𝐺𝐴) = 𝑈)) | ||
Theorem | grpolcan 28309 | Left cancellation law for groups. (Contributed by NM, 27-Oct-2006.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐶𝐺𝐴) = (𝐶𝐺𝐵) ↔ 𝐴 = 𝐵)) | ||
Theorem | grpo2inv 28310 | Double inverse law for groups. Lemma 2.2.1(c) of [Herstein] p. 55. (Contributed by NM, 27-Oct-2006.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑁 = (inv‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) → (𝑁‘(𝑁‘𝐴)) = 𝐴) | ||
Theorem | grpoinvf 28311 | Mapping of the inverse function of a group. (Contributed by NM, 29-Mar-2008.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑁 = (inv‘𝐺) ⇒ ⊢ (𝐺 ∈ GrpOp → 𝑁:𝑋–1-1-onto→𝑋) | ||
Theorem | grpoinvop 28312 | The inverse of the group operation reverses the arguments. Lemma 2.2.1(d) of [Herstein] p. 55. (Contributed by NM, 27-Oct-2006.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑁 = (inv‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑁‘(𝐴𝐺𝐵)) = ((𝑁‘𝐵)𝐺(𝑁‘𝐴))) | ||
Theorem | grpodivfval 28313* | Group division (or subtraction) operation. (Contributed by NM, 15-Feb-2008.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑁 = (inv‘𝐺) & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ (𝐺 ∈ GrpOp → 𝐷 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (𝑥𝐺(𝑁‘𝑦)))) | ||
Theorem | grpodivval 28314 | Group division (or subtraction) operation value. (Contributed by NM, 15-Feb-2008.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑁 = (inv‘𝐺) & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = (𝐴𝐺(𝑁‘𝐵))) | ||
Theorem | grpodivinv 28315 | Group division by an inverse. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑁 = (inv‘𝐺) & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷(𝑁‘𝐵)) = (𝐴𝐺𝐵)) | ||
Theorem | grpoinvdiv 28316 | Inverse of a group division. (Contributed by NM, 24-Feb-2008.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑁 = (inv‘𝐺) & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑁‘(𝐴𝐷𝐵)) = (𝐵𝐷𝐴)) | ||
Theorem | grpodivf 28317 | Mapping for group division. (Contributed by NM, 10-Apr-2008.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ (𝐺 ∈ GrpOp → 𝐷:(𝑋 × 𝑋)⟶𝑋) | ||
Theorem | grpodivcl 28318 | Closure of group division (or subtraction) operation. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) ∈ 𝑋) | ||
Theorem | grpodivdiv 28319 | Double group division. (Contributed by NM, 24-Feb-2008.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷(𝐵𝐷𝐶)) = (𝐴𝐺(𝐶𝐷𝐵))) | ||
Theorem | grpomuldivass 28320 | Associative-type law for multiplication and division. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐷𝐶) = (𝐴𝐺(𝐵𝐷𝐶))) | ||
Theorem | grpodivid 28321 | Division of a group member by itself. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝐷 = ( /𝑔 ‘𝐺) & ⊢ 𝑈 = (GId‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) → (𝐴𝐷𝐴) = 𝑈) | ||
Theorem | grponpcan 28322 | Cancellation law for group division. (npcan 10897 analog.) (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴𝐷𝐵)𝐺𝐵) = 𝐴) | ||
Syntax | cablo 28323 | Extend class notation with the class of all Abelian group operations. |
class AbelOp | ||
Definition | df-ablo 28324* | Define the class of all Abelian group operations. (Contributed by NM, 2-Nov-2006.) (New usage is discouraged.) |
⊢ AbelOp = {𝑔 ∈ GrpOp ∣ ∀𝑥 ∈ ran 𝑔∀𝑦 ∈ ran 𝑔(𝑥𝑔𝑦) = (𝑦𝑔𝑥)} | ||
Theorem | isablo 28325* | The predicate "is an Abelian (commutative) group operation." (Contributed by NM, 2-Nov-2006.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝐺 ∈ AbelOp ↔ (𝐺 ∈ GrpOp ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐺𝑦) = (𝑦𝐺𝑥))) | ||
Theorem | ablogrpo 28326 | An Abelian group operation is a group operation. (Contributed by NM, 2-Nov-2006.) (New usage is discouraged.) |
⊢ (𝐺 ∈ AbelOp → 𝐺 ∈ GrpOp) | ||
Theorem | ablocom 28327 | An Abelian group operation is commutative. (Contributed by NM, 2-Nov-2006.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝐺 ∈ AbelOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐺𝐵) = (𝐵𝐺𝐴)) | ||
Theorem | ablo32 28328 | Commutative/associative law for Abelian groups. (Contributed by NM, 26-Apr-2007.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝐺 ∈ AbelOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐺𝐶) = ((𝐴𝐺𝐶)𝐺𝐵)) | ||
Theorem | ablo4 28329 | Commutative/associative law for Abelian groups. (Contributed by NM, 26-Apr-2007.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝐺 ∈ AbelOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐺(𝐶𝐺𝐷)) = ((𝐴𝐺𝐶)𝐺(𝐵𝐺𝐷))) | ||
Theorem | isabloi 28330* | Properties that determine an Abelian group operation. (Contributed by NM, 5-Nov-2006.) (New usage is discouraged.) |
⊢ 𝐺 ∈ GrpOp & ⊢ dom 𝐺 = (𝑋 × 𝑋) & ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝐺𝑦) = (𝑦𝐺𝑥)) ⇒ ⊢ 𝐺 ∈ AbelOp | ||
Theorem | ablomuldiv 28331 | Law for group multiplication and division. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ ((𝐺 ∈ AbelOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐷𝐶) = ((𝐴𝐷𝐶)𝐺𝐵)) | ||
Theorem | ablodivdiv 28332 | Law for double group division. (Contributed by NM, 29-Feb-2008.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ ((𝐺 ∈ AbelOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷(𝐵𝐷𝐶)) = ((𝐴𝐷𝐵)𝐺𝐶)) | ||
Theorem | ablodivdiv4 28333 | Law for double group division. (Contributed by NM, 29-Feb-2008.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ ((𝐺 ∈ AbelOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐷𝐵)𝐷𝐶) = (𝐴𝐷(𝐵𝐺𝐶))) | ||
Theorem | ablodiv32 28334 | Swap the second and third terms in a double division. (Contributed by NM, 29-Feb-2008.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ ((𝐺 ∈ AbelOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐷𝐵)𝐷𝐶) = ((𝐴𝐷𝐶)𝐷𝐵)) | ||
Theorem | ablonncan 28335 | Cancellation law for group division. (nncan 10917 analog.) (Contributed by NM, 7-Mar-2008.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ ((𝐺 ∈ AbelOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷(𝐴𝐷𝐵)) = 𝐵) | ||
Theorem | ablonnncan1 28336 | Cancellation law for group division. (nnncan1 10924 analog.) (Contributed by NM, 7-Mar-2008.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ ((𝐺 ∈ AbelOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐷𝐵)𝐷(𝐴𝐷𝐶)) = (𝐶𝐷𝐵)) | ||
Syntax | cvc 28337 | Extend class notation with the class of all complex vector spaces. |
class CVecOLD | ||
Definition | df-vc 28338* | Define the class of all complex vector spaces. (Contributed by NM, 3-Nov-2006.) (New usage is discouraged.) |
⊢ CVecOLD = {〈𝑔, 𝑠〉 ∣ (𝑔 ∈ AbelOp ∧ 𝑠:(ℂ × ran 𝑔)⟶ran 𝑔 ∧ ∀𝑥 ∈ ran 𝑔((1𝑠𝑥) = 𝑥 ∧ ∀𝑦 ∈ ℂ (∀𝑧 ∈ ran 𝑔(𝑦𝑠(𝑥𝑔𝑧)) = ((𝑦𝑠𝑥)𝑔(𝑦𝑠𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝑔(𝑧𝑠𝑥)) ∧ ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥))))))} | ||
Theorem | vcrel 28339 | The class of all complex vector spaces is a relation. (Contributed by NM, 17-Mar-2007.) (New usage is discouraged.) |
⊢ Rel CVecOLD | ||
Theorem | vciOLD 28340* | Obsolete version of cvsi 23736. The properties of a complex vector space, which is an Abelian group (i.e. the vectors, with the operation of vector addition) accompanied by a scalar multiplication operation on the field of complex numbers. The variable 𝑊 was chosen because V is already used for the universal class. (Contributed by NM, 3-Nov-2006.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝐺 = (1st ‘𝑊) & ⊢ 𝑆 = (2nd ‘𝑊) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝑊 ∈ CVecOLD → (𝐺 ∈ AbelOp ∧ 𝑆:(ℂ × 𝑋)⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ((1𝑆𝑥) = 𝑥 ∧ ∀𝑦 ∈ ℂ (∀𝑧 ∈ 𝑋 (𝑦𝑆(𝑥𝐺𝑧)) = ((𝑦𝑆𝑥)𝐺(𝑦𝑆𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑆𝑥) = ((𝑦𝑆𝑥)𝐺(𝑧𝑆𝑥)) ∧ ((𝑦 · 𝑧)𝑆𝑥) = (𝑦𝑆(𝑧𝑆𝑥))))))) | ||
Theorem | vcsm 28341 | Functionality of th scalar product of a complex vector space. (Contributed by NM, 3-Nov-2006.) (New usage is discouraged.) |
⊢ 𝐺 = (1st ‘𝑊) & ⊢ 𝑆 = (2nd ‘𝑊) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝑊 ∈ CVecOLD → 𝑆:(ℂ × 𝑋)⟶𝑋) | ||
Theorem | vccl 28342 | Closure of the scalar product of a complex vector space. (Contributed by NM, 3-Nov-2006.) (New usage is discouraged.) |
⊢ 𝐺 = (1st ‘𝑊) & ⊢ 𝑆 = (2nd ‘𝑊) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑊 ∈ CVecOLD ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋) → (𝐴𝑆𝐵) ∈ 𝑋) | ||
Theorem | vcidOLD 28343 | Identity element for the scalar product of a complex vector space. (Contributed by NM, 3-Nov-2006.) Obsolete theorem, use clmvs1 23699 together with cvsclm 23732 instead. (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝐺 = (1st ‘𝑊) & ⊢ 𝑆 = (2nd ‘𝑊) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋) → (1𝑆𝐴) = 𝐴) | ||
Theorem | vcdi 28344 | Distributive law for the scalar product of a complex vector space. (Contributed by NM, 3-Nov-2006.) (New usage is discouraged.) |
⊢ 𝐺 = (1st ‘𝑊) & ⊢ 𝑆 = (2nd ‘𝑊) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑊 ∈ CVecOLD ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝑆(𝐵𝐺𝐶)) = ((𝐴𝑆𝐵)𝐺(𝐴𝑆𝐶))) | ||
Theorem | vcdir 28345 | Distributive law for the scalar product of a complex vector space. (Contributed by NM, 3-Nov-2006.) (New usage is discouraged.) |
⊢ 𝐺 = (1st ‘𝑊) & ⊢ 𝑆 = (2nd ‘𝑊) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑊 ∈ CVecOLD ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋)) → ((𝐴 + 𝐵)𝑆𝐶) = ((𝐴𝑆𝐶)𝐺(𝐵𝑆𝐶))) | ||
Theorem | vcass 28346 | Associative law for the scalar product of a complex vector space. (Contributed by NM, 3-Nov-2006.) (New usage is discouraged.) |
⊢ 𝐺 = (1st ‘𝑊) & ⊢ 𝑆 = (2nd ‘𝑊) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑊 ∈ CVecOLD ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋)) → ((𝐴 · 𝐵)𝑆𝐶) = (𝐴𝑆(𝐵𝑆𝐶))) | ||
Theorem | vc2OLD 28347 | A vector plus itself is two times the vector. (Contributed by NM, 1-Feb-2007.) Obsolete theorem, use clmvs2 23700 together with cvsclm 23732 instead. (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝐺 = (1st ‘𝑊) & ⊢ 𝑆 = (2nd ‘𝑊) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋) → (𝐴𝐺𝐴) = (2𝑆𝐴)) | ||
Theorem | vcablo 28348 | Vector addition is an Abelian group operation. (Contributed by NM, 3-Nov-2006.) (New usage is discouraged.) |
⊢ 𝐺 = (1st ‘𝑊) ⇒ ⊢ (𝑊 ∈ CVecOLD → 𝐺 ∈ AbelOp) | ||
Theorem | vcgrp 28349 | Vector addition is a group operation. (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.) |
⊢ 𝐺 = (1st ‘𝑊) ⇒ ⊢ (𝑊 ∈ CVecOLD → 𝐺 ∈ GrpOp) | ||
Theorem | vclcan 28350 | Left cancellation law for vector addition. (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.) |
⊢ 𝐺 = (1st ‘𝑊) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑊 ∈ CVecOLD ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐶𝐺𝐴) = (𝐶𝐺𝐵) ↔ 𝐴 = 𝐵)) | ||
Theorem | vczcl 28351 | The zero vector is a vector. (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.) |
⊢ 𝐺 = (1st ‘𝑊) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ (𝑊 ∈ CVecOLD → 𝑍 ∈ 𝑋) | ||
Theorem | vc0rid 28352 | The zero vector is a right identity element. (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.) |
⊢ 𝐺 = (1st ‘𝑊) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ ((𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋) → (𝐴𝐺𝑍) = 𝐴) | ||
Theorem | vc0 28353 | Zero times a vector is the zero vector. Equation 1a of [Kreyszig] p. 51. (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.) |
⊢ 𝐺 = (1st ‘𝑊) & ⊢ 𝑆 = (2nd ‘𝑊) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ ((𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋) → (0𝑆𝐴) = 𝑍) | ||
Theorem | vcz 28354 | Anything times the zero vector is the zero vector. Equation 1b of [Kreyszig] p. 51. (Contributed by NM, 24-Nov-2006.) (New usage is discouraged.) |
⊢ 𝐺 = (1st ‘𝑊) & ⊢ 𝑆 = (2nd ‘𝑊) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ ((𝑊 ∈ CVecOLD ∧ 𝐴 ∈ ℂ) → (𝐴𝑆𝑍) = 𝑍) | ||
Theorem | vcm 28355 | Minus 1 times a vector is the underlying group's inverse element. Equation 2 of [Kreyszig] p. 51. (Contributed by NM, 25-Nov-2006.) (New usage is discouraged.) |
⊢ 𝐺 = (1st ‘𝑊) & ⊢ 𝑆 = (2nd ‘𝑊) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑀 = (inv‘𝐺) ⇒ ⊢ ((𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋) → (-1𝑆𝐴) = (𝑀‘𝐴)) | ||
Theorem | isvclem 28356* | Lemma for isvcOLD 28358. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝐺 ∈ V ∧ 𝑆 ∈ V) → (〈𝐺, 𝑆〉 ∈ CVecOLD ↔ (𝐺 ∈ AbelOp ∧ 𝑆:(ℂ × 𝑋)⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ((1𝑆𝑥) = 𝑥 ∧ ∀𝑦 ∈ ℂ (∀𝑧 ∈ 𝑋 (𝑦𝑆(𝑥𝐺𝑧)) = ((𝑦𝑆𝑥)𝐺(𝑦𝑆𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑆𝑥) = ((𝑦𝑆𝑥)𝐺(𝑧𝑆𝑥)) ∧ ((𝑦 · 𝑧)𝑆𝑥) = (𝑦𝑆(𝑧𝑆𝑥)))))))) | ||
Theorem | vcex 28357 | The components of a complex vector space are sets. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
⊢ (〈𝐺, 𝑆〉 ∈ CVecOLD → (𝐺 ∈ V ∧ 𝑆 ∈ V)) | ||
Theorem | isvcOLD 28358* | The predicate "is a complex vector space." (Contributed by NM, 31-May-2008.) Obsolete version of iscvsp 23734. (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (〈𝐺, 𝑆〉 ∈ CVecOLD ↔ (𝐺 ∈ AbelOp ∧ 𝑆:(ℂ × 𝑋)⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ((1𝑆𝑥) = 𝑥 ∧ ∀𝑦 ∈ ℂ (∀𝑧 ∈ 𝑋 (𝑦𝑆(𝑥𝐺𝑧)) = ((𝑦𝑆𝑥)𝐺(𝑦𝑆𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑆𝑥) = ((𝑦𝑆𝑥)𝐺(𝑧𝑆𝑥)) ∧ ((𝑦 · 𝑧)𝑆𝑥) = (𝑦𝑆(𝑧𝑆𝑥))))))) | ||
Theorem | isvciOLD 28359* | Properties that determine a complex vector space. (Contributed by NM, 5-Nov-2006.) Obsolete version of iscvsi 23735. (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝐺 ∈ AbelOp & ⊢ dom 𝐺 = (𝑋 × 𝑋) & ⊢ 𝑆:(ℂ × 𝑋)⟶𝑋 & ⊢ (𝑥 ∈ 𝑋 → (1𝑆𝑥) = 𝑥) & ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → (𝑦𝑆(𝑥𝐺𝑧)) = ((𝑦𝑆𝑥)𝐺(𝑦𝑆𝑧))) & ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝑋) → ((𝑦 + 𝑧)𝑆𝑥) = ((𝑦𝑆𝑥)𝐺(𝑧𝑆𝑥))) & ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝑋) → ((𝑦 · 𝑧)𝑆𝑥) = (𝑦𝑆(𝑧𝑆𝑥))) & ⊢ 𝑊 = 〈𝐺, 𝑆〉 ⇒ ⊢ 𝑊 ∈ CVecOLD | ||
Theorem | cnaddabloOLD 28360 | Obsolete version of cnaddabl 18991. Complex number addition is an Abelian group operation. (Contributed by NM, 5-Nov-2006.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ + ∈ AbelOp | ||
Theorem | cnidOLD 28361 | Obsolete version of cnaddid 18992. The group identity element of complex number addition is zero. (Contributed by Steve Rodriguez, 3-Dec-2006.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 0 = (GId‘ + ) | ||
Theorem | cncvcOLD 28362 | Obsolete version of cncvs 23751. The set of complex numbers is a complex vector space. The vector operation is +, and the scalar product is ·. (Contributed by NM, 5-Nov-2006.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 〈 + , · 〉 ∈ CVecOLD | ||
Syntax | cnv 28363 | Extend class notation with the class of all normed complex vector spaces. |
class NrmCVec | ||
Syntax | cpv 28364 | Extend class notation with vector addition in a normed complex vector space. In the literature, the subscript "v" is omitted, but we need it to avoid ambiguity with complex number addition + caddc 10542. |
class +𝑣 | ||
Syntax | cba 28365 | Extend class notation with the base set of a normed complex vector space. (Note that BaseSet is capitalized because, once it is fixed for a particular vector space 𝑈, it is not a function, unlike e.g., normCV. This is our typical convention.) (New usage is discouraged.) |
class BaseSet | ||
Syntax | cns 28366 | Extend class notation with scalar multiplication in a normed complex vector space. In the literature scalar multiplication is usually indicated by juxtaposition, but we need an explicit symbol to prevent ambiguity. |
class ·𝑠OLD | ||
Syntax | cn0v 28367 | Extend class notation with zero vector in a normed complex vector space. |
class 0vec | ||
Syntax | cnsb 28368 | Extend class notation with vector subtraction in a normed complex vector space. |
class −𝑣 | ||
Syntax | cnmcv 28369 | Extend class notation with the norm function in a normed complex vector space. In the literature, the norm of 𝐴 is usually written "|| 𝐴 ||", but we use function notation to take advantage of our existing theorems about functions. |
class normCV | ||
Syntax | cims 28370 | Extend class notation with the class of the induced metrics on normed complex vector spaces. |
class IndMet | ||
Definition | df-nv 28371* | Define the class of all normed complex vector spaces. (Contributed by NM, 11-Nov-2006.) (New usage is discouraged.) |
⊢ NrmCVec = {〈〈𝑔, 𝑠〉, 𝑛〉 ∣ (〈𝑔, 𝑠〉 ∈ CVecOLD ∧ 𝑛:ran 𝑔⟶ℝ ∧ ∀𝑥 ∈ ran 𝑔(((𝑛‘𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛‘𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛‘𝑥) + (𝑛‘𝑦))))} | ||
Theorem | nvss 28372 | Structure of the class of all normed complex vectors spaces. (Contributed by NM, 28-Nov-2006.) (Revised by Mario Carneiro, 1-May-2015.) (New usage is discouraged.) |
⊢ NrmCVec ⊆ (CVecOLD × V) | ||
Theorem | nvvcop 28373 | A normed complex vector space is a vector space. (Contributed by NM, 5-Jun-2008.) (Revised by Mario Carneiro, 1-May-2015.) (New usage is discouraged.) |
⊢ (〈𝑊, 𝑁〉 ∈ NrmCVec → 𝑊 ∈ CVecOLD) | ||
Definition | df-va 28374 | Define vector addition on a normed complex vector space. (Contributed by NM, 23-Apr-2007.) (New usage is discouraged.) |
⊢ +𝑣 = (1st ∘ 1st ) | ||
Definition | df-ba 28375 | 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 28376 | 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 28377 | 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 28378 | Define vector subtraction on a normed complex vector space. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.) |
⊢ −𝑣 = ( /𝑔 ∘ +𝑣 ) | ||
Definition | df-nmcv 28379 | 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 28380 | 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 28381 | 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 28382 | 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 28383 | 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 28384 | 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 28385 | 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 28386 | 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 28387 | 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 28388 | 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 28389* | Lemma for isnv 28391. (Contributed by NM, 11-Nov-2006.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ ((𝐺 ∈ V ∧ 𝑆 ∈ V ∧ 𝑁 ∈ V) → (〈〈𝐺, 𝑆〉, 𝑁〉 ∈ NrmCVec ↔ (〈𝐺, 𝑆〉 ∈ CVecOLD ∧ 𝑁:𝑋⟶ℝ ∧ ∀𝑥 ∈ 𝑋 (((𝑁‘𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑁‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑁‘𝑥)) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦)))))) | ||
Theorem | nvex 28390 | 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 28391* | 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 28392* | 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 28393* | 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 28394 | 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 28395 | 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 28396 | 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 28397 | Mapping for the vector addition operation. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) ⇒ ⊢ (𝑈 ∈ NrmCVec → 𝐺:(𝑋 × 𝑋)⟶𝑋) | ||
Theorem | nvsf 28398 | Mapping for the scalar multiplication operation. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) ⇒ ⊢ (𝑈 ∈ NrmCVec → 𝑆:(ℂ × 𝑋)⟶𝑋) | ||
Theorem | nvgcl 28399 | 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 28400 | The vector addition (group) operation is commutative. (Contributed by NM, 4-Dec-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐺𝐵) = (𝐵𝐺𝐴)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |