Home | Metamath
Proof Explorer Theorem List (p. 275 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ablogrpo 27401 | An Abelian group operation is a group operation. (Contributed by NM, 2-Nov-2006.) (New usage is discouraged.) |
Theorem | ablocom 27402 | An Abelian group operation is commutative. (Contributed by NM, 2-Nov-2006.) (New usage is discouraged.) |
Theorem | ablo32 27403 | Commutative/associative law for Abelian groups. (Contributed by NM, 26-Apr-2007.) (New usage is discouraged.) |
Theorem | ablo4 27404 | Commutative/associative law for Abelian groups. (Contributed by NM, 26-Apr-2007.) (New usage is discouraged.) |
Theorem | isabloi 27405* | Properties that determine an Abelian group operation. (Contributed by NM, 5-Nov-2006.) (New usage is discouraged.) |
Theorem | ablomuldiv 27406 | Law for group multiplication and division. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.) |
Theorem | ablodivdiv 27407 | Law for double group division. (Contributed by NM, 29-Feb-2008.) (New usage is discouraged.) |
Theorem | ablodivdiv4 27408 | Law for double group division. (Contributed by NM, 29-Feb-2008.) (New usage is discouraged.) |
Theorem | ablodiv32 27409 | Swap the second and third terms in a double division. (Contributed by NM, 29-Feb-2008.) (New usage is discouraged.) |
Theorem | ablonnncan 27410 | Cancellation law for group division. (nnncan 10316 analog.) (Contributed by NM, 29-Feb-2008.) (New usage is discouraged.) |
Theorem | ablonncan 27411 | Cancellation law for group division. (nncan 10310 analog.) (Contributed by NM, 7-Mar-2008.) (New usage is discouraged.) |
Theorem | ablonnncan1 27412 | Cancellation law for group division. (nnncan1 10317 analog.) (Contributed by NM, 7-Mar-2008.) (New usage is discouraged.) |
Syntax | cvc 27413 | Extend class notation with the class of all complex vector spaces. |
Definition | df-vc 27414* | Define the class of all complex vector spaces. (Contributed by NM, 3-Nov-2006.) (New usage is discouraged.) |
Theorem | vcrel 27415 | The class of all complex vector spaces is a relation. (Contributed by NM, 17-Mar-2007.) (New usage is discouraged.) |
Theorem | vciOLD 27416* | Obsolete version of cvsi 22930 as of 21-Sep-2021. 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 is already used for the universal class. (Contributed by NM, 3-Nov-2006.) (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | vcsm 27417 | Functionality of th scalar product of a complex vector space. (Contributed by NM, 3-Nov-2006.) (New usage is discouraged.) |
Theorem | vccl 27418 | Closure of the scalar product of a complex vector space. (Contributed by NM, 3-Nov-2006.) (New usage is discouraged.) |
Theorem | vcidOLD 27419 | Identity element for the scalar product of a complex vector space. (Contributed by NM, 3-Nov-2006.) Obsolete as of 21-Sep-2021. Use clmvs1 22893 together with cvsclm 22926 instead. (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | vcdi 27420 | Distributive law for the scalar product of a complex vector space. (Contributed by NM, 3-Nov-2006.) (New usage is discouraged.) |
Theorem | vcdir 27421 | Distributive law for the scalar product of a complex vector space. (Contributed by NM, 3-Nov-2006.) (New usage is discouraged.) |
Theorem | vcass 27422 | Associative law for the scalar product of a complex vector space. (Contributed by NM, 3-Nov-2006.) (New usage is discouraged.) |
Theorem | vc2OLD 27423 | A vector plus itself is two times the vector. (Contributed by NM, 1-Feb-2007.) Obsolete as of 21-Sep-2021. Use clmvs2 22894 together with cvsclm 22926 instead. (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | vcablo 27424 | Vector addition is an Abelian group operation. (Contributed by NM, 3-Nov-2006.) (New usage is discouraged.) |
Theorem | vcgrp 27425 | Vector addition is a group operation. (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.) |
Theorem | vclcan 27426 | Left cancellation law for vector addition. (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.) |
Theorem | vczcl 27427 | The zero vector is a vector. (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.) |
GId | ||
Theorem | vc0rid 27428 | The zero vector is a right identity element. (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.) |
GId | ||
Theorem | vc0 27429 | Zero times a vector is the zero vector. Equation 1a of [Kreyszig] p. 51. (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.) |
GId | ||
Theorem | vcz 27430 | 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.) |
GId | ||
Theorem | vcm 27431 | 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.) |
Theorem | isvclem 27432* | Lemma for isvcOLD 27434. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
Theorem | vcex 27433 | The components of a complex vector space are sets. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
Theorem | isvcOLD 27434* | The predicate "is a complex vector space." (Contributed by NM, 31-May-2008.) Obsolete as of 4-Oct-2021. Use iscvsp 22928 instead. (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | isvciOLD 27435* | Properties that determine a complex vector space. (Contributed by NM, 5-Nov-2006.) Obsolete as of 4-Oct-2021. Use iscvsi 22929 instead. (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | cnaddabloOLD 27436 | Obsolete as of 23-Jan-2020. Use cnaddabl 18272 instead. Complex number addition is an Abelian group operation. (Contributed by NM, 5-Nov-2006.) (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | cnidOLD 27437 | Obsolete as of 23-Jan-2020. Use cnaddid 18273 instead. 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.) |
GId | ||
Theorem | cncvcOLD 27438 | Obsolete version of cncvs 22945 as of 20-Sep-2021. 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.) |
Syntax | cnv 27439 | Extend class notation with the class of all normed complex vector spaces. |
Syntax | cpv 27440 | 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 9939. |
Syntax | cba 27441 | Extend class notation with the base set of a normed complex vector space. (Note that is capitalized because, once it is fixed for a particular vector space , it is not a function, unlike e.g. CV. This is our typical convention.) (New usage is discouraged.) |
Syntax | cns 27442 | 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. |
Syntax | cn0v 27443 | Extend class notation with zero vector in a normed complex vector space. |
Syntax | cnsb 27444 | Extend class notation with vector subtraction in a normed complex vector space. |
Syntax | cnmcv 27445 | 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. |
CV | ||
Syntax | cims 27446 | Extend class notation with the class of the induced metrics on normed complex vector spaces. |
Definition | df-nv 27447* | Define the class of all normed complex vector spaces. (Contributed by NM, 11-Nov-2006.) (New usage is discouraged.) |
GId | ||
Theorem | nvss 27448 | 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.) |
Theorem | nvvcop 27449 | 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.) |
Definition | df-va 27450 | Define vector addition on a normed complex vector space. (Contributed by NM, 23-Apr-2007.) (New usage is discouraged.) |
Definition | df-ba 27451 | Define the base set of a normed complex vector space. (Contributed by NM, 23-Apr-2007.) (New usage is discouraged.) |
Definition | df-sm 27452 | Define scalar multiplication on a normed complex vector space. (Contributed by NM, 24-Apr-2007.) (New usage is discouraged.) |
Definition | df-0v 27453 | Define the zero vector in a normed complex vector space. (Contributed by NM, 24-Apr-2007.) (New usage is discouraged.) |
GId | ||
Definition | df-vs 27454 | Define vector subtraction on a normed complex vector space. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.) |
Definition | df-nmcv 27455 | Define the norm function in a normed complex vector space. (Contributed by NM, 25-Apr-2007.) (New usage is discouraged.) |
CV | ||
Definition | df-ims 27456 | Define the induced metric on a normed complex vector space. (Contributed by NM, 11-Sep-2007.) (New usage is discouraged.) |
CV | ||
Theorem | nvrel 27457 | The class of all normed complex vectors spaces is a relation. (Contributed by NM, 14-Nov-2006.) (New usage is discouraged.) |
Theorem | vafval 27458 | 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.) |
Theorem | bafval 27459 | 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.) |
Theorem | smfval 27460 | 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.) |
Theorem | 0vfval 27461 | 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.) |
GId | ||
Theorem | nmcvfval 27462 | Value of the norm function in a normed complex vector space. (Contributed by NM, 25-Apr-2007.) (New usage is discouraged.) |
CV | ||
Theorem | nvop2 27463 | 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.) |
CV | ||
Theorem | nvvop 27464 | 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.) |
Theorem | isnvlem 27465* | Lemma for isnv 27467. (Contributed by NM, 11-Nov-2006.) (New usage is discouraged.) |
GId | ||
Theorem | nvex 27466 | 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.) |
Theorem | isnv 27467* | The predicate "is a normed complex vector space." (Contributed by NM, 5-Jun-2008.) (New usage is discouraged.) |
GId | ||
Theorem | isnvi 27468* | Properties that determine a normed complex vector space. (Contributed by NM, 15-Apr-2007.) (New usage is discouraged.) |
GId | ||
Theorem | nvi 27469* | 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.) |
CV | ||
Theorem | nvvc 27470 | 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.) |
Theorem | nvablo 27471 | The vector addition operation of a normed complex vector space is an Abelian group. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.) |
Theorem | nvgrp 27472 | The vector addition operation of a normed complex vector space is a group. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.) |
Theorem | nvgf 27473 | Mapping for the vector addition operation. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.) |
Theorem | nvsf 27474 | Mapping for the scalar multiplication operation. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.) |
Theorem | nvgcl 27475 | Closure law for the vector addition (group) operation of a normed complex vector space. (Contributed by NM, 23-Apr-2007.) (New usage is discouraged.) |
Theorem | nvcom 27476 | The vector addition (group) operation is commutative. (Contributed by NM, 4-Dec-2007.) (New usage is discouraged.) |
Theorem | nvass 27477 | The vector addition (group) operation is associative. (Contributed by NM, 4-Dec-2007.) (New usage is discouraged.) |
Theorem | nvadd32 27478 | Commutative/associative law for vector addition. (Contributed by NM, 27-Dec-2007.) (New usage is discouraged.) |
Theorem | nvrcan 27479 | Right cancellation law for vector addition. (Contributed by NM, 4-Dec-2007.) (New usage is discouraged.) |
Theorem | nvadd4 27480 | Rearrangement of 4 terms in a vector sum. (Contributed by NM, 8-Feb-2008.) (New usage is discouraged.) |
Theorem | nvscl 27481 | Closure law for the scalar product operation of a normed complex vector space. (Contributed by NM, 1-Feb-2007.) (New usage is discouraged.) |
Theorem | nvsid 27482 | Identity element for the scalar product of a normed complex vector space. (Contributed by NM, 4-Dec-2007.) (New usage is discouraged.) |
Theorem | nvsass 27483 | Associative law for the scalar product of a normed complex vector space. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.) |
Theorem | nvscom 27484 | Commutative law for the scalar product of a normed complex vector space. (Contributed by NM, 14-Feb-2008.) (New usage is discouraged.) |
Theorem | nvdi 27485 | Distributive law for the scalar product of a complex vector space. (Contributed by NM, 4-Dec-2007.) (New usage is discouraged.) |
Theorem | nvdir 27486 | Distributive law for the scalar product of a complex vector space. (Contributed by NM, 4-Dec-2007.) (New usage is discouraged.) |
Theorem | nv2 27487 | A vector plus itself is two times the vector. (Contributed by NM, 9-Feb-2008.) (New usage is discouraged.) |
Theorem | vsfval 27488 | 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 27489 | 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.) |
Theorem | nv0rid 27490 | 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.) |
Theorem | nv0lid 27491 | 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.) |
Theorem | nv0 27492 | 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.) |
Theorem | nvsz 27493 | 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.) |
Theorem | nvinv 27494 | 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.) |
Theorem | nvinvfval 27495 | 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.) |
Theorem | nvm 27496 | Vector subtraction in terms of group division operation. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.) |
Theorem | nvmval 27497 | Value of vector subtraction on a normed complex vector space. (Contributed by NM, 11-Sep-2007.) (New usage is discouraged.) |
Theorem | nvmval2 27498 | Value of vector subtraction on a normed complex vector space. (Contributed by Mario Carneiro, 19-Nov-2013.) (New usage is discouraged.) |
Theorem | nvmfval 27499* | 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.) |
Theorem | nvmf 27500 | Mapping for the vector subtraction operation. (Contributed by NM, 11-Sep-2007.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |