mmtheorems114 - 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-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14200 143 14201-14300 144 14301-14400 145 14401-14500 146 14501-14600 147 14601-14700 148 14701-14800 149 14801-14900 150 14901-15000 151 15001-15100 152 15101-15200 153 15201-15300 154 15301-15400 155 15401-15500 156 15501-15600 157 15601-15700 158 15701-15800 159 15801-15900 160 15901-16000 161 16001-16100 162 16101-16200 163 16201-16300 164 16301-16400 165 16401-16500 166 16501-16600 167 16601-16700 168 16701-16800 169 16801-16900 170 16901-17000 171 17001-17100 172 17101-17200 173 17201-17300 174 17301-17400 175 17401-17411

Statement List for Metamath Proof Explorer - 11301-11400 - Page 114 of 175

Type	Label	Description
Statement
Theorem	pjnormi 11301	The norm of the projection is less than or equal to the norm.
|- H e. CH   &   |- A e. ~H   =>   |- (normh` ((proj` H)` A)) <_ (normh` A)
Theorem	pjpythi 11302	Pythagorean theorem for projections.
|- H e. CH   &   |- A e. ~H   =>   |- ((normh` A)^2) = (((normh` ((proj` H)` A))^2) + ((normh` ((proj` (_|_` H))` A))^2))
Theorem	pjneli 11303	If a vector does not belong to subspace, the norm of its projection is less than its norm.
|- H e. CH   &   |- A e. ~H   =>   |- (-. A e. H <-> (normh` ((proj` H)` A)) < (normh` A))
Theorem	pjnorm 11304	The norm of the projection is less than or equal to the norm.
|- ((H e. CH /\ A e. ~H) -> (normh` ((proj` H)` A)) <_ (normh` A))
Theorem	pjpyth 11305	Pythagorean theorem for projectors.
|- ((H e. CH /\ A e. ~H) -> ((normh` A)^2) = (((normh` ((proj` H)` A))^2) + ((normh` ((proj` (_|_` H))` A))^2)))
Theorem	pjnel 11306	If a vector does not belong to subspace, the norm of its projection is less than its norm.
|- ((H e. CH /\ A e. ~H) -> (-. A e. H <-> (normh` ((proj` H)` A)) < (normh` A)))
Theorem	pjnorm2 11307	A vector belongs to the subspace of a projection iff the norm of its projection equals its norm. This and pjch 11274 yield Theorem 26.3 of [Halmos] p. 44.
|- ((H e. CH /\ A e. ~H) -> (A e. H <-> (normh` ((proj` H)` A)) = (normh` A)))
Mayet's equation E_3
Theorem	mayete3i 11308	Mayet's equation E3. Part of Theorem 4.1 of [Mayet3] p. 1223.
|- A e. CH   &   |- B e. CH   &   |- C e. CH   &   |- D e. CH   &   |- F e. CH   &   |- G e. CH   &   |- A C_ (_|_` C)   &   |- A C_ (_|_` F)   &   |- C C_ (_|_` F)   &   |- A C_ (_|_` B)   &   |- C C_ (_|_` D)   &   |- F C_ (_|_` G)   &   |- X = ((A vH C) vH F)   &   |- Y = (((A vH B) i^i (C vH D)) i^i (F vH G))   &   |- Z = ((B vH D) vH G)   =>   |- (X i^i Y) C_ Z
Theorem	mayete3OLDi 11309	Mayet's equation E3. Part of Theorem 4.1 of [Mayet3] p. 7.
|- A e. CH   &   |- B e. CH   &   |- C e. CH   &   |- D e. CH   &   |- F e. CH   &   |- G e. CH   &   |- A C_ (_|_` B)   &   |- A C_ (_|_` C)   &   |- B C_ (_|_` C)   &   |- A C_ (_|_` D)   &   |- B C_ (_|_` F)   &   |- C C_ (_|_` G)   &   |- R = ((A vH B) vH C)   &   |- S = (((A vH D) i^i (B vH F)) i^i (C vH G))   &   |- T = ((D vH F) vH G)   =>   |- (R i^i S) C_ T
Theorem	mayetes3i 11310	Mayet's equation E^*3, derived from E3. Solution, for n = 3, to open problem in Remark (b) after Theorem 7.1 of [Mayet3] p. 1240.
|- A e. CH   &   |- B e. CH   &   |- C e. CH   &   |- D e. CH   &   |- F e. CH   &   |- G e. CH   &   |- R e. CH   &   |- A C_ (_|_` C)   &   |- A C_ (_|_` F)   &   |- C C_ (_|_` F)   &   |- A C_ (_|_` B)   &   |- C C_ (_|_` D)   &   |- F C_ (_|_` G)   &   |- R C_ (_|_` X)   &   |- X = ((A vH C) vH F)   &   |- Y = (((A vH B) i^i (C vH D)) i^i (F vH G))   &   |- Z = ((B vH D) vH G)   =>   |- ((X vH R) i^i Y) C_ (Z vH R)
Zero and identity operators
Definition	df-h0op 11311	Define the Hilbert space zero operator. See df0op2 11315 for alternate definition.
|- 0hop = (proj` 0H)
Definition	df-iop 11312	Define the Hilbert space identity operator. See dfiop2 11316 for alternate definition.
|- Iop = (proj` ~H)
Theorem	ho0val 11313	Value of the zero Hilbert space operator (null projector). Remark in [Beran] p. 111.
|- (A e. ~H -> (0hop` A) = 0h)
Theorem	ho0f 11314	Functionality of the zero Hilbert space operator.
|- 0hop:~H-->~H
Theorem	df0op2 11315	Alternate definition of Hilbert space zero operator.
|- 0hop = (~H X. 0H)
Theorem	dfiop2 11316	Alternate definition of Hilbert space identity operator.
|- Iop = ( _I |` ~H)
Theorem	hoif 11317	Functionality of the Hilbert space identity operator.
|- Iop :~H-1-1-onto->~H
Theorem	hoival 11318	The value of the Hilbert space identity operator.
|- (A e. ~H -> ( Iop ` A) = A)
Theorem	hoico1 11319	Composition with the Hilbert space identity operator.
|- (T:~H-->~H -> (T o. Iop ) = T)
Theorem	hoico2 11320	Composition with the Hilbert space identity operator.
|- (T:~H-->~H -> ( Iop o. T) = T)
Operations on Hilbert space operators
Theorem	hoaddcl 11321	The sum of Hilbert space operators is an operator.
|- ((S:~H-->~H /\ T:~H-->~H) -> (S +op T):~H-->~H)
Theorem	homulcl 11322	The scalar product of a Hilbert space operator is an operator.
|- ((A e. CC /\ T:~H-->~H) -> (A .op T):~H-->~H)
Theorem	hoeq 11323	Equality of Hilbert space operators.
|- ((T:~H-->~H /\ U:~H-->~H) -> (A.x e. ~H (T` x) = (U` x) <-> T = U))
Theorem	hoeqi 11324	Equality of Hilbert space operators.
|- S:~H-->~H   &   |- T:~H-->~H   =>   |- (A.x e. ~H (S` x) = (T` x) <-> S = T)
Theorem	hoscli 11325	Closure of Hilbert space operator sum.
|- S:~H-->~H   &   |- T:~H-->~H   =>   |- (A e. ~H -> ((S +op T)` A) e. ~H)
Theorem	hodcli 11326	Closure of Hilbert space operator difference.
|- S:~H-->~H   &   |- T:~H-->~H   =>   |- (A e. ~H -> ((S -op T)` A) e. ~H)
Theorem	hocoi 11327	Composition of Hilbert space operators.
|- S:~H-->~H   &   |- T:~H-->~H   =>   |- (A e. ~H -> ((S o. T)` A) = (S` (T` A)))
Theorem	hococli 11328	Closure of composition of Hilbert space operators.
|- S:~H-->~H   &   |- T:~H-->~H   =>   |- (A e. ~H -> ((S o. T)` A) e. ~H)
Theorem	hocofi 11329	Mapping of composition of Hilbert space operators.
|- S:~H-->~H   &   |- T:~H-->~H   =>   |- (S o. T):~H-->~H
Theorem	hocofni 11330	Functionality of composition of Hilbert space operators.
|- S:~H-->~H   &   |- T:~H-->~H   =>   |- (S o. T) Fn ~H
Theorem	hoaddcli 11331	Mapping of sum of Hilbert space operators.
|- S:~H-->~H   &   |- T:~H-->~H   =>   |- (S +op T):~H-->~H
Theorem	hosubcli 11332	Mapping of difference of Hilbert space operators.
|- S:~H-->~H   &   |- T:~H-->~H   =>   |- (S -op T):~H-->~H
Theorem	hoaddfni 11333	Functionality of sum of Hilbert space operators.
|- S:~H-->~H   &   |- T:~H-->~H   =>   |- (S +op T) Fn ~H
Theorem	hosubfni 11334	Functionality of difference of Hilbert space operators.
|- S:~H-->~H   &   |- T:~H-->~H   =>   |- (S -op T) Fn ~H
Theorem	hoaddcomi 11335	Commutativity of sum of Hilbert space operators.
|- S:~H-->~H   &   |- T:~H-->~H   =>   |- (S +op T) = (T +op S)
Theorem	hosubcl 11336	Mapping of difference of Hilbert space operators.
|- ((S:~H-->~H /\ T:~H-->~H) -> (S -op T):~H-->~H)
Theorem	hoaddcom 11337	Commutativity of sum of Hilbert space operators.
|- ((S:~H-->~H /\ T:~H-->~H) -> (S +op T) = (T +op S))
Theorem	hodsi 11338	Relationship between Hilbert space operator difference and sum.
|- R:~H-->~H   &   |- S:~H-->~H   &   |- T:~H-->~H   =>   |- ((R -op S) = T <-> (S +op T) = R)
Theorem	hoaddassi 11339	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	hoadd12i 11340	Commutative/associative law for Hilbert space operator sum that swaps the first two terms.
|- R:~H-->~H   &   |- S:~H-->~H   &   |- T:~H-->~H   =>   |- (R +op (S +op T)) = (S +op (R +op T))
Theorem	hoadd23i 11341	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	hocadddiri 11342	Distributive law for Hilbert space operator sum.
|- R:~H-->~H   &   |- S:~H-->~H   &   |- T:~H-->~H   =>   |- ((R +op S) o. T) = ((R o. T) +op (S o. T))
Theorem	hocsubdiri 11343	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	ho2coi 11344	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	hoaddass 11345	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	hoadd23 11346	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	hoadd4 11347	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	hocsubdir 11348	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	hoaddid1i 11349	Sum of a Hilbert space operator with the zero operator.
|- T:~H-->~H   =>   |- (T +op 0hop) = T
Theorem	hodidi 11350	Difference of a Hilbert space operator from itself.
|- T:~H-->~H   =>   |- (T -op T) = 0hop
Theorem	ho0coi 11351	Composition of the zero operator and a Hilbert space operator.
|- T:~H-->~H   =>   |- (0hop o. T) = 0hop
Theorem	hoid1i 11352	Composition of Hilbert space operator with unit identity.
|- T:~H-->~H   =>   |- (T o. Iop ) = T
Theorem	hoid1ri 11353	Composition of Hilbert space operator with unit identity.
|- T:~H-->~H   =>   |- ( Iop o. T) = T
Theorem	hoaddid1 11354	Sum of a Hilbert space operator with the zero operator.
|- (T:~H-->~H -> (T +op 0hop) = T)
Theorem	hodid 11355	Difference of a Hilbert space operator from itself.
|- (T:~H-->~H -> (T -op T) = 0hop)
Theorem	hon0 11356	A Hilbert space operator is not empty.
|- (T:~H-->~H -> -. T = (/))
Theorem	hodseqi 11357	Subtraction and addition of equal Hilbert space operators.
|- S:~H-->~H   &   |- T:~H-->~H   =>   |- (S +op (T -op S)) = T
Theorem	ho0subi 11358	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	honegsubi 11359	Relationship between Hilbert operator addition and subtraction.
|- S:~H-->~H   &   |- T:~H-->~H   =>   |- (S +op (-u1 .op T)) = (S -op T)
Theorem	ho0sub 11360	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	hosubid1 11361	The zero operator subtracted from a Hilbert space operator.
|- (T:~H-->~H -> (T -op 0hop) = T)
Theorem	honegsub 11362	Relationship between Hilbert space operator addition and subtraction.
|- ((T:~H-->~H /\ U:~H-->~H) -> (T +op (-u1 .op U)) = (T -op U))
Theorem	homulid2 11363	An operator equals its scalar product with one.
|- (T:~H-->~H -> (1 .op T) = T)
Theorem	homco1 11364	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	homulass 11365	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	hoadddi 11366	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	hoadddir 11367	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	homul12 11368	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	honegneg 11369	Double negative of a Hilbert space operator.
|- (T:~H-->~H -> (-u1 .op (-u1 .op T)) = T)
Theorem	hosubneg 11370	Relationship between operator subtraction and negative.
|- ((T:~H-->~H /\ U:~H-->~H) -> (T -op (-u1 .op U)) = (T +op U))
Theorem	hosubdi 11371	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	honegdi 11372	Distribution of negative over addition.
|- ((T:~H-->~H /\ U:~H-->~H) -> (-u1 .op (T +op U)) = ((-u1 .op T) +op (-u1 .op U)))
Theorem	honegsubdi 11373	Distribution of negative over subtraction.
|- ((T:~H-->~H /\ U:~H-->~H) -> (-u1 .op (T -op U)) = ((-u1 .op T) +op U))
Theorem	honegsubdi2 11374	Distribution of negative over subtraction.
|- ((T:~H-->~H /\ U:~H-->~H) -> (-u1 .op (T -op U)) = (U -op T))
Theorem	hosubsub2 11375	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	hosub4 11376	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	hosubadd4 11377	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	hoaddsubass 11378	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	hoaddsub 11379	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	hosubsub 11380	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	hosubsub4 11381	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	ho2times 11382	Two times a Hilbert space operator.
|- (T:~H-->~H -> (2 .op T) = (T +op T))
Theorem	hoaddsubassi 11383	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	hoaddsubi 11384	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	hosd1i 11385	Hilbert space operator sum expressed in terms of difference.
|- T:~H-->~H   &   |- U:~H-->~H   =>   |- (T +op U) = (T -op (0hop -op U))
Theorem	hosd2i 11386	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	hopncani 11387	Hilbert space operator cancellation law.
|- T:~H-->~H   &   |- U:~H-->~H   =>   |- ((T +op U) -op U) = T
Theorem	honpcani 11388	Hilbert space operator cancellation law.
|- T:~H-->~H   &   |- U:~H-->~H   =>   |- ((T -op U) +op U) = T
Theorem	hosubeq0i 11389	If the difference between two operators is zero, they are equal.
|- T:~H-->~H   &   |- U:~H-->~H   =>   |- ((T -op U) = 0hop <-> T = U)
Theorem	honpncani 11390	Hilbert space operator cancellation law.
|- R:~H-->~H   &   |- S:~H-->~H   &   |- T:~H-->~H   =>   |- ((R -op S) +op (S -op T)) = (R -op T)
Theorem	ho01i 11391	A condition implying that a Hilbert space operator is identically zero. Lemma 3.2(S8) of [Beran] p. 95.
|- T:~H-->~H   =>   |- (A.x e. ~H A.y e. ~H ((T` x) .ih y) = 0 <-> T = 0hop)
Theorem	ho02i 11392	A condition implying that a Hilbert space operator is identically zero. Lemma 3.2(S10) of [Beran] p. 95.
|- T:~H-->~H   =>   |- (A.x e. ~H A.y e. ~H (x .ih (T` y)) = 0 <-> T = 0hop)
Theorem	hoeq1 11393	A condition implying that two Hilbert space operators are equal. Lemma 3.2(S9) of [Beran] p. 95.
|- ((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 11394	A condition implying that two Hilbert space operators are equal. Lemma 3.2(S11) of [Beran] p. 95.
|- ((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 11395	Every Hilbert space operator has at most one adjoint.
|- E*u(u:~H-->~H /\ A.x e. ~H A.y e. ~H (x .ih (T` y)) = ((u` x) .ih y))
Theorem	adjsym 11396	Symmetry property of an adjoint.
|- ((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 11397	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.
|- 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 11398	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.
|- (((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 11399	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.
|- 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 11400	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.
|- 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))