P. 255 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 25401-25500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	rngomndo 25401	In a unital ring the multiplication is a monoid. (Contributed by FL, 24-Jan-2010.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.)
|- H = ( 2nd ` R )   =>    |- ( R e. RingOps -> H e. MndOp )
Theorem	rngoablo2 25402	In a unital ring the addition is an abelian group. (Contributed by FL, 31-Aug-2009.) (New usage is discouraged.)
|- ( <. G , H >. e. RingOps -> G e. AbelOp )
Theorem	rngoidmlem 25403	The unit of a ring is an identity element for the multiplication. (Contributed by FL, 18-Feb-2010.) (New usage is discouraged.)
|- H = ( 2nd ` R )   &    |- X = ran ( 1st ` R )   &    |- U = (GId ` H )   =>    |- ( ( R e. RingOps /\ A e. X ) -> ( ( U H A ) = A /\ ( A H U ) = A ) )
Theorem	rngolidm 25404	The unit of a ring is an identity element for the multiplication. (Contributed by FL, 18-Apr-2010.) (New usage is discouraged.)
|- H = ( 2nd ` R )   &    |- X = ran ( 1st ` R )   &    |- U = (GId ` H )   =>    |- ( ( R e. RingOps /\ A e. X ) -> ( U H A ) = A )
Theorem	rngoridm 25405	The unit of a ring is an identity element for the multiplication. (Contributed by FL, 18-Apr-2010.) (New usage is discouraged.)
|- H = ( 2nd ` R )   &    |- X = ran ( 1st ` R )   &    |- U = (GId ` H )   =>    |- ( ( R e. RingOps /\ A e. X ) -> ( A H U ) = A )
Theorem	rngosn3 25406	Obsolete as of 25-Jan-2020. Use ring1zr 17902 or srg1zr 17159 instead. The only unital ring with a base set consisting in one element is the zero ring. (Contributed by FL, 13-Feb-2010.) (Proof shortened by Mario Carneiro, 30-Apr-2015.) (New usage is discouraged.)
|- G = ( 1st ` R )   &    |- X = ran G   =>    |- ( ( R e. RingOps /\ A e. B ) -> ( X = { A } <-> R = <. { <. <. A , A >. , A >. } , { <. <. A , A >. , A >. } >. ) )
Theorem	rngosn4 25407	Obsolete as of 25-Jan-2020. Use rngen1zr 17903 instead. The only unital ring with one element is the zero ring. (Contributed by FL, 14-Feb-2010.) (Revised by Mario Carneiro, 30-Apr-2015.) (New usage is discouraged.)
|- G = ( 1st ` R )   &    |- X = ran G   =>    |- ( ( R e. RingOps /\ A e. X ) -> ( X ~~ 1o <-> R = <. { <. <. A , A >. , A >. } , { <. <. A , A >. , A >. } >. ) )
Theorem	rngosn6 25408	Obsolete as of 25-Jan-2020. Use ringen1zr 17904 or srgen1zr 17160 instead. The only unital ring with one element is the zero ring. (Contributed by FL, 15-Feb-2010.) (New usage is discouraged.)
|- G = ( 1st ` R )   &    |- X = ran G   &    |- Z = (GId ` G )   =>    |- ( R e. RingOps -> ( X ~~ 1o <-> R = <. { <. <. Z , Z >. , Z >. } , { <. <. Z , Z >. , Z >. } >. ) )
Theorem	rngo1cl 25409	The unit of a ring belongs to the base set. (Contributed by FL, 12-Feb-2010.) (New usage is discouraged.)
|- X = ran ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- U = (GId ` H )   =>    |- ( R e. RingOps -> U e. X )
Theorem	rngoueqz 25410	Obsolete as of 23-Jan-2020. Use 0ring01eqbi 17900 instead. In a unital ring the zero equals the unity iff the ring is the zero ring. (Contributed by FL, 14-Feb-2010.) (New usage is discouraged.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- Z = (GId ` G )   &    |- U = (GId ` H )   &    |- X = ran G   =>    |- ( R e. RingOps -> ( X ~~ 1o <-> U = Z ) )
Theorem	isdivrngo 25411	The predicate "is a division ring". (Contributed by FL, 6-Sep-2009.) (New usage is discouraged.)
|- ( H e. A -> ( <. G , H >. e. DivRingOps <-> ( <. G , H >. e. RingOps /\ ( H |` ( ( ran G \ { (GId ` G ) } ) X. ( ran G \ { (GId ` G ) } ) ) ) e. GrpOp ) ) )
Theorem	zrdivrng 25412	The zero ring is not a division ring. (Contributed by FL, 24-Jan-2010.) (Proof shortened by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.)
|- A e. _V   =>    |- -. <. { <. <. A , A >. , A >. } , { <. <. A , A >. , A >. } >. e. DivRingOps
Theorem	dvrunz 25413	In a division ring the unit is different from the zero. (Contributed by FL, 14-Feb-2010.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- X = ran G   &    |- Z = (GId ` G )   &    |- U = (GId ` H )   =>    |- ( R e. DivRingOps -> U =/= Z )
Theorem	zerdivemp1 25414*	In a unitary ring a left invertible element is not a zero divisor. (Contributed by FL, 18-Apr-2010.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- Z = (GId ` G )   &    |- X = ran G   &    |- U = (GId ` H )   =>    |- ( ( R e. RingOps /\ A e. ( X \ Z ) /\ E. a e. X ( a H A ) = U ) -> ( B e. X -> ( ( A H B ) = Z -> B = Z ) ) )
Theorem	rngoridfz 25415*	In a unitary ring a left invertible element is different from zero iff 1 =/= 0. (Contributed by FL, 18-Apr-2010.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- Z = (GId ` G )   &    |- X = ran G   &    |- U = (GId ` H )   =>    |- ( ( R e. RingOps /\ A e. X /\ E. a e. X ( a H A ) = U ) -> ( A =/= Z <-> U =/= Z ) )
PART 19  COMPLEX TOPOLOGICAL VECTOR SPACES (DEPRECATED) The intent is for this deprecated section to be deleted once its theorems have extensible structure versions (or are not useful). You can make a list of "terminal" theorems (i.e. theorems not referenced by anything else) and for each theorem see if there exists an extensible structure version (or decide it's not useful), and if so, delete it. Then repeat this recursively. One way to search for terminal theorems is to log the output ("open log x.txt") of "show usage WHATEVER" in metamath.exe and search for "(None)".
19.1  Complex vector spaces
19.1.1  Definition and basic properties
Syntax	cvc 25416	Extend class notation with the class of all complex vector spaces.
class CVecOLD
Definition	df-vc 25417*	Define the class of all complex vector spaces. (Contributed by NM, 3-Nov-2006.) (New usage is discouraged.)
|- CVecOLD = { <. g , s >. | ( g e. AbelOp /\ s : ( CC X. ran g ) --> ran g /\ A. x e. ran g ( ( 1 s x ) = x /\ A. y e. CC ( A. z e. ran g ( y s ( x g z ) ) = ( ( y s x ) g ( y s z ) ) /\ A. z e. CC ( ( ( y + z ) s x ) = ( ( y s x ) g ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) ) ) ) ) }
Theorem	vcrel 25418	The class of all complex vector spaces is a relation. (Contributed by NM, 17-Mar-2007.) (New usage is discouraged.)
|- Rel CVecOLD
Theorem	vci 25419*	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 W was chosen because _V is already used for the universal class. (Contributed by NM, 3-Nov-2006.) (New usage is discouraged.)
|- G = ( 1st ` W )   &    |- S = ( 2nd ` W )   &    |- X = ran G   =>    |- ( W e. CVecOLD -> ( G e. AbelOp /\ S : ( CC X. X ) --> X /\ A. x e. X ( ( 1 S x ) = x /\ A. y e. CC ( A. z e. X ( y S ( x G z ) ) = ( ( y S x ) G ( y S z ) ) /\ A. z e. CC ( ( ( y + z ) S x ) = ( ( y S x ) G ( z S x ) ) /\ ( ( y x. z ) S x ) = ( y S ( z S x ) ) ) ) ) ) )
Theorem	vcsm 25420	Functionality of th scalar product of a complex vector space. (Contributed by NM, 3-Nov-2006.) (New usage is discouraged.)
|- G = ( 1st ` W )   &    |- S = ( 2nd ` W )   &    |- X = ran G   =>    |- ( W e. CVecOLD -> S : ( CC X. X ) --> X )
Theorem	vccl 25421	Closure of the scalar product of a complex vector space. (Contributed by NM, 3-Nov-2006.) (New usage is discouraged.)
|- G = ( 1st ` W )   &    |- S = ( 2nd ` W )   &    |- X = ran G   =>    |- ( ( W e. CVecOLD /\ A e. CC /\ B e. X ) -> ( A S B ) e. X )
Theorem	vcid 25422	Identity element for the scalar product of a complex vector space. (Contributed by NM, 3-Nov-2006.) (New usage is discouraged.)
|- G = ( 1st ` W )   &    |- S = ( 2nd ` W )   &    |- X = ran G   =>    |- ( ( W e. CVecOLD /\ A e. X ) -> ( 1 S A ) = A )
Theorem	vcdi 25423	Distributive law for the scalar product of a complex vector space. (Contributed by NM, 3-Nov-2006.) (New usage is discouraged.)
|- G = ( 1st ` W )   &    |- S = ( 2nd ` W )   &    |- X = ran G   =>    |- ( ( W e. CVecOLD /\ ( A e. CC /\ B e. X /\ C e. X ) ) -> ( A S ( B G C ) ) = ( ( A S B ) G ( A S C ) ) )
Theorem	vcdir 25424	Distributive law for the scalar product of a complex vector space. (Contributed by NM, 3-Nov-2006.) (New usage is discouraged.)
|- G = ( 1st ` W )   &    |- S = ( 2nd ` W )   &    |- X = ran G   =>    |- ( ( W e. CVecOLD /\ ( A e. CC /\ B e. CC /\ C e. X ) ) -> ( ( A + B ) S C ) = ( ( A S C ) G ( B S C ) ) )
Theorem	vcass 25425	Associative law for the scalar product of a complex vector space. (Contributed by NM, 3-Nov-2006.) (New usage is discouraged.)
|- G = ( 1st ` W )   &    |- S = ( 2nd ` W )   &    |- X = ran G   =>    |- ( ( W e. CVecOLD /\ ( A e. CC /\ B e. CC /\ C e. X ) ) -> ( ( A x. B ) S C ) = ( A S ( B S C ) ) )
Theorem	vc2 25426	A vector plus itself is two times the vector. (Contributed by NM, 1-Feb-2007.) (New usage is discouraged.)
|- G = ( 1st ` W )   &    |- S = ( 2nd ` W )   &    |- X = ran G   =>    |- ( ( W e. CVecOLD /\ A e. X ) -> ( A G A ) = ( 2 S A ) )
Theorem	vcsubdir 25427	Subtractive distributive law for the scalar product of a complex vector space. (Contributed by NM, 31-Jul-2007.) (New usage is discouraged.)
|- G = ( 1st ` W )   &    |- S = ( 2nd ` W )   &    |- X = ran G   =>    |- ( ( W e. CVecOLD /\ ( A e. CC /\ B e. CC /\ C e. X ) ) -> ( ( A - B ) S C ) = ( ( A S C ) G ( -u 1 S ( B S C ) ) ) )
Theorem	vcablo 25428	Vector addition is an Abelian group operation. (Contributed by NM, 3-Nov-2006.) (New usage is discouraged.)
|- G = ( 1st ` W )   =>    |- ( W e. CVecOLD -> G e. AbelOp )
Theorem	vcgrp 25429	Vector addition is a group operation. (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.)
|- G = ( 1st ` W )   =>    |- ( W e. CVecOLD -> G e. GrpOp )
Theorem	vcgcl 25430	Closure law for the vector addition (group) operation of a complex vector space. (Contributed by NM, 1-Feb-2007.) (New usage is discouraged.)
|- G = ( 1st ` W )   &    |- X = ran G   =>    |- ( ( W e. CVecOLD /\ A e. X /\ B e. X ) -> ( A G B ) e. X )
Theorem	vccom 25431	Vector addition is commutative. (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.)
|- G = ( 1st ` W )   &    |- X = ran G   =>    |- ( ( W e. CVecOLD /\ A e. X /\ B e. X ) -> ( A G B ) = ( B G A ) )
Theorem	vcaass 25432	Vector addition is associative. (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.)
|- G = ( 1st ` W )   &    |- X = ran G   =>    |- ( ( W e. CVecOLD /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A G B ) G C ) = ( A G ( B G C ) ) )
Theorem	vca32 25433	Commutative/associative law that swaps the last two terms in a triple vector sum. (Contributed by NM, 5-Aug-2007.) (New usage is discouraged.)
|- G = ( 1st ` W )   &    |- X = ran G   =>    |- ( ( W e. CVecOLD /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A G B ) G C ) = ( ( A G C ) G B ) )
Theorem	vca4 25434	Rearrangement of 4 terms in a vector sum. (Contributed by NM, 5-Aug-2007.) (New usage is discouraged.)
|- G = ( 1st ` W )   &    |- X = ran G   =>    |- ( ( W e. CVecOLD /\ ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) -> ( ( A G B ) G ( C G D ) ) = ( ( A G C ) G ( B G D ) ) )
Theorem	vcrcan 25435	Right cancellation law for vector addition. (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.)
|- G = ( 1st ` W )   &    |- X = ran G   =>    |- ( ( W e. CVecOLD /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A G C ) = ( B G C ) <-> A = B ) )
Theorem	vclcan 25436	Left cancellation law for vector addition. (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.)
|- G = ( 1st ` W )   &    |- X = ran G   =>    |- ( ( W e. CVecOLD /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( C G A ) = ( C G B ) <-> A = B ) )
Theorem	vczcl 25437	The zero vector is a vector. (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.)
|- G = ( 1st ` W )   &    |- X = ran G   &    |- Z = (GId ` G )   =>    |- ( W e. CVecOLD -> Z e. X )
Theorem	vc0rid 25438	The zero vector is a right identity element. (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.)
|- G = ( 1st ` W )   &    |- X = ran G   &    |- Z = (GId ` G )   =>    |- ( ( W e. CVecOLD /\ A e. X ) -> ( A G Z ) = A )
Theorem	vc0lid 25439	The zero vector is a left identity element. (Contributed by NM, 26-Apr-2007.) (New usage is discouraged.)
|- G = ( 1st ` W )   &    |- X = ran G   &    |- Z = (GId ` G )   =>    |- ( ( W e. CVecOLD /\ A e. X ) -> ( Z G A ) = A )
Theorem	vc0 25440	Zero times a vector is the zero vector. Equation 1a of [Kreyszig] p. 51. (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.)
|- G = ( 1st ` W )   &    |- S = ( 2nd ` W )   &    |- X = ran G   &    |- Z = (GId ` G )   =>    |- ( ( W e. CVecOLD /\ A e. X ) -> ( 0 S A ) = Z )
Theorem	vcz 25441	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.)
|- G = ( 1st ` W )   &    |- S = ( 2nd ` W )   &    |- X = ran G   &    |- Z = (GId ` G )   =>    |- ( ( W e. CVecOLD /\ A e. CC ) -> ( A S Z ) = Z )
Theorem	vcm 25442	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.)
|- G = ( 1st ` W )   &    |- S = ( 2nd ` W )   &    |- X = ran G   &    |- M = ( inv ` G )   =>    |- ( ( W e. CVecOLD /\ A e. X ) -> ( -u 1 S A ) = ( M ` A ) )
Theorem	vcrinv 25443	A vector minus itself. (Contributed by NM, 4-Dec-2006.) (New usage is discouraged.)
|- G = ( 1st ` W )   &    |- S = ( 2nd ` W )   &    |- X = ran G   &    |- Z = (GId ` G )   =>    |- ( ( W e. CVecOLD /\ A e. X ) -> ( A G ( -u 1 S A ) ) = Z )
Theorem	vclinv 25444	Minus a vector plus itself. (Contributed by NM, 4-Dec-2006.) (New usage is discouraged.)
|- G = ( 1st ` W )   &    |- S = ( 2nd ` W )   &    |- X = ran G   &    |- Z = (GId ` G )   =>    |- ( ( W e. CVecOLD /\ A e. X ) -> ( ( -u 1 S A ) G A ) = Z )
Theorem	vcnegneg 25445	Double negative of a vector. (Contributed by NM, 6-Aug-2007.) (New usage is discouraged.)
|- G = ( 1st ` W )   &    |- S = ( 2nd ` W )   &    |- X = ran G   =>    |- ( ( W e. CVecOLD /\ A e. X ) -> ( -u 1 S ( -u 1 S A ) ) = A )
Theorem	vcnegsubdi2 25446	Distribution of negative over vector subtraction. (Contributed by NM, 6-Aug-2007.) (New usage is discouraged.)
|- G = ( 1st ` W )   &    |- S = ( 2nd ` W )   &    |- X = ran G   =>    |- ( ( W e. CVecOLD /\ A e. X /\ B e. X ) -> ( -u 1 S ( A G ( -u 1 S B ) ) ) = ( B G ( -u 1 S A ) ) )
Theorem	vcsub4 25447	Rearrangement of 4 terms in a mixed vector addition and subtraction. (Contributed by NM, 5-Aug-2007.) (New usage is discouraged.)
|- G = ( 1st ` W )   &    |- S = ( 2nd ` W )   &    |- X = ran G   =>    |- ( ( W e. CVecOLD /\ ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) -> ( ( A G B ) G ( -u 1 S ( C G D ) ) ) = ( ( A G ( -u 1 S C ) ) G ( B G ( -u 1 S D ) ) ) )
Theorem	isvclem 25448*	Lemma for isvc 25452. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
|- X = ran G   =>    |- ( ( G e. _V /\ S e. _V ) -> ( <. G , S >. e. CVecOLD <-> ( G e. AbelOp /\ S : ( CC X. X ) --> X /\ A. x e. X ( ( 1 S x ) = x /\ A. y e. CC ( A. z e. X ( y S ( x G z ) ) = ( ( y S x ) G ( y S z ) ) /\ A. z e. CC ( ( ( y + z ) S x ) = ( ( y S x ) G ( z S x ) ) /\ ( ( y x. z ) S x ) = ( y S ( z S x ) ) ) ) ) ) ) )
Theorem	vcoprnelem 25449	Lemma for vcoprne 25450. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
|- ( <. G , G >. e. CVecOLD -> G : ( CC X. CC ) --> CC )
Theorem	vcoprne 25450	The operations of a complex vector space cannot be identical. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
|- ( <. G , S >. e. CVecOLD -> G =/= S )
Theorem	vcex 25451	The components of a complex vector space are sets. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
|- ( <. G , S >. e. CVecOLD -> ( G e. _V /\ S e. _V ) )
Theorem	isvc 25452*	The predicate "is a complex vector space." (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
|- X = ran G   =>    |- ( <. G , S >. e. CVecOLD <-> ( G e. AbelOp /\ S : ( CC X. X ) --> X /\ A. x e. X ( ( 1 S x ) = x /\ A. y e. CC ( A. z e. X ( y S ( x G z ) ) = ( ( y S x ) G ( y S z ) ) /\ A. z e. CC ( ( ( y + z ) S x ) = ( ( y S x ) G ( z S x ) ) /\ ( ( y x. z ) S x ) = ( y S ( z S x ) ) ) ) ) ) )
Theorem	isvci 25453*	Properties that determine a complex vector space. (Contributed by NM, 5-Nov-2006.) (New usage is discouraged.)
|- G e. AbelOp   &    |- dom G = ( X X. X )   &    |- S : ( CC X. X ) --> X   &    |- ( x e. X -> ( 1 S x ) = x )   &    |- ( ( y e. CC /\ x e. X /\ z e. X ) -> ( y S ( x G z ) ) = ( ( y S x ) G ( y S z ) ) )   &    |- ( ( y e. CC /\ z e. CC /\ x e. X ) -> ( ( y + z ) S x ) = ( ( y S x ) G ( z S x ) ) )   &    |- ( ( y e. CC /\ z e. CC /\ x e. X ) -> ( ( y x. z ) S x ) = ( y S ( z S x ) ) )   &    |- W = <. G , S >.   =>    |- W e. CVecOLD
19.1.2  Examples of complex vector spaces
Theorem	cncvc 25454	The set of complex numbers is a complex vector space. The vector operation is +, and the scalar product is x.. (Contributed by NM, 5-Nov-2006.) (New usage is discouraged.)
|- <. + , x. >. e. CVecOLD
19.2  Normed complex vector spaces
19.2.1  Definition and basic properties
Syntax	cnv 25455	Extend class notation with the class of all normed complex vector spaces.
class NrmCVec
Syntax	cpv 25456	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 9498.
class +v
Syntax	cba 25457	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 U, it is not a function, unlike e.g. normCV. This is our typical convention.) (New usage is discouraged.)
class BaseSet
Syntax	cns 25458	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 .sOLD
Syntax	cn0v 25459	Extend class notation with zero vector in a normed complex vector space.
class 0vec
Syntax	cnsb 25460	Extend class notation with vector subtraction in a normed complex vector space.
class -v
Syntax	cnmcv 25461	Extend class notation with the norm function in a normed complex vector space. In the literature, the norm of A is usually written "|| A ||", but we use function notation to take advantage of our existing theorems about functions.
class normCV
Syntax	cims 25462	Extend class notation with the class of the induced metrics on normed complex vector spaces.
class IndMet
Definition	df-nv 25463*	Define the class of all normed complex vector spaces. (Contributed by NM, 11-Nov-2006.) (New usage is discouraged.)
|- NrmCVec = { <. <. g , s >. , n >. | ( <. g , s >. e. CVecOLD /\ n : ran g --> RR /\ A. x e. ran g ( ( ( n ` x ) = 0 -> x = (GId ` g ) ) /\ A. y e. CC ( n ` ( y s x ) ) = ( ( abs ` y ) x. ( n ` x ) ) /\ A. y e. ran g ( n ` ( x g y ) ) <_ ( ( n ` x ) + ( n ` y ) ) ) ) }
Theorem	nvss 25464	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 C_ ( CVecOLD X. _V )
Theorem	nvvcop 25465	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.)
|- ( <. W , N >. e. NrmCVec -> W e. CVecOLD )
Definition	df-va 25466	Define vector addition on a normed complex vector space. (Contributed by NM, 23-Apr-2007.) (New usage is discouraged.)
|- +v = ( 1st o. 1st )
Definition	df-ba 25467	Define the base set of a normed complex vector space. (Contributed by NM, 23-Apr-2007.) (New usage is discouraged.)
|- BaseSet = ( x e. _V |-> ran ( +v ` x ) )
Definition	df-sm 25468	Define scalar multiplication on a normed complex vector space. (Contributed by NM, 24-Apr-2007.) (New usage is discouraged.)
|- .sOLD = ( 2nd o. 1st )
Definition	df-0v 25469	Define the zero vector in a normed complex vector space. (Contributed by NM, 24-Apr-2007.) (New usage is discouraged.)
|- 0vec = (GId o. +v )
Definition	df-vs 25470	Define vector subtraction on a normed complex vector space. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.)
|- -v = ( /g o. +v )
Definition	df-nmcv 25471	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 25472	Define the induced metric on a normed complex vector space. (Contributed by NM, 11-Sep-2007.) (New usage is discouraged.)
|- IndMet = ( u e. NrmCVec |-> ( ( normCV ` u ) o. ( -v ` u ) ) )
Theorem	nvrel 25473	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 25474	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.)
|- G = ( +v ` U )   =>    |- G = ( 1st ` ( 1st ` U ) )
Theorem	bafval 25475	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.)
|- X = ( BaseSet ` U )   &    |- G = ( +v ` U )   =>    |- X = ran G
Theorem	smfval 25476	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.)
|- S = ( .sOLD ` U )   =>    |- S = ( 2nd ` ( 1st ` U ) )
Theorem	0vfval 25477	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.)
|- G = ( +v ` U )   &    |- Z = ( 0vec ` U )   =>    |- ( U e. V -> Z = (GId ` G ) )
Theorem	nmcvfval 25478	Value of the norm function in a normed complex vector space. (Contributed by NM, 25-Apr-2007.) (New usage is discouraged.)
|- N = ( normCV ` U )   =>    |- N = ( 2nd ` U )
Theorem	nvop2 25479	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.)
|- W = ( 1st ` U )   &    |- N = ( normCV ` U )   =>    |- ( U e. NrmCVec -> U = <. W , N >. )
Theorem	nvvop 25480	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.)
|- W = ( 1st ` U )   &    |- G = ( +v ` U )   &    |- S = ( .sOLD ` U )   =>    |- ( U e. NrmCVec -> W = <. G , S >. )
Theorem	isnvlem 25481*	Lemma for isnv 25483. (Contributed by NM, 11-Nov-2006.) (New usage is discouraged.)
|- X = ran G   &    |- Z = (GId ` G )   =>    |- ( ( G e. _V /\ S e. _V /\ N e. _V ) -> ( <. <. G , S >. , N >. e. NrmCVec <-> ( <. G , S >. e. CVecOLD /\ N : X --> RR /\ A. x e. X ( ( ( N ` x ) = 0 -> x = Z ) /\ A. y e. CC ( N ` ( y S x ) ) = ( ( abs ` y ) x. ( N ` x ) ) /\ A. y e. X ( N ` ( x G y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) ) )
Theorem	nvex 25482	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.)
|- ( <. <. G , S >. , N >. e. NrmCVec -> ( G e. _V /\ S e. _V /\ N e. _V ) )
Theorem	isnv 25483*	The predicate "is a normed complex vector space." (Contributed by NM, 5-Jun-2008.) (New usage is discouraged.)
|- X = ran G   &    |- Z = (GId ` G )   =>    |- ( <. <. G , S >. , N >. e. NrmCVec <-> ( <. G , S >. e. CVecOLD /\ N : X --> RR /\ A. x e. X ( ( ( N ` x ) = 0 -> x = Z ) /\ A. y e. CC ( N ` ( y S x ) ) = ( ( abs ` y ) x. ( N ` x ) ) /\ A. y e. X ( N ` ( x G y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) )
Theorem	isnvi 25484*	Properties that determine a normed complex vector space. (Contributed by NM, 15-Apr-2007.) (New usage is discouraged.)
|- X = ran G   &    |- Z = (GId ` G )   &    |- <. G , S >. e. CVecOLD   &    |- N : X --> RR   &    |- ( ( x e. X /\ ( N ` x ) = 0 ) -> x = Z )   &    |- ( ( y e. CC /\ x e. X ) -> ( N ` ( y S x ) ) = ( ( abs ` y ) x. ( N ` x ) ) )   &    |- ( ( x e. X /\ y e. X ) -> ( N ` ( x G y ) ) <_ ( ( N ` x ) + ( N ` y ) ) )   &    |- U = <. <. G , S >. , N >.   =>    |- U e. NrmCVec
Theorem	nvi 25485*	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.)
|- X = ( BaseSet ` U )   &    |- G = ( +v ` U )   &    |- S = ( .sOLD ` U )   &    |- Z = ( 0vec ` U )   &    |- N = ( normCV ` U )   =>    |- ( U e. NrmCVec -> ( <. G , S >. e. CVecOLD /\ N : X --> RR /\ A. x e. X ( ( ( N ` x ) = 0 -> x = Z ) /\ A. y e. CC ( N ` ( y S x ) ) = ( ( abs ` y ) x. ( N ` x ) ) /\ A. y e. X ( N ` ( x G y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) )
Theorem	nvvc 25486	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.)
|- W = ( 1st ` U )   =>    |- ( U e. NrmCVec -> W e. CVecOLD )
Theorem	nvablo 25487	The vector addition operation of a normed complex vector space is an Abelian group. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.)
|- G = ( +v ` U )   =>    |- ( U e. NrmCVec -> G e. AbelOp )
Theorem	nvgrp 25488	The vector addition operation of a normed complex vector space is a group. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.)
|- G = ( +v ` U )   =>    |- ( U e. NrmCVec -> G e. GrpOp )
Theorem	nvgf 25489	Mapping for the vector addition operation. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- G = ( +v ` U )   =>    |- ( U e. NrmCVec -> G : ( X X. X ) --> X )
Theorem	nvsf 25490	Mapping for the scalar multiplication operation. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- S = ( .sOLD ` U )   =>    |- ( U e. NrmCVec -> S : ( CC X. X ) --> X )
Theorem	nvgcl 25491	Closure law for the vector addition (group) operation of a normed complex vector space. (Contributed by NM, 23-Apr-2007.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- G = ( +v ` U )   =>    |- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A G B ) e. X )
Theorem	nvcom 25492	The vector addition (group) operation is commutative. (Contributed by NM, 4-Dec-2007.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- G = ( +v ` U )   =>    |- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A G B ) = ( B G A ) )
Theorem	nvass 25493	The vector addition (group) operation is associative. (Contributed by NM, 4-Dec-2007.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- G = ( +v ` U )   =>    |- ( ( U e. NrmCVec /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A G B ) G C ) = ( A G ( B G C ) ) )
Theorem	nvadd12 25494	Commutative/associative law for vector addition. (Contributed by NM, 14-Dec-2007.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- G = ( +v ` U )   =>    |- ( ( U e. NrmCVec /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A G ( B G C ) ) = ( B G ( A G C ) ) )
Theorem	nvadd32 25495	Commutative/associative law for vector addition. (Contributed by NM, 27-Dec-2007.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- G = ( +v ` U )   =>    |- ( ( U e. NrmCVec /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A G B ) G C ) = ( ( A G C ) G B ) )
Theorem	nvrcan 25496	Right cancellation law for vector addition. (Contributed by NM, 4-Dec-2007.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- G = ( +v ` U )   =>    |- ( ( U e. NrmCVec /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A G C ) = ( B G C ) <-> A = B ) )
Theorem	nvlcan 25497	Left cancellation law for vector addition. (Contributed by NM, 14-Dec-2007.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- G = ( +v ` U )   =>    |- ( ( U e. NrmCVec /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( C G A ) = ( C G B ) <-> A = B ) )
Theorem	nvadd4 25498	Rearrangement of 4 terms in a vector sum. (Contributed by NM, 8-Feb-2008.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- G = ( +v ` U )   =>    |- ( ( U e. NrmCVec /\ ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) -> ( ( A G B ) G ( C G D ) ) = ( ( A G C ) G ( B G D ) ) )
Theorem	nvscl 25499	Closure law for the scalar product operation of a normed complex vector space. (Contributed by NM, 1-Feb-2007.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- S = ( .sOLD ` U )   =>    |- ( ( U e. NrmCVec /\ A e. CC /\ B e. X ) -> ( A S B ) e. X )
Theorem	nvsid 25500	Identity element for the scalar product of a normed complex vector space. (Contributed by NM, 4-Dec-2007.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- S = ( .sOLD ` U )   =>    |- ( ( U e. NrmCVec /\ A e. X ) -> ( 1 S A ) = A )