P. 276 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 27501-27600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nvmcl 27501	Closure law for the vector subtraction operation of a normed complex vector space. (Contributed by NM, 11-Sep-2007.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- M = ( -v ` U )   =>    |- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A M B ) e. X )
Theorem	nvnnncan1 27502	Cancellation law for vector subtraction. (nnncan1 10317 analog.) (Contributed by NM, 7-Mar-2008.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- M = ( -v ` U )   =>    |- ( ( U e. NrmCVec /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A M B ) M ( A M C ) ) = ( C M B ) )
Theorem	nvmdi 27503	Distributive law for scalar product over subtraction. (Contributed by NM, 14-Feb-2008.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- M = ( -v ` U )   &    |- S = ( .sOLD ` U )   =>    |- ( ( U e. NrmCVec /\ ( A e. CC /\ B e. X /\ C e. X ) ) -> ( A S ( B M C ) ) = ( ( A S B ) M ( A S C ) ) )
Theorem	nvnegneg 27504	Double negative of a vector. (Contributed by NM, 4-Dec-2007.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- S = ( .sOLD ` U )   =>    |- ( ( U e. NrmCVec /\ A e. X ) -> ( -u 1 S ( -u 1 S A ) ) = A )
Theorem	nvmul0or 27505	If a scalar product is zero, one of its factors must be zero. (Contributed by NM, 6-Dec-2007.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- S = ( .sOLD ` U )   &    |- Z = ( 0vec ` U )   =>    |- ( ( U e. NrmCVec /\ A e. CC /\ B e. X ) -> ( ( A S B ) = Z <-> ( A = 0 \/ B = Z ) ) )
Theorem	nvrinv 27506	A vector minus itself. (Contributed by NM, 4-Dec-2007.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- G = ( +v ` U )   &    |- S = ( .sOLD ` U )   &    |- Z = ( 0vec ` U )   =>    |- ( ( U e. NrmCVec /\ A e. X ) -> ( A G ( -u 1 S A ) ) = Z )
Theorem	nvlinv 27507	Minus a vector plus itself. (Contributed by NM, 4-Dec-2007.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- G = ( +v ` U )   &    |- S = ( .sOLD ` U )   &    |- Z = ( 0vec ` U )   =>    |- ( ( U e. NrmCVec /\ A e. X ) -> ( ( -u 1 S A ) G A ) = Z )
Theorem	nvpncan2 27508	Cancellation law for vector subtraction. (Contributed by NM, 27-Dec-2007.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- G = ( +v ` U )   &    |- M = ( -v ` U )   =>    |- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( A G B ) M A ) = B )
Theorem	nvpncan 27509	Cancellation law for vector subtraction. (Contributed by NM, 24-Jan-2008.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- G = ( +v ` U )   &    |- M = ( -v ` U )   =>    |- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( A G B ) M B ) = A )
Theorem	nvaddsub 27510	Commutative/associative law for vector addition and subtraction. (Contributed by NM, 24-Jan-2008.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- G = ( +v ` U )   &    |- M = ( -v ` U )   =>    |- ( ( U e. NrmCVec /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A G B ) M C ) = ( ( A M C ) G B ) )
Theorem	nvnpcan 27511	Cancellation law for a normed complex vector space. (Contributed by NM, 24-Jan-2008.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- G = ( +v ` U )   &    |- M = ( -v ` U )   =>    |- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( A M B ) G B ) = A )
Theorem	nvaddsub4 27512	Rearrangement of 4 terms in a mixed vector addition and subtraction. (Contributed by NM, 8-Feb-2008.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- G = ( +v ` U )   &    |- M = ( -v ` U )   =>    |- ( ( U e. NrmCVec /\ ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) -> ( ( A G B ) M ( C G D ) ) = ( ( A M C ) G ( B M D ) ) )
Theorem	nvmeq0 27513	The difference between two vectors is zero iff they are equal. (Contributed by NM, 24-Jan-2008.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- M = ( -v ` U )   &    |- Z = ( 0vec ` U )   =>    |- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( A M B ) = Z <-> A = B ) )
Theorem	nvmid 27514	A vector minus itself is the zero vector. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- M = ( -v ` U )   &    |- Z = ( 0vec ` U )   =>    |- ( ( U e. NrmCVec /\ A e. X ) -> ( A M A ) = Z )
Theorem	nvf 27515	Mapping for the norm function. (Contributed by NM, 11-Nov-2006.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- N = ( normCV ` U )   =>    |- ( U e. NrmCVec -> N : X --> RR )
Theorem	nvcl 27516	The norm of a normed complex vector space is a real number. (Contributed by NM, 24-Nov-2006.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- N = ( normCV ` U )   =>    |- ( ( U e. NrmCVec /\ A e. X ) -> ( N ` A ) e. RR )
Theorem	nvcli 27517	The norm of a normed complex vector space is a real number. (Contributed by NM, 20-Apr-2007.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- N = ( normCV ` U )   &    |- U e. NrmCVec   &    |- A e. X   =>    |- ( N ` A ) e. RR
Theorem	nvs 27518	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.)
|- X = ( BaseSet ` U )   &    |- S = ( .sOLD ` U )   &    |- N = ( normCV ` U )   =>    |- ( ( U e. NrmCVec /\ A e. CC /\ B e. X ) -> ( N ` ( A S B ) ) = ( ( abs ` A ) x. ( N ` B ) ) )
Theorem	nvsge0 27519	The norm of a scalar product with a nonnegative real. (Contributed by NM, 1-Jan-2008.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- S = ( .sOLD ` U )   &    |- N = ( normCV ` U )   =>    |- ( ( U e. NrmCVec /\ ( A e. RR /\ 0 <_ A ) /\ B e. X ) -> ( N ` ( A S B ) ) = ( A x. ( N ` B ) ) )
Theorem	nvm1 27520	The norm of the negative of a vector. (Contributed by NM, 28-Nov-2006.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- S = ( .sOLD ` U )   &    |- N = ( normCV ` U )   =>    |- ( ( U e. NrmCVec /\ A e. X ) -> ( N ` ( -u 1 S A ) ) = ( N ` A ) )
Theorem	nvdif 27521	The norm of the difference between two vectors. (Contributed by NM, 1-Dec-2006.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- G = ( +v ` U )   &    |- S = ( .sOLD ` U )   &    |- N = ( normCV ` U )   =>    |- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( N ` ( A G ( -u 1 S B ) ) ) = ( N ` ( B G ( -u 1 S A ) ) ) )
Theorem	nvpi 27522	The norm of a vector plus the imaginary scalar product of another. (Contributed by NM, 2-Feb-2007.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- G = ( +v ` U )   &    |- S = ( .sOLD ` U )   &    |- N = ( normCV ` U )   =>    |- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( N ` ( A G ( _i S B ) ) ) = ( N ` ( B G ( -u _i S A ) ) ) )
Theorem	nvz0 27523	The norm of a zero vector is zero. (Contributed by NM, 24-Nov-2006.) (New usage is discouraged.)
|- Z = ( 0vec ` U )   &    |- N = ( normCV ` U )   =>    |- ( U e. NrmCVec -> ( N ` Z ) = 0 )
Theorem	nvz 27524	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.)
|- X = ( BaseSet ` U )   &    |- Z = ( 0vec ` U )   &    |- N = ( normCV ` U )   =>    |- ( ( U e. NrmCVec /\ A e. X ) -> ( ( N ` A ) = 0 <-> A = Z ) )
Theorem	nvtri 27525	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.)
|- X = ( BaseSet ` U )   &    |- G = ( +v ` U )   &    |- N = ( normCV ` U )   =>    |- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( N ` ( A G B ) ) <_ ( ( N ` A ) + ( N ` B ) ) )
Theorem	nvmtri 27526	Triangle inequality for the norm of a vector difference. (Contributed by NM, 27-Dec-2007.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- M = ( -v ` U )   &    |- N = ( normCV ` U )   =>    |- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( N ` ( A M B ) ) <_ ( ( N ` A ) + ( N ` B ) ) )
Theorem	nvabs 27527	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.)
|- X = ( BaseSet ` U )   &    |- G = ( +v ` U )   &    |- S = ( .sOLD ` U )   &    |- N = ( normCV ` U )   =>    |- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( abs ` ( ( N ` A ) - ( N ` B ) ) ) <_ ( N ` ( A G ( -u 1 S B ) ) ) )
Theorem	nvge0 27528	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.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- N = ( normCV ` U )   =>    |- ( ( U e. NrmCVec /\ A e. X ) -> 0 <_ ( N ` A ) )
Theorem	nvgt0 27529	A nonzero norm is positive. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- Z = ( 0vec ` U )   &    |- N = ( normCV ` U )   =>    |- ( ( U e. NrmCVec /\ A e. X ) -> ( A =/= Z <-> 0 < ( N ` A ) ) )
Theorem	nv1 27530	From any nonzero vector, construct a vector whose norm is one. (Contributed by NM, 6-Dec-2007.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- S = ( .sOLD ` U )   &    |- Z = ( 0vec ` U )   &    |- N = ( normCV ` U )   =>    |- ( ( U e. NrmCVec /\ A e. X /\ A =/= Z ) -> ( N ` ( ( 1 / ( N ` A ) ) S A ) ) = 1 )
Theorem	nvop 27531	A complex inner product space in terms of ordered pair components. (Contributed by NM, 11-Sep-2007.) (New usage is discouraged.)
|- G = ( +v ` U )   &    |- S = ( .sOLD ` U )   &    |- N = ( normCV ` U )   =>    |- ( U e. NrmCVec -> U = <. <. G , S >. , N >. )
18.3.2  Examples of normed complex vector spaces
Theorem	cnnv 27532	The set of complex numbers is a normed complex vector space. The vector operation is +, the scalar product is x., and the norm function is abs. (Contributed by Steve Rodriguez, 3-Dec-2006.) (New usage is discouraged.)
|- U = <. <. + , x. >. , abs >.   =>    |- U e. NrmCVec
Theorem	cnnvg 27533	The vector addition (group) operation of the normed complex vector space of complex numbers. (Contributed by NM, 12-Jan-2008.) (New usage is discouraged.)
|- U = <. <. + , x. >. , abs >.   =>    |- + = ( +v ` U )
Theorem	cnnvba 27534	The base set of the normed complex vector space of complex numbers. (Contributed by NM, 7-Nov-2007.) (New usage is discouraged.)
|- U = <. <. + , x. >. , abs >.   =>    |- CC = ( BaseSet ` U )
Theorem	cnnvs 27535	The scalar product operation of the normed complex vector space of complex numbers. (Contributed by NM, 12-Jan-2008.) (New usage is discouraged.)
|- U = <. <. + , x. >. , abs >.   =>    |- x. = ( .sOLD ` U )
Theorem	cnnvnm 27536	The norm operation of the normed complex vector space of complex numbers. (Contributed by NM, 12-Jan-2008.) (New usage is discouraged.)
|- U = <. <. + , x. >. , abs >.   =>    |- abs = ( normCV ` U )
Theorem	cnnvm 27537	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.)
|- U = <. <. + , x. >. , abs >.   =>    |- - = ( -v ` U )
Theorem	elimnv 27538	Hypothesis elimination lemma for normed complex vector spaces to assist weak deduction theorem. (Contributed by NM, 16-May-2007.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- Z = ( 0vec ` U )   &    |- U e. NrmCVec   =>    |- if ( A e. X , A , Z ) e. X
Theorem	elimnvu 27539	Hypothesis elimination lemma for normed complex vector spaces to assist weak deduction theorem. (Contributed by NM, 16-May-2007.) (New usage is discouraged.)
|- if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) e. NrmCVec
18.3.3  Induced metric of a normed complex vector space
Theorem	imsval 27540	Value of the induced metric of a normed complex vector space. (Contributed by NM, 11-Sep-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
|- M = ( -v ` U )   &    |- N = ( normCV ` U )   &    |- D = ( IndMet ` U )   =>    |- ( U e. NrmCVec -> D = ( N o. M ) )
Theorem	imsdval 27541	Value of the induced metric (distance function) of a normed complex vector space. Equation 1 of [Kreyszig] p. 59. (Contributed by NM, 11-Sep-2007.) (Revised by Mario Carneiro, 27-Dec-2014.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- M = ( -v ` U )   &    |- N = ( normCV ` U )   &    |- D = ( IndMet ` U )   =>    |- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A D B ) = ( N ` ( A M B ) ) )
Theorem	imsdval2 27542	Value of the distance function of the induced metric of a normed complex vector space. Equation 1 of [Kreyszig] p. 59. (Contributed by NM, 28-Nov-2006.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- G = ( +v ` U )   &    |- S = ( .sOLD ` U )   &    |- N = ( normCV ` U )   &    |- D = ( IndMet ` U )   =>    |- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A D B ) = ( N ` ( A G ( -u 1 S B ) ) ) )
Theorem	nvnd 27543	The norm of a normed complex vector space expressed in terms of the distance function of its induced metric. Problem 1 of [Kreyszig] p. 63. (Contributed by NM, 4-Dec-2006.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- Z = ( 0vec ` U )   &    |- N = ( normCV ` U )   &    |- D = ( IndMet ` U )   =>    |- ( ( U e. NrmCVec /\ A e. X ) -> ( N ` A ) = ( A D Z ) )
Theorem	imsdf 27544	Mapping for the induced metric distance function of a normed complex vector space. (Contributed by NM, 29-Nov-2006.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- D = ( IndMet ` U )   =>    |- ( U e. NrmCVec -> D : ( X X. X ) --> RR )
Theorem	imsmetlem 27545	Lemma for imsmet 27546. (Contributed by NM, 29-Nov-2006.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- G = ( +v ` U )   &    |- M = ( inv ` G )   &    |- S = ( .sOLD ` U )   &    |- Z = ( 0vec ` U )   &    |- N = ( normCV ` U )   &    |- D = ( IndMet ` U )   &    |- U e. NrmCVec   =>    |- D e. ( Met ` X )
Theorem	imsmet 27546	The induced metric of a normed complex vector space is a metric space. Part of Definition 2.2-1 of [Kreyszig] p. 58. (Contributed by NM, 4-Dec-2006.) (Revised by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- D = ( IndMet ` U )   =>    |- ( U e. NrmCVec -> D e. ( Met ` X ) )
Theorem	imsxmet 27547	The induced metric of a normed complex vector space is an extended metric space. (Contributed by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- D = ( IndMet ` U )   =>    |- ( U e. NrmCVec -> D e. ( *Met ` X ) )
Theorem	cnims 27548	The metric induced on the complex numbers. cnmet 22575 proves that it is a metric. (Contributed by Steve Rodriguez, 5-Dec-2006.) (Revised by NM, 15-Jan-2008.) (New usage is discouraged.)
|- U = <. <. + , x. >. , abs >.   &    |- D = ( abs o. - )   =>    |- D = ( IndMet ` U )
Theorem	vacn 27549	Vector addition is jointly continuous in both arguments. (Contributed by Jeff Hankins, 16-Jun-2009.) (Revised by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.)
|- C = ( IndMet ` U )   &    |- J = ( MetOpen ` C )   &    |- G = ( +v ` U )   =>    |- ( U e. NrmCVec -> G e. ( ( J tX J ) Cn J ) )
Theorem	nmcvcn 27550	The norm of a normed complex vector space is a continuous function. (Contributed by NM, 16-May-2007.) (Proof shortened by Mario Carneiro, 10-Jan-2014.) (New usage is discouraged.)
|- N = ( normCV ` U )   &    |- C = ( IndMet ` U )   &    |- J = ( MetOpen ` C )   &    |- K = ( topGen ` ran (,) )   =>    |- ( U e. NrmCVec -> N e. ( J Cn K ) )
Theorem	nmcnc 27551	The norm of a normed complex vector space is a continuous function to CC. (For RR, see nmcvcn 27550.) (Contributed by NM, 12-Aug-2007.) (New usage is discouraged.)
|- N = ( normCV ` U )   &    |- C = ( IndMet ` U )   &    |- J = ( MetOpen ` C )   &    |- K = ( TopOpen ` ℂfld )   =>    |- ( U e. NrmCVec -> N e. ( J Cn K ) )
Theorem	smcnlem 27552*	Lemma for smcn 27553. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.)
|- C = ( IndMet ` U )   &    |- J = ( MetOpen ` C )   &    |- S = ( .sOLD ` U )   &    |- K = ( TopOpen ` ℂfld )   &    |- X = ( BaseSet ` U )   &    |- N = ( normCV ` U )   &    |- U e. NrmCVec   &    |- T = ( 1 / ( 1 + ( ( ( ( N ` y ) + ( abs ` x ) ) + 1 ) / r ) ) )   =>    |- S e. ( ( K tX J ) Cn J )
Theorem	smcn 27553	Scalar multiplication is jointly continuous in both arguments. (Contributed by NM, 16-Jun-2009.) (Revised by Mario Carneiro, 5-May-2014.) (New usage is discouraged.)
|- C = ( IndMet ` U )   &    |- J = ( MetOpen ` C )   &    |- S = ( .sOLD ` U )   &    |- K = ( TopOpen ` ℂfld )   =>    |- ( U e. NrmCVec -> S e. ( ( K tX J ) Cn J ) )
Theorem	vmcn 27554	Vector subtraction is jointly continuous in both arguments. (Contributed by Mario Carneiro, 6-May-2014.) (New usage is discouraged.)
|- C = ( IndMet ` U )   &    |- J = ( MetOpen ` C )   &    |- M = ( -v ` U )   =>    |- ( U e. NrmCVec -> M e. ( ( J tX J ) Cn J ) )
18.3.4  Inner product
Syntax	cdip 27555	Extend class notation with the class inner product functions.
class .iOLD
Definition	df-dip 27556*	Define a function that maps a normed complex vector space to its inner product operation in case its norm satisfies the parallelogram identity (otherwise the operation is still defined, but not meaningful). Based on Exercise 4(a) of [ReedSimon] p. 63 and Theorem 6.44 of [Ponnusamy] p. 361. Vector addition is ( 1st ` w ), the scalar product is ( 2nd ` w ), and the norm is n. (Contributed by NM, 10-Apr-2007.) (New usage is discouraged.)
|- .iOLD = ( u e. NrmCVec |-> ( x e. ( BaseSet ` u ) , y e. ( BaseSet ` u ) |-> ( sum_ k e. ( 1 ... 4 ) ( ( _i ^ k ) x. ( ( ( normCV ` u ) ` ( x ( +v ` u ) ( ( _i ^ k ) ( .sOLD ` u ) y ) ) ) ^ 2 ) ) / 4 ) ) )
Theorem	dipfval 27557*	The inner product function on a normed complex vector space. The definition is meaningful for vector spaces that are also inner product spaces, i.e. satisfy the parallelogram law. (Contributed by NM, 10-Apr-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- G = ( +v ` U )   &    |- S = ( .sOLD ` U )   &    |- N = ( normCV ` U )   &    |- P = ( .iOLD ` U )   =>    |- ( U e. NrmCVec -> P = ( x e. X , y e. X |-> ( sum_ k e. ( 1 ... 4 ) ( ( _i ^ k ) x. ( ( N ` ( x G ( ( _i ^ k ) S y ) ) ) ^ 2 ) ) / 4 ) ) )
Theorem	ipval 27558*	Value of the inner product. The definition is meaningful for normed complex vector spaces that are also inner product spaces, i.e. satisfy the parallelogram law, although for convenience we define it for any normed complex vector space. The vector (group) addition operation is G, the scalar product is S, the norm is N, and the set of vectors is X. Equation 6.45 of [Ponnusamy] p. 361. (Contributed by NM, 31-Jan-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- G = ( +v ` U )   &    |- S = ( .sOLD ` U )   &    |- N = ( normCV ` U )   &    |- P = ( .iOLD ` U )   =>    |- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A P B ) = ( sum_ k e. ( 1 ... 4 ) ( ( _i ^ k ) x. ( ( N ` ( A G ( ( _i ^ k ) S B ) ) ) ^ 2 ) ) / 4 ) )
Theorem	ipval2lem2 27559	Lemma for ipval3 27564. (Contributed by NM, 1-Feb-2007.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- G = ( +v ` U )   &    |- S = ( .sOLD ` U )   &    |- N = ( normCV ` U )   &    |- P = ( .iOLD ` U )   =>    |- ( ( ( U e. NrmCVec /\ A e. X /\ B e. X ) /\ C e. CC ) -> ( ( N ` ( A G ( C S B ) ) ) ^ 2 ) e. RR )
Theorem	ipval2lem3 27560	Lemma for ipval3 27564. (Contributed by NM, 1-Feb-2007.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- G = ( +v ` U )   &    |- S = ( .sOLD ` U )   &    |- N = ( normCV ` U )   &    |- P = ( .iOLD ` U )   =>    |- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( N ` ( A G B ) ) ^ 2 ) e. RR )
Theorem	ipval2lem4 27561	Lemma for ipval3 27564. (Contributed by NM, 1-Feb-2007.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- G = ( +v ` U )   &    |- S = ( .sOLD ` U )   &    |- N = ( normCV ` U )   &    |- P = ( .iOLD ` U )   =>    |- ( ( ( U e. NrmCVec /\ A e. X /\ B e. X ) /\ C e. CC ) -> ( ( N ` ( A G ( C S B ) ) ) ^ 2 ) e. CC )
Theorem	ipval2 27562	Expansion of the inner product value ipval 27558. (Contributed by NM, 31-Jan-2007.) (Revised by Mario Carneiro, 5-May-2014.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- G = ( +v ` U )   &    |- S = ( .sOLD ` U )   &    |- N = ( normCV ` U )   &    |- P = ( .iOLD ` U )   =>    |- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A P B ) = ( ( ( ( ( N ` ( A G B ) ) ^ 2 ) - ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) + ( _i x. ( ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) - ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) ) ) / 4 ) )
Theorem	4ipval2 27563	Four times the inner product value ipval3 27564, useful for simplifying certain proofs. (Contributed by NM, 10-Apr-2007.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- G = ( +v ` U )   &    |- S = ( .sOLD ` U )   &    |- N = ( normCV ` U )   &    |- P = ( .iOLD ` U )   =>    |- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( 4 x. ( A P B ) ) = ( ( ( ( N ` ( A G B ) ) ^ 2 ) - ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) + ( _i x. ( ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) - ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) ) ) )
Theorem	ipval3 27564	Expansion of the inner product value ipval 27558. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- G = ( +v ` U )   &    |- S = ( .sOLD ` U )   &    |- N = ( normCV ` U )   &    |- P = ( .iOLD ` U )   &    |- M = ( -v ` U )   =>    |- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A P B ) = ( ( ( ( ( N ` ( A G B ) ) ^ 2 ) - ( ( N ` ( A M B ) ) ^ 2 ) ) + ( _i x. ( ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) - ( ( N ` ( A M ( _i S B ) ) ) ^ 2 ) ) ) ) / 4 ) )
Theorem	ipidsq 27565	The inner product of a vector with itself is the square of the vector's norm. Equation I4 of [Ponnusamy] p. 362. (Contributed by NM, 1-Feb-2007.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- N = ( normCV ` U )   &    |- P = ( .iOLD ` U )   =>    |- ( ( U e. NrmCVec /\ A e. X ) -> ( A P A ) = ( ( N ` A ) ^ 2 ) )
Theorem	ipnm 27566	Norm expressed in terms of inner product. (Contributed by NM, 11-Sep-2007.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- N = ( normCV ` U )   &    |- P = ( .iOLD ` U )   =>    |- ( ( U e. NrmCVec /\ A e. X ) -> ( N ` A ) = ( sqr ` ( A P A ) ) )
Theorem	dipcl 27567	An inner product is a complex number. (Contributed by NM, 1-Feb-2007.) (Revised by Mario Carneiro, 5-May-2014.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- P = ( .iOLD ` U )   =>    |- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A P B ) e. CC )
Theorem	ipf 27568	Mapping for the inner product operation. (Contributed by NM, 28-Jan-2008.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- P = ( .iOLD ` U )   =>    |- ( U e. NrmCVec -> P : ( X X. X ) --> CC )
Theorem	dipcj 27569	The complex conjugate of an inner product reverses its arguments. Equation I1 of [Ponnusamy] p. 362. (Contributed by NM, 1-Feb-2007.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- P = ( .iOLD ` U )   =>    |- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( * ` ( A P B ) ) = ( B P A ) )
Theorem	ipipcj 27570	An inner product times its conjugate. (Contributed by NM, 23-Nov-2007.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- P = ( .iOLD ` U )   =>    |- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( A P B ) x. ( B P A ) ) = ( ( abs ` ( A P B ) ) ^ 2 ) )
Theorem	diporthcom 27571	Orthogonality (meaning inner product is 0) is commutative. (Contributed by NM, 17-Apr-2008.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- P = ( .iOLD ` U )   =>    |- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( A P B ) = 0 <-> ( B P A ) = 0 ) )
Theorem	dip0r 27572	Inner product with a zero second argument. (Contributed by NM, 5-Feb-2007.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- Z = ( 0vec ` U )   &    |- P = ( .iOLD ` U )   =>    |- ( ( U e. NrmCVec /\ A e. X ) -> ( A P Z ) = 0 )
Theorem	dip0l 27573	Inner product with a zero first argument. Part of proof of Theorem 6.44 of [Ponnusamy] p. 361. (Contributed by NM, 5-Feb-2007.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- Z = ( 0vec ` U )   &    |- P = ( .iOLD ` U )   =>    |- ( ( U e. NrmCVec /\ A e. X ) -> ( Z P A ) = 0 )
Theorem	ipz 27574	The inner product of a vector with itself is zero iff the vector is zero. Part of Definition 3.1-1 of [Kreyszig] p. 129. (Contributed by NM, 24-Jan-2008.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- Z = ( 0vec ` U )   &    |- P = ( .iOLD ` U )   =>    |- ( ( U e. NrmCVec /\ A e. X ) -> ( ( A P A ) = 0 <-> A = Z ) )
Theorem	dipcn 27575	Inner product is jointly continuous in both arguments. (Contributed by NM, 21-Aug-2007.) (Revised by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.)
|- P = ( .iOLD ` U )   &    |- C = ( IndMet ` U )   &    |- J = ( MetOpen ` C )   &    |- K = ( TopOpen ` ℂfld )   =>    |- ( U e. NrmCVec -> P e. ( ( J tX J ) Cn K ) )
18.3.5  Subspaces
Syntax	css 27576	Extend class notation with the class of all subspaces of normed complex vector spaces.
class SubSp
Definition	df-ssp 27577*	Define the class of all subspaces of normed complex vector spaces. (Contributed by NM, 26-Jan-2008.) (New usage is discouraged.)
|- SubSp = ( u e. NrmCVec |-> { w e. NrmCVec | ( ( +v ` w ) C_ ( +v ` u ) /\ ( .sOLD ` w ) C_ ( .sOLD ` u ) /\ ( normCV ` w ) C_ ( normCV ` u ) ) } )
Theorem	sspval 27578*	The set of all subspaces of a normed complex vector space. (Contributed by NM, 26-Jan-2008.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
|- G = ( +v ` U )   &    |- S = ( .sOLD ` U )   &    |- N = ( normCV ` U )   &    |- H = ( SubSp ` U )   =>    |- ( U e. NrmCVec -> H = { w e. NrmCVec | ( ( +v ` w ) C_ G /\ ( .sOLD ` w ) C_ S /\ ( normCV ` w ) C_ N ) } )
Theorem	isssp 27579	The predicate "is a subspace." (Contributed by NM, 26-Jan-2008.) (New usage is discouraged.)
|- G = ( +v ` U )   &    |- F = ( +v ` W )   &    |- S = ( .sOLD ` U )   &    |- R = ( .sOLD ` W )   &    |- N = ( normCV ` U )   &    |- M = ( normCV ` W )   &    |- H = ( SubSp ` U )   =>    |- ( U e. NrmCVec -> ( W e. H <-> ( W e. NrmCVec /\ ( F C_ G /\ R C_ S /\ M C_ N ) ) ) )
Theorem	sspid 27580	A normed complex vector space is a subspace of itself. (Contributed by NM, 8-Apr-2008.) (New usage is discouraged.)
|- H = ( SubSp ` U )   =>    |- ( U e. NrmCVec -> U e. H )
Theorem	sspnv 27581	A subspace is a normed complex vector space. (Contributed by NM, 27-Jan-2008.) (New usage is discouraged.)
|- H = ( SubSp ` U )   =>    |- ( ( U e. NrmCVec /\ W e. H ) -> W e. NrmCVec )
Theorem	sspba 27582	The base set of a subspace is included in the parent base set. (Contributed by NM, 27-Jan-2008.) (New usage is discouraged.)
|- X = ( BaseSet ` U )   &    |- Y = ( BaseSet ` W )   &    |- H = ( SubSp ` U )   =>    |- ( ( U e. NrmCVec /\ W e. H ) -> Y C_ X )
Theorem	sspg 27583	Vector addition on a subspace is a restriction of vector addition on the parent space. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.)
|- Y = ( BaseSet ` W )   &    |- G = ( +v ` U )   &    |- F = ( +v ` W )   &    |- H = ( SubSp ` U )   =>    |- ( ( U e. NrmCVec /\ W e. H ) -> F = ( G |` ( Y X. Y ) ) )
Theorem	sspgval 27584	Vector addition on a subspace in terms of vector addition on the parent space. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.)
|- Y = ( BaseSet ` W )   &    |- G = ( +v ` U )   &    |- F = ( +v ` W )   &    |- H = ( SubSp ` U )   =>    |- ( ( ( U e. NrmCVec /\ W e. H ) /\ ( A e. Y /\ B e. Y ) ) -> ( A F B ) = ( A G B ) )
Theorem	ssps 27585	Scalar multiplication on a subspace is a restriction of scalar multiplication on the parent space. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.)
|- Y = ( BaseSet ` W )   &    |- S = ( .sOLD ` U )   &    |- R = ( .sOLD ` W )   &    |- H = ( SubSp ` U )   =>    |- ( ( U e. NrmCVec /\ W e. H ) -> R = ( S |` ( CC X. Y ) ) )
Theorem	sspsval 27586	Scalar multiplication on a subspace in terms of scalar multiplication on the parent space. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.)
|- Y = ( BaseSet ` W )   &    |- S = ( .sOLD ` U )   &    |- R = ( .sOLD ` W )   &    |- H = ( SubSp ` U )   =>    |- ( ( ( U e. NrmCVec /\ W e. H ) /\ ( A e. CC /\ B e. Y ) ) -> ( A R B ) = ( A S B ) )
Theorem	sspmlem 27587*	Lemma for sspm 27589 and others. (Contributed by NM, 1-Feb-2008.) (New usage is discouraged.)
|- Y = ( BaseSet ` W )   &    |- H = ( SubSp ` U )   &    |- ( ( ( U e. NrmCVec /\ W e. H ) /\ ( x e. Y /\ y e. Y ) ) -> ( x F y ) = ( x G y ) )   &    |- ( W e. NrmCVec -> F : ( Y X. Y ) --> R )   &    |- ( U e. NrmCVec -> G : ( ( BaseSet ` U ) X. ( BaseSet ` U ) ) --> S )   =>    |- ( ( U e. NrmCVec /\ W e. H ) -> F = ( G |` ( Y X. Y ) ) )
Theorem	sspmval 27588	Vector addition on a subspace in terms of vector addition on the parent space. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.)
|- Y = ( BaseSet ` W )   &    |- M = ( -v ` U )   &    |- L = ( -v ` W )   &    |- H = ( SubSp ` U )   =>    |- ( ( ( U e. NrmCVec /\ W e. H ) /\ ( A e. Y /\ B e. Y ) ) -> ( A L B ) = ( A M B ) )
Theorem	sspm 27589	Vector subtraction on a subspace is a restriction of vector subtraction on the parent space. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.)
|- Y = ( BaseSet ` W )   &    |- M = ( -v ` U )   &    |- L = ( -v ` W )   &    |- H = ( SubSp ` U )   =>    |- ( ( U e. NrmCVec /\ W e. H ) -> L = ( M |` ( Y X. Y ) ) )
Theorem	sspz 27590	The zero vector of a subspace is the same as the parent's. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.)
|- Z = ( 0vec ` U )   &    |- Q = ( 0vec ` W )   &    |- H = ( SubSp ` U )   =>    |- ( ( U e. NrmCVec /\ W e. H ) -> Q = Z )
Theorem	sspn 27591	The norm on a subspace is a restriction of the norm on the parent space. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.)
|- Y = ( BaseSet ` W )   &    |- N = ( normCV ` U )   &    |- M = ( normCV ` W )   &    |- H = ( SubSp ` U )   =>    |- ( ( U e. NrmCVec /\ W e. H ) -> M = ( N |` Y ) )
Theorem	sspnval 27592	The norm on a subspace in terms of the norm on the parent space. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.)
|- Y = ( BaseSet ` W )   &    |- N = ( normCV ` U )   &    |- M = ( normCV ` W )   &    |- H = ( SubSp ` U )   =>    |- ( ( U e. NrmCVec /\ W e. H /\ A e. Y ) -> ( M ` A ) = ( N ` A ) )
Theorem	sspimsval 27593	The induced metric on a subspace in terms of the induced metric on the parent space. (Contributed by NM, 1-Feb-2008.) (New usage is discouraged.)
|- Y = ( BaseSet ` W )   &    |- D = ( IndMet ` U )   &    |- C = ( IndMet ` W )   &    |- H = ( SubSp ` U )   =>    |- ( ( ( U e. NrmCVec /\ W e. H ) /\ ( A e. Y /\ B e. Y ) ) -> ( A C B ) = ( A D B ) )
Theorem	sspims 27594	The induced metric on a subspace is a restriction of the induced metric on the parent space. (Contributed by NM, 1-Feb-2008.) (New usage is discouraged.)
|- Y = ( BaseSet ` W )   &    |- D = ( IndMet ` U )   &    |- C = ( IndMet ` W )   &    |- H = ( SubSp ` U )   =>    |- ( ( U e. NrmCVec /\ W e. H ) -> C = ( D |` ( Y X. Y ) ) )
18.4  Operators on complex vector spaces
18.4.1  Definitions and basic properties
Syntax	clno 27595	Extend class notation with the class of linear operators on normed complex vector spaces.
class LnOp
Syntax	cnmoo 27596	Extend class notation with the class of operator norms on normed complex vector spaces.
class normOpOLD
Syntax	cblo 27597	Extend class notation with the class of bounded linear operators on normed complex vector spaces.
class BLnOp
Syntax	c0o 27598	Extend class notation with the class of zero operators on normed complex vector spaces.
class 0op
Definition	df-lno 27599*	Define the class of linear operators between two normed complex vector spaces. In the literature, an operator may be a partial function, i.e. the domain of an operator is not necessarily the entire vector space. However, since the domain of a linear operator is a vector subspace, we define it with a complete function for convenience and will use subset relations to specify the partial function case. (Contributed by NM, 6-Nov-2007.) (New usage is discouraged.)
|- LnOp = ( u e. NrmCVec , w e. NrmCVec |-> { t e. ( ( BaseSet ` w ) ^m ( BaseSet ` u ) ) | A. x e. CC A. y e. ( BaseSet ` u ) A. z e. ( BaseSet ` u ) ( t ` ( ( x ( .sOLD ` u ) y ) ( +v ` u ) z ) ) = ( ( x ( .sOLD ` w ) ( t ` y ) ) ( +v ` w ) ( t ` z ) ) } )
Definition	df-nmoo 27600*	Define the norm of an operator between two normed complex vector spaces. This definition produces an operator norm function for each pair of vector spaces <. u , w >.. Based on definition of linear operator norm in [AkhiezerGlazman] p. 39, although we define it for all operators for convenience. It isn't necessarily meaningful for nonlinear operators, since it doesn't take into account operator values at vectors with norm greater than 1. See Equation 2 of [Kreyszig] p. 92 for a definition that does (although it ignores the value at the zero vector). However, operator norms are rarely if ever used for nonlinear operators. (Contributed by NM, 6-Nov-2007.) (New usage is discouraged.)
|- normOpOLD = ( u e. NrmCVec , w e. NrmCVec |-> ( t e. ( ( BaseSet ` w ) ^m ( BaseSet ` u ) ) |-> sup ( { x | E. z e. ( BaseSet ` u ) ( ( ( normCV ` u ) ` z ) <_ 1 /\ x = ( ( normCV ` w ) ` ( t ` z ) ) ) } , RR* , < ) ) )