Theorem hmopre

Description: The inner product of the value and argument of a Hermitian operator is real. (Contributed by NM, 23-Jul-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	hmopre	$$⊢\left(T\in \mathrm{HrmOp}\wedge A\in \mathscr{H}\right)\to T\left(A\right){\cdot }_{\mathrm{ih}}A\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		hmop	$$⊢\left(T\in \mathrm{HrmOp}\wedge A\in \mathscr{H}\wedge A\in \mathscr{H}\right)\to A{\cdot }_{\mathrm{ih}}T\left(A\right)=T\left(A\right){\cdot }_{\mathrm{ih}}A$$
2	1	3anidm23	$$⊢\left(T\in \mathrm{HrmOp}\wedge A\in \mathscr{H}\right)\to A{\cdot }_{\mathrm{ih}}T\left(A\right)=T\left(A\right){\cdot }_{\mathrm{ih}}A$$
3	2	eqcomd	$$⊢\left(T\in \mathrm{HrmOp}\wedge A\in \mathscr{H}\right)\to T\left(A\right){\cdot }_{\mathrm{ih}}A=A{\cdot }_{\mathrm{ih}}T\left(A\right)$$
4		hmopf	$$⊢T\in \mathrm{HrmOp}\to T:\mathscr{H}⟶\mathscr{H}$$
5	4	ffvelrnda	$$⊢\left(T\in \mathrm{HrmOp}\wedge A\in \mathscr{H}\right)\to T\left(A\right)\in \mathscr{H}$$
6		hire	$$⊢\left(T\left(A\right)\in \mathscr{H}\wedge A\in \mathscr{H}\right)\to \left(T\left(A\right){\cdot }_{\mathrm{ih}}A\in ℝ\leftrightarrow T\left(A\right){\cdot }_{\mathrm{ih}}A=A{\cdot }_{\mathrm{ih}}T\left(A\right)\right)$$
7	5 6	sylancom	$$⊢\left(T\in \mathrm{HrmOp}\wedge A\in \mathscr{H}\right)\to \left(T\left(A\right){\cdot }_{\mathrm{ih}}A\in ℝ\leftrightarrow T\left(A\right){\cdot }_{\mathrm{ih}}A=A{\cdot }_{\mathrm{ih}}T\left(A\right)\right)$$
8	3 7	mpbird	$$⊢\left(T\in \mathrm{HrmOp}\wedge A\in \mathscr{H}\right)\to T\left(A\right){\cdot }_{\mathrm{ih}}A\in ℝ$$