P. 287 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 28601-28700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	hodval 28601	Value of the difference of two Hilbert space operators. (Contributed by NM, 10-Nov-2000.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
|- ( ( S : ~H --> ~H /\ T : ~H --> ~H /\ A e. ~H ) -> ( ( S -op T ) ` A ) = ( ( S ` A ) -h ( T ` A ) ) )
Theorem	hfsval 28602	Value of the sum of two Hilbert space functionals. (Contributed by NM, 23-May-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
|- ( ( S : ~H --> CC /\ T : ~H --> CC /\ A e. ~H ) -> ( ( S +fn T ) ` A ) = ( ( S ` A ) + ( T ` A ) ) )
Theorem	hfmval 28603	Value of the scalar product with a Hilbert space functional. (Contributed by NM, 23-May-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
|- ( ( A e. CC /\ T : ~H --> CC /\ B e. ~H ) -> ( ( A .fn T ) ` B ) = ( A x. ( T ` B ) ) )
Theorem	hoscl 28604	Closure of the sum of two Hilbert space operators. (Contributed by NM, 12-Nov-2000.) (New usage is discouraged.)
|- ( ( ( S : ~H --> ~H /\ T : ~H --> ~H ) /\ A e. ~H ) -> ( ( S +op T ) ` A ) e. ~H )
Theorem	homcl 28605	Closure of the scalar product of a Hilbert space operator. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.)
|- ( ( A e. CC /\ T : ~H --> ~H /\ B e. ~H ) -> ( ( A .op T ) ` B ) e. ~H )
Theorem	hodcl 28606	Closure of the difference of two Hilbert space operators. (Contributed by NM, 15-Nov-2002.) (New usage is discouraged.)
|- ( ( ( S : ~H --> ~H /\ T : ~H --> ~H ) /\ A e. ~H ) -> ( ( S -op T ) ` A ) e. ~H )
19.6.2  Zero and identity operators
Definition	df-h0op 28607	Define the Hilbert space zero operator. See df0op2 28611 for alternate definition. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.)
|- 0hop = ( proj h ` 0H )
Definition	df-iop 28608	Define the Hilbert space identity operator. See dfiop2 28612 for alternate definition. (Contributed by NM, 15-Nov-2000.) (New usage is discouraged.)
|- Iop = ( proj h ` ~H )
Theorem	ho0val 28609	Value of the zero Hilbert space operator (null projector). Remark in [Beran] p. 111. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.)
|- ( A e. ~H -> ( 0hop ` A ) = 0h )
Theorem	ho0f 28610	Functionality of the zero Hilbert space operator. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.)
|- 0hop : ~H --> ~H
Theorem	df0op2 28611	Alternate definition of Hilbert space zero operator. (Contributed by NM, 7-Aug-2006.) (New usage is discouraged.)
|- 0hop = ( ~H X. 0H )
Theorem	dfiop2 28612	Alternate definition of Hilbert space identity operator. (Contributed by NM, 7-Aug-2006.) (New usage is discouraged.)
|- Iop = ( _I |` ~H )
Theorem	hoif 28613	Functionality of the Hilbert space identity operator. (Contributed by NM, 8-Aug-2006.) (New usage is discouraged.)
|- Iop : ~H -1-1-onto-> ~H
Theorem	hoival 28614	The value of the Hilbert space identity operator. (Contributed by NM, 8-Aug-2006.) (New usage is discouraged.)
|- ( A e. ~H -> ( Iop ` A ) = A )
Theorem	hoico1 28615	Composition with the Hilbert space identity operator. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.)
|- ( T : ~H --> ~H -> ( T o. Iop ) = T )
Theorem	hoico2 28616	Composition with the Hilbert space identity operator. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.)
|- ( T : ~H --> ~H -> ( Iop o. T ) = T )
19.6.3  Operations on Hilbert space operators
Theorem	hoaddcl 28617	The sum of Hilbert space operators is an operator. (Contributed by NM, 21-Feb-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
|- ( ( S : ~H --> ~H /\ T : ~H --> ~H ) -> ( S +op T ) : ~H --> ~H )
Theorem	homulcl 28618	The scalar product of a Hilbert space operator is an operator. (Contributed by NM, 21-Feb-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
|- ( ( A e. CC /\ T : ~H --> ~H ) -> ( A .op T ) : ~H --> ~H )
Theorem	hoeq 28619*	Equality of Hilbert space operators. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.)
|- ( ( T : ~H --> ~H /\ U : ~H --> ~H ) -> ( A. x e. ~H ( T ` x ) = ( U ` x ) <-> T = U ) )
Theorem	hoeqi 28620*	Equality of Hilbert space operators. (Contributed by NM, 14-Nov-2000.) (New usage is discouraged.)
|- S : ~H --> ~H   &    |- T : ~H --> ~H   =>    |- ( A. x e. ~H ( S ` x ) = ( T ` x ) <-> S = T )
Theorem	hoscli 28621	Closure of Hilbert space operator sum. (Contributed by NM, 12-Nov-2000.) (New usage is discouraged.)
|- S : ~H --> ~H   &    |- T : ~H --> ~H   =>    |- ( A e. ~H -> ( ( S +op T ) ` A ) e. ~H )
Theorem	hodcli 28622	Closure of Hilbert space operator difference. (Contributed by NM, 12-Nov-2000.) (New usage is discouraged.)
|- S : ~H --> ~H   &    |- T : ~H --> ~H   =>    |- ( A e. ~H -> ( ( S -op T ) ` A ) e. ~H )
Theorem	hocoi 28623	Composition of Hilbert space operators. (Contributed by NM, 12-Nov-2000.) (New usage is discouraged.)
|- S : ~H --> ~H   &    |- T : ~H --> ~H   =>    |- ( A e. ~H -> ( ( S o. T ) ` A ) = ( S ` ( T ` A ) ) )
Theorem	hococli 28624	Closure of composition of Hilbert space operators. (Contributed by NM, 12-Nov-2000.) (New usage is discouraged.)
|- S : ~H --> ~H   &    |- T : ~H --> ~H   =>    |- ( A e. ~H -> ( ( S o. T ) ` A ) e. ~H )
Theorem	hocofi 28625	Mapping of composition of Hilbert space operators. (Contributed by NM, 14-Nov-2000.) (New usage is discouraged.)
|- S : ~H --> ~H   &    |- T : ~H --> ~H   =>    |- ( S o. T ) : ~H --> ~H
Theorem	hocofni 28626	Functionality of composition of Hilbert space operators. (Contributed by NM, 12-Nov-2000.) (New usage is discouraged.)
|- S : ~H --> ~H   &    |- T : ~H --> ~H   =>    |- ( S o. T ) Fn ~H
Theorem	hoaddcli 28627	Mapping of sum of Hilbert space operators. (Contributed by NM, 14-Nov-2000.) (New usage is discouraged.)
|- S : ~H --> ~H   &    |- T : ~H --> ~H   =>    |- ( S +op T ) : ~H --> ~H
Theorem	hosubcli 28628	Mapping of difference of Hilbert space operators. (Contributed by NM, 14-Nov-2000.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
|- S : ~H --> ~H   &    |- T : ~H --> ~H   =>    |- ( S -op T ) : ~H --> ~H
Theorem	hoaddfni 28629	Functionality of sum of Hilbert space operators. (Contributed by NM, 14-Nov-2000.) (New usage is discouraged.)
|- S : ~H --> ~H   &    |- T : ~H --> ~H   =>    |- ( S +op T ) Fn ~H
Theorem	hosubfni 28630	Functionality of difference of Hilbert space operators. (Contributed by NM, 2-Jun-2006.) (New usage is discouraged.)
|- S : ~H --> ~H   &    |- T : ~H --> ~H   =>    |- ( S -op T ) Fn ~H
Theorem	hoaddcomi 28631	Commutativity of sum of Hilbert space operators. (Contributed by NM, 15-Nov-2000.) (New usage is discouraged.)
|- S : ~H --> ~H   &    |- T : ~H --> ~H   =>    |- ( S +op T ) = ( T +op S )
Theorem	hosubcl 28632	Mapping of difference of Hilbert space operators. (Contributed by NM, 23-Aug-2006.) (New usage is discouraged.)
|- ( ( S : ~H --> ~H /\ T : ~H --> ~H ) -> ( S -op T ) : ~H --> ~H )
Theorem	hoaddcom 28633	Commutativity of sum of Hilbert space operators. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.)
|- ( ( S : ~H --> ~H /\ T : ~H --> ~H ) -> ( S +op T ) = ( T +op S ) )
Theorem	hodsi 28634	Relationship between Hilbert space operator difference and sum. (Contributed by NM, 17-Nov-2000.) (New usage is discouraged.)
|- R : ~H --> ~H   &    |- S : ~H --> ~H   &    |- T : ~H --> ~H   =>    |- ( ( R -op S ) = T <-> ( S +op T ) = R )
Theorem	hoaddassi 28635	Associativity of sum of Hilbert space operators. (Contributed by NM, 26-Nov-2000.) (New usage is discouraged.)
|- R : ~H --> ~H   &    |- S : ~H --> ~H   &    |- T : ~H --> ~H   =>    |- ( ( R +op S ) +op T ) = ( R +op ( S +op T ) )
Theorem	hoadd12i 28636	Commutative/associative law for Hilbert space operator sum that swaps the first two terms. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.)
|- R : ~H --> ~H   &    |- S : ~H --> ~H   &    |- T : ~H --> ~H   =>    |- ( R +op ( S +op T ) ) = ( S +op ( R +op T ) )
Theorem	hoadd32i 28637	Commutative/associative law for Hilbert space operator sum that swaps the second and third terms. (Contributed by NM, 27-Jul-2006.) (New usage is discouraged.)
|- R : ~H --> ~H   &    |- S : ~H --> ~H   &    |- T : ~H --> ~H   =>    |- ( ( R +op S ) +op T ) = ( ( R +op T ) +op S )
Theorem	hocadddiri 28638	Distributive law for Hilbert space operator sum. (Contributed by NM, 26-Nov-2000.) (New usage is discouraged.)
|- R : ~H --> ~H   &    |- S : ~H --> ~H   &    |- T : ~H --> ~H   =>    |- ( ( R +op S ) o. T ) = ( ( R o. T ) +op ( S o. T ) )
Theorem	hocsubdiri 28639	Distributive law for Hilbert space operator difference. (Contributed by NM, 26-Nov-2000.) (New usage is discouraged.)
|- R : ~H --> ~H   &    |- S : ~H --> ~H   &    |- T : ~H --> ~H   =>    |- ( ( R -op S ) o. T ) = ( ( R o. T ) -op ( S o. T ) )
Theorem	ho2coi 28640	Double composition of Hilbert space operators. (Contributed by NM, 1-Dec-2000.) (New usage is discouraged.)
|- R : ~H --> ~H   &    |- S : ~H --> ~H   &    |- T : ~H --> ~H   =>    |- ( A e. ~H -> ( ( ( R o. S ) o. T ) ` A ) = ( R ` ( S ` ( T ` A ) ) ) )
Theorem	hoaddass 28641	Associativity of sum of Hilbert space operators. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.)
|- ( ( R : ~H --> ~H /\ S : ~H --> ~H /\ T : ~H --> ~H ) -> ( ( R +op S ) +op T ) = ( R +op ( S +op T ) ) )
Theorem	hoadd32 28642	Commutative/associative law for Hilbert space operator sum that swaps the second and third terms. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.)
|- ( ( R : ~H --> ~H /\ S : ~H --> ~H /\ T : ~H --> ~H ) -> ( ( R +op S ) +op T ) = ( ( R +op T ) +op S ) )
Theorem	hoadd4 28643	Rearrangement of 4 terms in a sum of Hilbert space operators. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.)
|- ( ( ( R : ~H --> ~H /\ S : ~H --> ~H ) /\ ( T : ~H --> ~H /\ U : ~H --> ~H ) ) -> ( ( R +op S ) +op ( T +op U ) ) = ( ( R +op T ) +op ( S +op U ) ) )
Theorem	hocsubdir 28644	Distributive law for Hilbert space operator difference. (Contributed by NM, 23-Aug-2006.) (New usage is discouraged.)
|- ( ( R : ~H --> ~H /\ S : ~H --> ~H /\ T : ~H --> ~H ) -> ( ( R -op S ) o. T ) = ( ( R o. T ) -op ( S o. T ) ) )
Theorem	hoaddid1i 28645	Sum of a Hilbert space operator with the zero operator. (Contributed by NM, 15-Nov-2000.) (New usage is discouraged.)
|- T : ~H --> ~H   =>    |- ( T +op 0hop ) = T
Theorem	hodidi 28646	Difference of a Hilbert space operator from itself. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.)
|- T : ~H --> ~H   =>    |- ( T -op T ) = 0hop
Theorem	ho0coi 28647	Composition of the zero operator and a Hilbert space operator. (Contributed by NM, 9-Aug-2006.) (New usage is discouraged.)
|- T : ~H --> ~H   =>    |- ( 0hop o. T ) = 0hop
Theorem	hoid1i 28648	Composition of Hilbert space operator with unit identity. (Contributed by NM, 15-Nov-2000.) (New usage is discouraged.)
|- T : ~H --> ~H   =>    |- ( T o. Iop ) = T
Theorem	hoid1ri 28649	Composition of Hilbert space operator with unit identity. (Contributed by NM, 15-Nov-2000.) (New usage is discouraged.)
|- T : ~H --> ~H   =>    |- ( Iop o. T ) = T
Theorem	hoaddid1 28650	Sum of a Hilbert space operator with the zero operator. (Contributed by NM, 25-Jul-2006.) (New usage is discouraged.)
|- ( T : ~H --> ~H -> ( T +op 0hop ) = T )
Theorem	hodid 28651	Difference of a Hilbert space operator from itself. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.)
|- ( T : ~H --> ~H -> ( T -op T ) = 0hop )
Theorem	hon0 28652	A Hilbert space operator is not empty. (Contributed by NM, 24-Mar-2006.) (New usage is discouraged.)
|- ( T : ~H --> ~H -> -. T = (/) )
Theorem	hodseqi 28653	Subtraction and addition of equal Hilbert space operators. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.)
|- S : ~H --> ~H   &    |- T : ~H --> ~H   =>    |- ( S +op ( T -op S ) ) = T
Theorem	ho0subi 28654	Subtraction of Hilbert space operators expressed in terms of difference from zero. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.)
|- S : ~H --> ~H   &    |- T : ~H --> ~H   =>    |- ( S -op T ) = ( S +op ( 0hop -op T ) )
Theorem	honegsubi 28655	Relationship between Hilbert operator addition and subtraction. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.)
|- S : ~H --> ~H   &    |- T : ~H --> ~H   =>    |- ( S +op ( -u 1 .op T ) ) = ( S -op T )
Theorem	ho0sub 28656	Subtraction of Hilbert space operators expressed in terms of difference from zero. (Contributed by NM, 25-Jul-2006.) (New usage is discouraged.)
|- ( ( S : ~H --> ~H /\ T : ~H --> ~H ) -> ( S -op T ) = ( S +op ( 0hop -op T ) ) )
Theorem	hosubid1 28657	The zero operator subtracted from a Hilbert space operator. (Contributed by NM, 25-Jul-2006.) (New usage is discouraged.)
|- ( T : ~H --> ~H -> ( T -op 0hop ) = T )
Theorem	honegsub 28658	Relationship between Hilbert space operator addition and subtraction. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.)
|- ( ( T : ~H --> ~H /\ U : ~H --> ~H ) -> ( T +op ( -u 1 .op U ) ) = ( T -op U ) )
Theorem	homulid2 28659	An operator equals its scalar product with one. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.)
|- ( T : ~H --> ~H -> ( 1 .op T ) = T )
Theorem	homco1 28660	Associative law for scalar product and composition of operators. (Contributed by NM, 13-Aug-2006.) (New usage is discouraged.)
|- ( ( A e. CC /\ T : ~H --> ~H /\ U : ~H --> ~H ) -> ( ( A .op T ) o. U ) = ( A .op ( T o. U ) ) )
Theorem	homulass 28661	Scalar product associative law for Hilbert space operators. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.)
|- ( ( A e. CC /\ B e. CC /\ T : ~H --> ~H ) -> ( ( A x. B ) .op T ) = ( A .op ( B .op T ) ) )
Theorem	hoadddi 28662	Scalar product distributive law for Hilbert space operators. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.)
|- ( ( A e. CC /\ T : ~H --> ~H /\ U : ~H --> ~H ) -> ( A .op ( T +op U ) ) = ( ( A .op T ) +op ( A .op U ) ) )
Theorem	hoadddir 28663	Scalar product reverse distributive law for Hilbert space operators. (Contributed by NM, 25-Aug-2006.) (New usage is discouraged.)
|- ( ( A e. CC /\ B e. CC /\ T : ~H --> ~H ) -> ( ( A + B ) .op T ) = ( ( A .op T ) +op ( B .op T ) ) )
Theorem	homul12 28664	Swap first and second factors in a nested operator scalar product. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.)
|- ( ( A e. CC /\ B e. CC /\ T : ~H --> ~H ) -> ( A .op ( B .op T ) ) = ( B .op ( A .op T ) ) )
Theorem	honegneg 28665	Double negative of a Hilbert space operator. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.)
|- ( T : ~H --> ~H -> ( -u 1 .op ( -u 1 .op T ) ) = T )
Theorem	hosubneg 28666	Relationship between operator subtraction and negative. (Contributed by NM, 25-Aug-2006.) (New usage is discouraged.)
|- ( ( T : ~H --> ~H /\ U : ~H --> ~H ) -> ( T -op ( -u 1 .op U ) ) = ( T +op U ) )
Theorem	hosubdi 28667	Scalar product distributive law for operator difference. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.)
|- ( ( A e. CC /\ T : ~H --> ~H /\ U : ~H --> ~H ) -> ( A .op ( T -op U ) ) = ( ( A .op T ) -op ( A .op U ) ) )
Theorem	honegdi 28668	Distribution of negative over addition. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.)
|- ( ( T : ~H --> ~H /\ U : ~H --> ~H ) -> ( -u 1 .op ( T +op U ) ) = ( ( -u 1 .op T ) +op ( -u 1 .op U ) ) )
Theorem	honegsubdi 28669	Distribution of negative over subtraction. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.)
|- ( ( T : ~H --> ~H /\ U : ~H --> ~H ) -> ( -u 1 .op ( T -op U ) ) = ( ( -u 1 .op T ) +op U ) )
Theorem	honegsubdi2 28670	Distribution of negative over subtraction. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.)
|- ( ( T : ~H --> ~H /\ U : ~H --> ~H ) -> ( -u 1 .op ( T -op U ) ) = ( U -op T ) )
Theorem	hosubsub2 28671	Law for double subtraction of Hilbert space operators. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.)
|- ( ( S : ~H --> ~H /\ T : ~H --> ~H /\ U : ~H --> ~H ) -> ( S -op ( T -op U ) ) = ( S +op ( U -op T ) ) )
Theorem	hosub4 28672	Rearrangement of 4 terms in a mixed addition and subtraction of Hilbert space operators. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.)
|- ( ( ( R : ~H --> ~H /\ S : ~H --> ~H ) /\ ( T : ~H --> ~H /\ U : ~H --> ~H ) ) -> ( ( R +op S ) -op ( T +op U ) ) = ( ( R -op T ) +op ( S -op U ) ) )
Theorem	hosubadd4 28673	Rearrangement of 4 terms in a mixed addition and subtraction of Hilbert space operators. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.)
|- ( ( ( R : ~H --> ~H /\ S : ~H --> ~H ) /\ ( T : ~H --> ~H /\ U : ~H --> ~H ) ) -> ( ( R -op S ) -op ( T -op U ) ) = ( ( R +op U ) -op ( S +op T ) ) )
Theorem	hoaddsubass 28674	Associative-type law for addition and subtraction of Hilbert space operators. (Contributed by NM, 25-Aug-2006.) (New usage is discouraged.)
|- ( ( S : ~H --> ~H /\ T : ~H --> ~H /\ U : ~H --> ~H ) -> ( ( S +op T ) -op U ) = ( S +op ( T -op U ) ) )
Theorem	hoaddsub 28675	Law for operator addition and subtraction of Hilbert space operators. (Contributed by NM, 25-Aug-2006.) (New usage is discouraged.)
|- ( ( S : ~H --> ~H /\ T : ~H --> ~H /\ U : ~H --> ~H ) -> ( ( S +op T ) -op U ) = ( ( S -op U ) +op T ) )
Theorem	hosubsub 28676	Law for double subtraction of Hilbert space operators. (Contributed by NM, 25-Aug-2006.) (New usage is discouraged.)
|- ( ( S : ~H --> ~H /\ T : ~H --> ~H /\ U : ~H --> ~H ) -> ( S -op ( T -op U ) ) = ( ( S -op T ) +op U ) )
Theorem	hosubsub4 28677	Law for double subtraction of Hilbert space operators. (Contributed by NM, 25-Aug-2006.) (New usage is discouraged.)
|- ( ( S : ~H --> ~H /\ T : ~H --> ~H /\ U : ~H --> ~H ) -> ( ( S -op T ) -op U ) = ( S -op ( T +op U ) ) )
Theorem	ho2times 28678	Two times a Hilbert space operator. (Contributed by NM, 26-Aug-2006.) (New usage is discouraged.)
|- ( T : ~H --> ~H -> ( 2 .op T ) = ( T +op T ) )
Theorem	hoaddsubassi 28679	Associativity of sum and difference of Hilbert space operators. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.)
|- R : ~H --> ~H   &    |- S : ~H --> ~H   &    |- T : ~H --> ~H   =>    |- ( ( R +op S ) -op T ) = ( R +op ( S -op T ) )
Theorem	hoaddsubi 28680	Law for sum and difference of Hilbert space operators. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.)
|- R : ~H --> ~H   &    |- S : ~H --> ~H   &    |- T : ~H --> ~H   =>    |- ( ( R +op S ) -op T ) = ( ( R -op T ) +op S )
Theorem	hosd1i 28681	Hilbert space operator sum expressed in terms of difference. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.)
|- T : ~H --> ~H   &    |- U : ~H --> ~H   =>    |- ( T +op U ) = ( T -op ( 0hop -op U ) )
Theorem	hosd2i 28682	Hilbert space operator sum expressed in terms of difference. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.)
|- T : ~H --> ~H   &    |- U : ~H --> ~H   =>    |- ( T +op U ) = ( T -op ( ( U -op U ) -op U ) )
Theorem	hopncani 28683	Hilbert space operator cancellation law. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.)
|- T : ~H --> ~H   &    |- U : ~H --> ~H   =>    |- ( ( T +op U ) -op U ) = T
Theorem	honpcani 28684	Hilbert space operator cancellation law. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.)
|- T : ~H --> ~H   &    |- U : ~H --> ~H   =>    |- ( ( T -op U ) +op U ) = T
Theorem	hosubeq0i 28685	If the difference between two operators is zero, they are equal. (Contributed by NM, 27-Jul-2006.) (New usage is discouraged.)
|- T : ~H --> ~H   &    |- U : ~H --> ~H   =>    |- ( ( T -op U ) = 0hop <-> T = U )
Theorem	honpncani 28686	Hilbert space operator cancellation law. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.)
|- R : ~H --> ~H   &    |- S : ~H --> ~H   &    |- T : ~H --> ~H   =>    |- ( ( R -op S ) +op ( S -op T ) ) = ( R -op T )
Theorem	ho01i 28687*	A condition implying that a Hilbert space operator is identically zero. Lemma 3.2(S8) of [Beran] p. 95. (Contributed by NM, 28-Jan-2006.) (New usage is discouraged.)
|- T : ~H --> ~H   =>    |- ( A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = 0 <-> T = 0hop )
Theorem	ho02i 28688*	A condition implying that a Hilbert space operator is identically zero. Lemma 3.2(S10) of [Beran] p. 95. (Contributed by NM, 28-Jan-2006.) (New usage is discouraged.)
|- T : ~H --> ~H   =>    |- ( A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = 0 <-> T = 0hop )
Theorem	hoeq1 28689*	A condition implying that two Hilbert space operators are equal. Lemma 3.2(S9) of [Beran] p. 95. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.)
|- ( ( S : ~H --> ~H /\ T : ~H --> ~H ) -> ( A. x e. ~H A. y e. ~H ( ( S ` x ) .ih y ) = ( ( T ` x ) .ih y ) <-> S = T ) )
Theorem	hoeq2 28690*	A condition implying that two Hilbert space operators are equal. Lemma 3.2(S11) of [Beran] p. 95. (Contributed by NM, 15-Feb-2006.) (New usage is discouraged.)
|- ( ( S : ~H --> ~H /\ T : ~H --> ~H ) -> ( A. x e. ~H A. y e. ~H ( x .ih ( S ` y ) ) = ( x .ih ( T ` y ) ) <-> S = T ) )
Theorem	adjmo 28691*	Every Hilbert space operator has at most one adjoint. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.)
|- E* u ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) )
Theorem	adjsym 28692*	Symmetry property of an adjoint. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.)
|- ( ( S : ~H --> ~H /\ T : ~H --> ~H ) -> ( A. x e. ~H A. y e. ~H ( x .ih ( S ` y ) ) = ( ( T ` x ) .ih y ) <-> A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( S ` x ) .ih y ) ) )
Theorem	eigrei 28693	A necessary and sufficient condition (that holds when T is a Hermitian operator) for an eigenvalue B to be real. Generalization of Equation 1.30 of [Hughes] p. 49. (Contributed by NM, 21-Jan-2005.) (New usage is discouraged.)
|- A e. ~H   &    |- B e. CC   =>    |- ( ( ( T ` A ) = ( B .h A ) /\ A =/= 0h ) -> ( ( A .ih ( T ` A ) ) = ( ( T ` A ) .ih A ) <-> B e. RR ) )
Theorem	eigre 28694	A necessary and sufficient condition (that holds when T is a Hermitian operator) for an eigenvalue B to be real. Generalization of Equation 1.30 of [Hughes] p. 49. (Contributed by NM, 19-Mar-2006.) (New usage is discouraged.)
|- ( ( ( A e. ~H /\ B e. CC ) /\ ( ( T ` A ) = ( B .h A ) /\ A =/= 0h ) ) -> ( ( A .ih ( T ` A ) ) = ( ( T ` A ) .ih A ) <-> B e. RR ) )
Theorem	eigposi 28695	A sufficient condition (first conjunct pair, that holds when T is a positive operator) for an eigenvalue B (second conjunct pair) to be nonnegative. Remark (ii) in [Hughes] p. 137. (Contributed by NM, 2-Jul-2005.) (New usage is discouraged.)
|- A e. ~H   &    |- B e. CC   =>    |- ( ( ( ( A .ih ( T ` A ) ) e. RR /\ 0 <_ ( A .ih ( T ` A ) ) ) /\ ( ( T ` A ) = ( B .h A ) /\ A =/= 0h ) ) -> ( B e. RR /\ 0 <_ B ) )
Theorem	eigorthi 28696	A necessary and sufficient condition (that holds when T is a Hermitian operator) for two eigenvectors A and B to be orthogonal. Generalization of Equation 1.31 of [Hughes] p. 49. (Contributed by NM, 23-Jan-2005.) (New usage is discouraged.)
|- A e. ~H   &    |- B e. ~H   &    |- C e. CC   &    |- D e. CC   =>    |- ( ( ( ( T ` A ) = ( C .h A ) /\ ( T ` B ) = ( D .h B ) ) /\ C =/= ( * ` D ) ) -> ( ( A .ih ( T ` B ) ) = ( ( T ` A ) .ih B ) <-> ( A .ih B ) = 0 ) )
Theorem	eigorth 28697	A necessary and sufficient condition (that holds when T is a Hermitian operator) for two eigenvectors A and B to be orthogonal. Generalization of Equation 1.31 of [Hughes] p. 49. (Contributed by NM, 23-Mar-2006.) (New usage is discouraged.)
|- ( ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. CC /\ D e. CC ) ) /\ ( ( ( T ` A ) = ( C .h A ) /\ ( T ` B ) = ( D .h B ) ) /\ C =/= ( * ` D ) ) ) -> ( ( A .ih ( T ` B ) ) = ( ( T ` A ) .ih B ) <-> ( A .ih B ) = 0 ) )
19.6.4  Linear, continuous, bounded, Hermitian, unitary operators and norms
Definition	df-nmop 28698*	Define the norm of a Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.)
|- normop = ( t e. ( ~H ^m ~H ) |-> sup ( { x | E. z e. ~H ( ( normh ` z ) <_ 1 /\ x = ( normh ` ( t ` z ) ) ) } , RR* , < ) )
Definition	df-cnop 28699*	Define the set of continuous operators on Hilbert space. For every "epsilon" ( y) there is a "delta" ( z) such that... (Contributed by NM, 28-Jan-2006.) (New usage is discouraged.)
|- ContOp = { t e. ( ~H ^m ~H ) | A. x e. ~H A. y e. RR+ E. z e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < z -> ( normh ` ( ( t ` w ) -h ( t ` x ) ) ) < y ) }
Definition	df-lnop 28700*	Define the set of linear operators on Hilbert space. (See df-hosum 28589 for definition of operator.) (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.)
|- LinOp = { t e. ( ~H ^m ~H ) | A. x e. CC A. y e. ~H A. z e. ~H ( t ` ( ( x .h y ) +h z ) ) = ( ( x .h ( t ` y ) ) +h ( t ` z ) ) }