P. 233 of Theorem List - Metamath Proof Explorer

Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Metamath Proof Explorer - 23201-23300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	hoscl 23201	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 23202	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 23203	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 )
18.6.2  Zero and identity operators
Definition	df-h0op 23204	Define the Hilbert space zero operator. See df0op2 23208 for alternate definition. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.)
|- 0hop = ( proj h ` 0H )
Definition	df-iop 23205	Define the Hilbert space identity operator. See dfiop2 23209 for alternate definition. (Contributed by NM, 15-Nov-2000.) (New usage is discouraged.)
|- Iop = ( proj h ` ~H )
Theorem	ho0val 23206	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 23207	Functionality of the zero Hilbert space operator. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.)
|- 0hop : ~H --> ~H
Theorem	df0op2 23208	Alternate definition of Hilbert space zero operator. (Contributed by NM, 7-Aug-2006.) (New usage is discouraged.)
|- 0hop = ( ~H X. 0H )
Theorem	dfiop2 23209	Alternate definition of Hilbert space identity operator. (Contributed by NM, 7-Aug-2006.) (New usage is discouraged.)
|- Iop = ( _I |` ~H )
Theorem	hoif 23210	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 23211	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 23212	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 23213	Composition with the Hilbert space identity operator. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.)
|- ( T : ~H --> ~H -> ( Iop o. T ) = T )
18.6.3  Operations on Hilbert space operators
Theorem	hoaddcl 23214	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 23215	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 23216*	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 23217*	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 23218	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 23219	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 23220	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 23221	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 23222	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 23223	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 23224	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 23225	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 23226	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 23227	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 23228	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 23229	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 23230	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 23231	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 23232	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 23233	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 23234	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 23235	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 23236	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 23237	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 23238	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 23239	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 23240	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 23241	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 23242	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 23243	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 23244	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 23245	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 23246	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 23247	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 23248	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 23249	A Hilbert space operator is not empty. (Contributed by NM, 24-Mar-2006.) (New usage is discouraged.)
|- ( T : ~H --> ~H -> -. T = (/) )
Theorem	hodseqi 23250	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 23251	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 23252	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 23253	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 23254	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 23255	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 23256	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 23257	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 23258	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 23259	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 23260	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 23261	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 23262	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 23263	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 23264	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 23265	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 23266	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 23267	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 23268	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 23269	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 23270	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 23271	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 23272	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 23273	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 23274	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 23275	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 23276	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 23277	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 23278	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 23279	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 23280	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 23281	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 23282	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 23283	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 23284*	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 23285*	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 23286*	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 23287*	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 23288*	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 23289*	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 23290	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 23291	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 23292	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 23293	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 23294	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 ) )
18.6.4  Linear, continuous, bounded, Hermitian, unitary operators and norms
Definition	df-nmop 23295*	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 23296*	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.)
|- ConOp = { 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 23297*	Define the set of linear operators on Hilbert space. (See df-hosum 23186 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 ) ) }
Definition	df-bdop 23298	Define the set of bounded linear Hilbert space operators. (See df-hosum 23186 for definition of operator.) (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.)
|- BndLinOp = { t e. LinOp | ( normop ` t ) < +oo }
Definition	df-unop 23299*	Define the set of unitary operators on Hilbert space. (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.)
|- UniOp = { t | ( t : ~H -onto-> ~H /\ A. x e. ~H A. y e. ~H ( ( t ` x ) .ih ( t ` y ) ) = ( x .ih y ) ) }
Definition	df-hmop 23300*	Define the set of Hermitian operators on Hilbert space. Some books call these "symmetric operators" and others call them "self-adjoint operators," sometimes with slightly different technical meanings. (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.)
|- HrmOp = { t e. ( ~H ^m ~H ) | A. x e. ~H A. y e. ~H ( x .ih ( t ` y ) ) = ( ( t ` x ) .ih y ) }