Theorem hmopadj

Description: A Hermitian operator is self-adjoint. (Contributed by NM, 24-Mar-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	hmopadj	$$⊢T\in \mathrm{HrmOp}\to {adj}_h\left(T\right)=T$$

Proof

Step	Hyp	Ref	Expression
1		hmopf	$$⊢T\in \mathrm{HrmOp}\to T:\mathscr{H}⟶\mathscr{H}$$
2		hmop	$$⊢\left(T\in \mathrm{HrmOp}\wedge x\in \mathscr{H}\wedge y\in \mathscr{H}\right)\to x{\cdot }_{\mathrm{ih}}T\left(y\right)=T\left(x\right){\cdot }_{\mathrm{ih}}y$$
3	2	eqcomd	$$⊢\left(T\in \mathrm{HrmOp}\wedge x\in \mathscr{H}\wedge y\in \mathscr{H}\right)\to T\left(x\right){\cdot }_{\mathrm{ih}}y=x{\cdot }_{\mathrm{ih}}T\left(y\right)$$
4	3	3expib	$$⊢T\in \mathrm{HrmOp}\to \left(\left(x\in \mathscr{H}\wedge y\in \mathscr{H}\right)\to T\left(x\right){\cdot }_{\mathrm{ih}}y=x{\cdot }_{\mathrm{ih}}T\left(y\right)\right)$$
5	4	ralrimivv	$$⊢T\in \mathrm{HrmOp}\to \forall x\in \mathscr{H}\forall y\in \mathscr{H}T\left(x\right){\cdot }_{\mathrm{ih}}y=x{\cdot }_{\mathrm{ih}}T\left(y\right)$$
6		adjeq	$$⊢\left(T:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\wedge \forall x\in \mathscr{H}\forall y\in \mathscr{H}T\left(x\right){\cdot }_{\mathrm{ih}}y=x{\cdot }_{\mathrm{ih}}T\left(y\right)\right)\to {adj}_h\left(T\right)=T$$
7	1 1 5 6	syl3anc	$$⊢T\in \mathrm{HrmOp}\to {adj}_h\left(T\right)=T$$