![]() |
Metamath
Proof Explorer Theorem List (p. 302 of 480) | < 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: | ![]() (1-30435) |
![]() (30436-31958) |
![]() (31959-47941) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | cnv 30101 | Extend class notation with the class of all normed complex vector spaces. |
class NrmCVec | ||
Syntax | cpv 30102 | 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 11116. |
class +π£ | ||
Syntax | cba 30103 | 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 30104 | 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 30105 | Extend class notation with zero vector in a normed complex vector space. |
class 0vec | ||
Syntax | cnsb 30106 | Extend class notation with vector subtraction in a normed complex vector space. |
class βπ£ | ||
Syntax | cnmcv 30107 | 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 30108 | Extend class notation with the class of the induced metrics on normed complex vector spaces. |
class IndMet | ||
Definition | df-nv 30109* | 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 30110 | 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 30111 | 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 30112 | Define vector addition on a normed complex vector space. (Contributed by NM, 23-Apr-2007.) (New usage is discouraged.) |
β’ +π£ = (1st β 1st ) | ||
Definition | df-ba 30113 | 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 30114 | 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 30115 | 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 30116 | Define vector subtraction on a normed complex vector space. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.) |
β’ βπ£ = ( /π β +π£ ) | ||
Definition | df-nmcv 30117 | 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 30118 | 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 30119 | 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 30120 | 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 30121 | 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 30122 | 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 30123 | 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 30124 | 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 30125 | 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 30126 | 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 30127* | Lemma for isnv 30129. (Contributed by NM, 11-Nov-2006.) (New usage is discouraged.) |
β’ π = ran πΊ & β’ π = (GIdβπΊ) β β’ ((πΊ β V β§ π β V β§ π β V) β (β¨β¨πΊ, πβ©, πβ© β NrmCVec β (β¨πΊ, πβ© β CVecOLD β§ π:πβΆβ β§ βπ₯ β π (((πβπ₯) = 0 β π₯ = π) β§ βπ¦ β β (πβ(π¦ππ₯)) = ((absβπ¦) Β· (πβπ₯)) β§ βπ¦ β π (πβ(π₯πΊπ¦)) β€ ((πβπ₯) + (πβπ¦)))))) | ||
Theorem | nvex 30128 | 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 30129* | 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 30130* | 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 30131* | 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 30132 | 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 30133 | 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 30134 | 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 30135 | Mapping for the vector addition operation. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) β β’ (π β NrmCVec β πΊ:(π Γ π)βΆπ) | ||
Theorem | nvsf 30136 | Mapping for the scalar multiplication operation. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( Β·π OLD βπ) β β’ (π β NrmCVec β π:(β Γ π)βΆπ) | ||
Theorem | nvgcl 30137 | 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 30138 | The vector addition (group) operation is commutative. (Contributed by NM, 4-Dec-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) β β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (π΄πΊπ΅) = (π΅πΊπ΄)) | ||
Theorem | nvass 30139 | The vector addition (group) operation is associative. (Contributed by NM, 4-Dec-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) β β’ ((π β NrmCVec β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄πΊπ΅)πΊπΆ) = (π΄πΊ(π΅πΊπΆ))) | ||
Theorem | nvadd32 30140 | Commutative/associative law for vector addition. (Contributed by NM, 27-Dec-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) β β’ ((π β NrmCVec β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄πΊπ΅)πΊπΆ) = ((π΄πΊπΆ)πΊπ΅)) | ||
Theorem | nvrcan 30141 | Right cancellation law for vector addition. (Contributed by NM, 4-Dec-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) β β’ ((π β NrmCVec β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄πΊπΆ) = (π΅πΊπΆ) β π΄ = π΅)) | ||
Theorem | nvadd4 30142 | Rearrangement of 4 terms in a vector sum. (Contributed by NM, 8-Feb-2008.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) β β’ ((π β NrmCVec β§ (π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π)) β ((π΄πΊπ΅)πΊ(πΆπΊπ·)) = ((π΄πΊπΆ)πΊ(π΅πΊπ·))) | ||
Theorem | nvscl 30143 | 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 30144 | 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 30145 | 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 30146 | 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 30147 | 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 30148 | 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 30149 | 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 30150 | 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 30151 | 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 30152 | 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 30153 | 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 30154 | 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 30155 | 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 30156 | 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 30157 | 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 30158 | Vector subtraction in terms of group division operation. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = ( βπ£ βπ) & β’ π = ( /π βπΊ) β β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (π΄ππ΅) = (π΄ππ΅)) | ||
Theorem | nvmval 30159 | 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 30160 | 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 30161* | 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 30162 | 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 30163 | 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 30164 | Cancellation law for vector subtraction. (nnncan1 11501 analog.) (Contributed by NM, 7-Mar-2008.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( βπ£ βπ) β β’ ((π β NrmCVec β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄ππ΅)π(π΄ππΆ)) = (πΆππ΅)) | ||
Theorem | nvmdi 30165 | Distributive law for scalar product over subtraction. (Contributed by NM, 14-Feb-2008.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( βπ£ βπ) & β’ π = ( Β·π OLD βπ) β β’ ((π β NrmCVec β§ (π΄ β β β§ π΅ β π β§ πΆ β π)) β (π΄π(π΅ππΆ)) = ((π΄ππ΅)π(π΄ππΆ))) | ||
Theorem | nvnegneg 30166 | Double negative of a vector. (Contributed by NM, 4-Dec-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( Β·π OLD βπ) β β’ ((π β NrmCVec β§ π΄ β π) β (-1π(-1ππ΄)) = π΄) | ||
Theorem | nvmul0or 30167 | 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 30168 | 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 30169 | 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 30170 | Cancellation law for vector subtraction. (Contributed by NM, 27-Dec-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = ( βπ£ βπ) β β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β ((π΄πΊπ΅)ππ΄) = π΅) | ||
Theorem | nvpncan 30171 | Cancellation law for vector subtraction. (Contributed by NM, 24-Jan-2008.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = ( βπ£ βπ) β β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β ((π΄πΊπ΅)ππ΅) = π΄) | ||
Theorem | nvaddsub 30172 | Commutative/associative law for vector addition and subtraction. (Contributed by NM, 24-Jan-2008.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = ( βπ£ βπ) β β’ ((π β NrmCVec β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄πΊπ΅)ππΆ) = ((π΄ππΆ)πΊπ΅)) | ||
Theorem | nvnpcan 30173 | Cancellation law for a normed complex vector space. (Contributed by NM, 24-Jan-2008.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = ( βπ£ βπ) β β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β ((π΄ππ΅)πΊπ΅) = π΄) | ||
Theorem | nvaddsub4 30174 | 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 30175 | 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 30176 | A vector minus itself is the zero vector. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( βπ£ βπ) & β’ π = (0vecβπ) β β’ ((π β NrmCVec β§ π΄ β π) β (π΄ππ΄) = π) | ||
Theorem | nvf 30177 | Mapping for the norm function. (Contributed by NM, 11-Nov-2006.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (normCVβπ) β β’ (π β NrmCVec β π:πβΆβ) | ||
Theorem | nvcl 30178 | 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 30179 | 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 30180 | 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 30181 | 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 30182 | 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 30183 | 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 30184 | 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 30185 | The norm of a zero vector is zero. (Contributed by NM, 24-Nov-2006.) (New usage is discouraged.) |
β’ π = (0vecβπ) & β’ π = (normCVβπ) β β’ (π β NrmCVec β (πβπ) = 0) | ||
Theorem | nvz 30186 | 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 30187 | 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 30188 | Triangle inequality for the norm of a vector difference. (Contributed by NM, 27-Dec-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( βπ£ βπ) & β’ π = (normCVβπ) β β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (πβ(π΄ππ΅)) β€ ((πβπ΄) + (πβπ΅))) | ||
Theorem | nvabs 30189 | 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 30190 | 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 30191 | A nonzero norm is positive. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (0vecβπ) & β’ π = (normCVβπ) β β’ ((π β NrmCVec β§ π΄ β π) β (π΄ β π β 0 < (πβπ΄))) | ||
Theorem | nv1 30192 | 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 30193 | 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 30194 | 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 30195 | 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 30196 | 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 30197 | 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 30198 | 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 30199 | 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 30200 | 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(π΄ β π, π΄, π) β π |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |