Theorem eigre

Description: 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.)

	Ref	Expression
Assertion	eigre	$$⊢\left(\left(A\in \mathscr{H}\wedge B\in ℂ\right)\wedge \left(T\left(A\right)=B{\cdot }_{ℎ}A\wedge A\ne 0_{ℎ}\right)\right)\to \left(A{\cdot }_{\mathrm{ih}}T\left(A\right)=T\left(A\right){\cdot }_{\mathrm{ih}}A\leftrightarrow B\in ℝ\right)$$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to T\left(A\right)=T\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)$$
2		oveq2	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to B{\cdot }_{ℎ}A=B{\cdot }_{ℎ}if\left(A\in \mathscr{H},A,0_{ℎ}\right)$$
3	1 2	eqeq12d	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to \left(T\left(A\right)=B{\cdot }_{ℎ}A\leftrightarrow T\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)=B{\cdot }_{ℎ}if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)$$
4		neeq1	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to \left(A\ne 0_{ℎ}\leftrightarrow if\left(A\in \mathscr{H},A,0_{ℎ}\right)\ne 0_{ℎ}\right)$$
5	3 4	anbi12d	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to \left(\left(T\left(A\right)=B{\cdot }_{ℎ}A\wedge A\ne 0_{ℎ}\right)\leftrightarrow \left(T\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)=B{\cdot }_{ℎ}if\left(A\in \mathscr{H},A,0_{ℎ}\right)\wedge if\left(A\in \mathscr{H},A,0_{ℎ}\right)\ne 0_{ℎ}\right)\right)$$
6		id	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)$$
7	6 1	oveq12d	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to A{\cdot }_{\mathrm{ih}}T\left(A\right)=if\left(A\in \mathscr{H},A,0_{ℎ}\right){\cdot }_{\mathrm{ih}}T\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)$$
8	1 6	oveq12d	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to T\left(A\right){\cdot }_{\mathrm{ih}}A=T\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}if\left(A\in \mathscr{H},A,0_{ℎ}\right)$$
9	7 8	eqeq12d	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to \left(A{\cdot }_{\mathrm{ih}}T\left(A\right)=T\left(A\right){\cdot }_{\mathrm{ih}}A\leftrightarrow if\left(A\in \mathscr{H},A,0_{ℎ}\right){\cdot }_{\mathrm{ih}}T\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)=T\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)$$
10	9	bibi1d	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to \left(\left(A{\cdot }_{\mathrm{ih}}T\left(A\right)=T\left(A\right){\cdot }_{\mathrm{ih}}A\leftrightarrow B\in ℝ\right)\leftrightarrow \left(if\left(A\in \mathscr{H},A,0_{ℎ}\right){\cdot }_{\mathrm{ih}}T\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)=T\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}if\left(A\in \mathscr{H},A,0_{ℎ}\right)\leftrightarrow B\in ℝ\right)\right)$$
11	5 10	imbi12d	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to \left(\left(\left(T\left(A\right)=B{\cdot }_{ℎ}A\wedge A\ne 0_{ℎ}\right)\to \left(A{\cdot }_{\mathrm{ih}}T\left(A\right)=T\left(A\right){\cdot }_{\mathrm{ih}}A\leftrightarrow B\in ℝ\right)\right)\leftrightarrow \left(\left(T\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)=B{\cdot }_{ℎ}if\left(A\in \mathscr{H},A,0_{ℎ}\right)\wedge if\left(A\in \mathscr{H},A,0_{ℎ}\right)\ne 0_{ℎ}\right)\to \left(if\left(A\in \mathscr{H},A,0_{ℎ}\right){\cdot }_{\mathrm{ih}}T\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)=T\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}if\left(A\in \mathscr{H},A,0_{ℎ}\right)\leftrightarrow B\in ℝ\right)\right)\right)$$
12		oveq1	$$⊢B=if\left(B\in ℂ,B,0\right)\to B{\cdot }_{ℎ}if\left(A\in \mathscr{H},A,0_{ℎ}\right)=if\left(B\in ℂ,B,0\right){\cdot }_{ℎ}if\left(A\in \mathscr{H},A,0_{ℎ}\right)$$
13	12	eqeq2d	$$⊢B=if\left(B\in ℂ,B,0\right)\to \left(T\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)=B{\cdot }_{ℎ}if\left(A\in \mathscr{H},A,0_{ℎ}\right)\leftrightarrow T\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)=if\left(B\in ℂ,B,0\right){\cdot }_{ℎ}if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)$$
14	13	anbi1d	$$⊢B=if\left(B\in ℂ,B,0\right)\to \left(\left(T\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)=B{\cdot }_{ℎ}if\left(A\in \mathscr{H},A,0_{ℎ}\right)\wedge if\left(A\in \mathscr{H},A,0_{ℎ}\right)\ne 0_{ℎ}\right)\leftrightarrow \left(T\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)=if\left(B\in ℂ,B,0\right){\cdot }_{ℎ}if\left(A\in \mathscr{H},A,0_{ℎ}\right)\wedge if\left(A\in \mathscr{H},A,0_{ℎ}\right)\ne 0_{ℎ}\right)\right)$$
15		eleq1	$$⊢B=if\left(B\in ℂ,B,0\right)\to \left(B\in ℝ\leftrightarrow if\left(B\in ℂ,B,0\right)\in ℝ\right)$$
16	15	bibi2d	$$⊢B=if\left(B\in ℂ,B,0\right)\to \left(\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right){\cdot }_{\mathrm{ih}}T\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)=T\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}if\left(A\in \mathscr{H},A,0_{ℎ}\right)\leftrightarrow B\in ℝ\right)\leftrightarrow \left(if\left(A\in \mathscr{H},A,0_{ℎ}\right){\cdot }_{\mathrm{ih}}T\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)=T\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}if\left(A\in \mathscr{H},A,0_{ℎ}\right)\leftrightarrow if\left(B\in ℂ,B,0\right)\in ℝ\right)\right)$$
17	14 16	imbi12d	$$⊢B=if\left(B\in ℂ,B,0\right)\to \left(\left(\left(T\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)=B{\cdot }_{ℎ}if\left(A\in \mathscr{H},A,0_{ℎ}\right)\wedge if\left(A\in \mathscr{H},A,0_{ℎ}\right)\ne 0_{ℎ}\right)\to \left(if\left(A\in \mathscr{H},A,0_{ℎ}\right){\cdot }_{\mathrm{ih}}T\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)=T\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}if\left(A\in \mathscr{H},A,0_{ℎ}\right)\leftrightarrow B\in ℝ\right)\right)\leftrightarrow \left(\left(T\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)=if\left(B\in ℂ,B,0\right){\cdot }_{ℎ}if\left(A\in \mathscr{H},A,0_{ℎ}\right)\wedge if\left(A\in \mathscr{H},A,0_{ℎ}\right)\ne 0_{ℎ}\right)\to \left(if\left(A\in \mathscr{H},A,0_{ℎ}\right){\cdot }_{\mathrm{ih}}T\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)=T\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}if\left(A\in \mathscr{H},A,0_{ℎ}\right)\leftrightarrow if\left(B\in ℂ,B,0\right)\in ℝ\right)\right)\right)$$
18		ifhvhv0	$$⊢if\left(A\in \mathscr{H},A,0_{ℎ}\right)\in \mathscr{H}$$
19		0cn	$$⊢0\in ℂ$$
20	19	elimel	$$⊢if\left(B\in ℂ,B,0\right)\in ℂ$$
21	18 20	eigrei	$$⊢\left(T\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)=if\left(B\in ℂ,B,0\right){\cdot }_{ℎ}if\left(A\in \mathscr{H},A,0_{ℎ}\right)\wedge if\left(A\in \mathscr{H},A,0_{ℎ}\right)\ne 0_{ℎ}\right)\to \left(if\left(A\in \mathscr{H},A,0_{ℎ}\right){\cdot }_{\mathrm{ih}}T\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)=T\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}if\left(A\in \mathscr{H},A,0_{ℎ}\right)\leftrightarrow if\left(B\in ℂ,B,0\right)\in ℝ\right)$$
22	11 17 21	dedth2h	$$⊢\left(A\in \mathscr{H}\wedge B\in ℂ\right)\to \left(\left(T\left(A\right)=B{\cdot }_{ℎ}A\wedge A\ne 0_{ℎ}\right)\to \left(A{\cdot }_{\mathrm{ih}}T\left(A\right)=T\left(A\right){\cdot }_{\mathrm{ih}}A\leftrightarrow B\in ℝ\right)\right)$$
23	22	imp	$$⊢\left(\left(A\in \mathscr{H}\wedge B\in ℂ\right)\wedge \left(T\left(A\right)=B{\cdot }_{ℎ}A\wedge A\ne 0_{ℎ}\right)\right)\to \left(A{\cdot }_{\mathrm{ih}}T\left(A\right)=T\left(A\right){\cdot }_{\mathrm{ih}}A\leftrightarrow B\in ℝ\right)$$