mmtheorems98 - Metamath Proof Explorer

Jump to page: Contents + 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10752

Statement List for Metamath Proof Explorer - 9701-9800 - Page 98 of 108

Type	Label	Description
Statement
Theorem	hocsubdir 9701	Distributive law for Hilbert space operator difference.
|- R:H~-->H~   &   |- S:H~-->H~   &   |- T:H~-->H~   =>   |- ((R -op S) o. T) = ((R o. T) -op (S o. T))
Theorem	ho2co 9702	Double composition of Hilbert space operators.
|- R:H~-->H~   &   |- S:H~-->H~   &   |- T:H~-->H~   =>   |- (A e. H~ -> (((R o. S) o. T)` A) = (R` (S` (T` A))))
Theorem	hoaddasst 9703	Associativity of sum of Hilbert space operators.
|- ((R:H~-->H~ /\ S:H~-->H~ /\ T:H~-->H~) -> ((R +op S) +op T) = (R +op (S +op T)))
Theorem	hoadd23t 9704	Commutative/associative law for Hilbert space operator sum that swaps the second and third terms.
|- ((R:H~-->H~ /\ S:H~-->H~ /\ T:H~-->H~) -> ((R +op S) +op T) = ((R +op T) +op S))
Theorem	hoadd4t 9705	Rearrangement of 4 terms in a sum of Hilbert space operators.
|- (((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	hocsubdirt 9706	Distributive law for Hilbert space operator difference.
|- ((R:H~-->H~ /\ S:H~-->H~ /\ T:H~-->H~) -> ((R -op S) o. T) = ((R o. T) -op (S o. T)))
Theorem	hoaddid1 9707	Sum of a Hilbert space operator with the zero operator.
|- T:H~-->H~   =>   |- (T +op 0hop) = T
Theorem	hodid 9708	Difference of a Hilbert space operator from itself.
|- T:H~-->H~   =>   |- (T -op T) = 0hop
Theorem	ho0co 9709	Composition of the zero operator and a Hilbert space operator.
|- T:H~-->H~   =>   |- (0hop o. T) = 0hop
Theorem	hoid1 9710	Composition of Hilbert space operator with unit identity.
|- T:H~-->H~   =>   |- (T o. Iop ) = T
Theorem	hoid1r 9711	Composition of Hilbert space operator with unit identity.
|- T:H~-->H~   =>   |- ( Iop o. T) = T
Theorem	hoaddid1t 9712	Sum of a Hilbert space operator with the zero operator.
|- (T:H~-->H~ -> (T +op 0hop) = T)
Theorem	hodidt 9713	Difference of a Hilbert space operator from itself.
|- (T:H~-->H~ -> (T -op T) = 0hop)
Theorem	hon0 9714	A Hilbert space operator is not empty.
|- (T:H~-->H~ -> -. T = (/))
Theorem	hodseq 9715	Subtraction and addition of equal Hilbert space operators.
|- S:H~-->H~   &   |- T:H~-->H~   =>   |- (S +op (T -op S)) = T
Theorem	ho0sub 9716	Subtraction of Hilbert space operators expressed in terms of difference from zero.
|- S:H~-->H~   &   |- T:H~-->H~   =>   |- (S -op T) = (S +op (0hop -op T))
Theorem	honegsub 9717	Relationship between Hilbert operator addition and subtraction.
|- S:H~-->H~   &   |- T:H~-->H~   =>   |- (S +op (-u1 .op T)) = (S -op T)
Theorem	ho0subt 9718	Subtraction of Hilbert space operators expressed in terms of difference from zero.
|- ((S:H~-->H~ /\ T:H~-->H~) -> (S -op T) = (S +op (0hop -op T)))
Theorem	hosubid1t 9719	The zero operator subtracted from a Hilbert space operator.
|- (T:H~-->H~ -> (T -op 0hop) = T)
Theorem	honegsubt 9720	Relationship between Hilbert space operator addition and subtraction.
|- ((T:H~-->H~ /\ U:H~-->H~) -> (T +op (-u1 .op U)) = (T -op U))
Theorem	homulid2t 9721	An operator equals its scalar product with one.
|- (T:H~-->H~ -> (1 .op T) = T)
Theorem	homco1t 9722	Associative law for scalar product and composition of operators.
|- ((A e. CC /\ T:H~-->H~ /\ U:H~-->H~) -> ((A .op T) o. U) = (A .op (T o. U)))
Theorem	homulasst 9723	Scalar product associative law for Hilbert space operators.
|- ((A e. CC /\ B e. CC /\ T:H~-->H~) -> ((A x. B) .op T) = (A .op (B .op T)))
Theorem	hoadddit 9724	Scalar product distributive law for Hilbert space operators.
|- ((A e. CC /\ T:H~-->H~ /\ U:H~-->H~) -> (A .op (T +op U)) = ((A .op T) +op (A .op U)))
Theorem	hoadddirt 9725	Scalar product reverse distributive law for Hilbert space operators.
|- ((A e. CC /\ B e. CC /\ T:H~-->H~) -> ((A + B) .op T) = ((A .op T) +op (B .op T)))
Theorem	homul12t 9726	Swap first and second factors in a nested operator scalar product.
|- ((A e. CC /\ B e. CC /\ T:H~-->H~) -> (A .op (B .op T)) = (B .op (A .op T)))
Theorem	honegnegt 9727	Double negative of a Hilbert space operator.
|- (T:H~-->H~ -> (-u1 .op (-u1 .op T)) = T)
Theorem	hosubnegt 9728	Relationship between operator subtraction and negative.
|- ((T:H~-->H~ /\ U:H~-->H~) -> (T -op (-u1 .op U)) = (T +op U))
Theorem	hosubdit 9729	Scalar product distributive law for operator difference.
|- ((A e. CC /\ T:H~-->H~ /\ U:H~-->H~) -> (A .op (T -op U)) = ((A .op T) -op (A .op U)))
Theorem	honegdit 9730	Distribution of negative over addition.
|- ((T:H~-->H~ /\ U:H~-->H~) -> (-u1 .op (T +op U)) = ((-u1 .op T) +op (-u1 .op U)))
Theorem	honegsubdit 9731	Distribution of negative over subtraction.
|- ((T:H~-->H~ /\ U:H~-->H~) -> (-u1 .op (T -op U)) = ((-u1 .op T) +op U))
Theorem	honegsubdi2t 9732	Distribution of negative over subtraction.
|- ((T:H~-->H~ /\ U:H~-->H~) -> (-u1 .op (T -op U)) = (U -op T))
Theorem	hosubsub2t 9733	Law for double subtraction of Hilbert space operators.
|- ((S:H~-->H~ /\ T:H~-->H~ /\ U:H~-->H~) -> (S -op (T -op U)) = (S +op (U -op T)))
Theorem	hosub4t 9734	Rearrangement of 4 terms in a mixed addition and subtraction of Hilbert space operators.
|- (((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	hosubadd4t 9735	Rearrangement of 4 terms in a mixed addition and subtraction of Hilbert space operators.
|- (((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	hoaddsubasst 9736	Associative-type law for addition and subtraction of Hilbert space operators.
|- ((S:H~-->H~ /\ T:H~-->H~ /\ U:H~-->H~) -> ((S +op T) -op U) = (S +op (T -op U)))
Theorem	hoaddsubt 9737	Law for operator addition and subtraction of Hilbert space operators.
|- ((S:H~-->H~ /\ T:H~-->H~ /\ U:H~-->H~) -> ((S +op T) -op U) = ((S -op U) +op T))
Theorem	hosubsubt 9738	Law for double subtraction of Hilbert space operators.
|- ((S:H~-->H~ /\ T:H~-->H~ /\ U:H~-->H~) -> (S -op (T -op U)) = ((S -op T) +op U))
Theorem	hosubsub4t 9739	Law for double subtraction of Hilbert space operators.
|- ((S:H~-->H~ /\ T:H~-->H~ /\ U:H~-->H~) -> ((S -op T) -op U) = (S -op (T +op U)))
Theorem	ho2timest 9740	Two times a Hilbert space operator.
|- (T:H~-->H~ -> (2 .op T) = (T +op T))
Theorem	hoaddsubass 9741	Associativity of sum and difference of Hilbert space operators.
|- R:H~-->H~   &   |- S:H~-->H~   &   |- T:H~-->H~   =>   |- ((R +op S) -op T) = (R +op (S -op T))
Theorem	hoaddsub 9742	Law for sum and difference of Hilbert space operators.
|- R:H~-->H~   &   |- S:H~-->H~   &   |- T:H~-->H~   =>   |- ((R +op S) -op T) = ((R -op T) +op S)
Theorem	hosd1 9743	Hilbert space operator sum expressed in terms of difference.
|- T:H~-->H~   &   |- U:H~-->H~   =>   |- (T +op U) = (T -op (0hop -op U))
Theorem	hosd2 9744	Hilbert space operator sum expressed in terms of difference.
|- T:H~-->H~   &   |- U:H~-->H~   =>   |- (T +op U) = (T -op ((U -op U) -op U))
Theorem	hopncan 9745	Hilbert space operator cancellation law.
|- T:H~-->H~   &   |- U:H~-->H~   =>   |- ((T +op U) -op U) = T
Theorem	honpcan 9746	Hilbert space operator cancellation law.
|- T:H~-->H~   &   |- U:H~-->H~   =>   |- ((T -op U) +op U) = T
Theorem	hosubeq0 9747	If the difference between two operators is zero, they are equal.
|- T:H~-->H~   &   |- U:H~-->H~   =>   |- ((T -op U) = 0hop <-> T = U)
Theorem	honpncan 9748	Hilbert space operator cancellation law.
|- R:H~-->H~&nbs