Theorem ishmo

Description: The predicate "is a hermitian operator." (Contributed by NM, 26-Jan-2008) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hmoval.8	$$⊢H=\mathrm{HmOp}\left(U\right)$$
	hmoval.9	$$⊢A=U\mathrm{adj}U$$
Assertion	ishmo	$$⊢U\in \mathrm{NrmCVec}\to \left(T\in H\leftrightarrow \left(T\in \mathrm{dom}A\wedge A\left(T\right)=T\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		hmoval.8	$$⊢H=\mathrm{HmOp}\left(U\right)$$
2		hmoval.9	$$⊢A=U\mathrm{adj}U$$
3	1 2	hmoval	$$⊢U\in \mathrm{NrmCVec}\to H=\left\{t\in \mathrm{dom}A|A\left(t\right)=t\right\}$$
4	3	eleq2d	$$⊢U\in \mathrm{NrmCVec}\to \left(T\in H\leftrightarrow T\in \left\{t\in \mathrm{dom}A|A\left(t\right)=t\right\}\right)$$
5		fveq2	$$⊢t=T\to A\left(t\right)=A\left(T\right)$$
6		id	$$⊢t=T\to t=T$$
7	5 6	eqeq12d	$$⊢t=T\to \left(A\left(t\right)=t\leftrightarrow A\left(T\right)=T\right)$$
8	7	elrab	$$⊢T\in \left\{t\in \mathrm{dom}A|A\left(t\right)=t\right\}\leftrightarrow \left(T\in \mathrm{dom}A\wedge A\left(T\right)=T\right)$$
9	4 8	bitrdi	$$⊢U\in \mathrm{NrmCVec}\to \left(T\in H\leftrightarrow \left(T\in \mathrm{dom}A\wedge A\left(T\right)=T\right)\right)$$