Theorem hmdmadj

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

	Ref	Expression
Assertion	hmdmadj	$$⊢T\in \mathrm{HrmOp}\to T\in \mathrm{dom}{adj}_h$$

Proof

Step	Hyp	Ref	Expression
1		hmopf	$$⊢T\in \mathrm{HrmOp}\to T:\mathscr{H}⟶\mathscr{H}$$
2		hon0	$$⊢T:\mathscr{H}⟶\mathscr{H}\to \neg T=\varnothing$$
3	1 2	syl	$$⊢T\in \mathrm{HrmOp}\to \neg T=\varnothing$$
4		hmopadj	$$⊢T\in \mathrm{HrmOp}\to {adj}_h\left(T\right)=T$$
5	4	eqeq1d	$$⊢T\in \mathrm{HrmOp}\to \left({adj}_h\left(T\right)=\varnothing \leftrightarrow T=\varnothing \right)$$
6	3 5	mtbird	$$⊢T\in \mathrm{HrmOp}\to \neg {adj}_h\left(T\right)=\varnothing$$
7		ndmfv	$$⊢\neg T\in \mathrm{dom}{adj}_h\to {adj}_h\left(T\right)=\varnothing$$
8	6 7	nsyl2	$$⊢T\in \mathrm{HrmOp}\to T\in \mathrm{dom}{adj}_h$$