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 = ( HmOp ` U )
	hmoval.9	|- A = ( U adj U )
Assertion	ishmo	|- ( U e. NrmCVec -> ( T e. H <-> ( T e. dom A /\ ( A ` T ) = T ) ) )

Proof

Step	Hyp	Ref	Expression
1		hmoval.8	|- H = ( HmOp ` U )
2		hmoval.9	|- A = ( U adj U )
3	1 2	hmoval	|- ( U e. NrmCVec -> H = { t e. dom A | ( A ` t ) = t } )
4	3	eleq2d	|- ( U e. NrmCVec -> ( T e. H <-> T e. { t e. dom A | ( A ` t ) = t } ) )
5		fveq2	|- ( t = T -> ( A ` t ) = ( A ` T ) )
6		id	|- ( t = T -> t = T )
7	5 6	eqeq12d	|- ( t = T -> ( ( A ` t ) = t <-> ( A ` T ) = T ) )
8	7	elrab	|- ( T e. { t e. dom A | ( A ` t ) = t } <-> ( T e. dom A /\ ( A ` T ) = T ) )
9	4 8	bitrdi	|- ( U e. NrmCVec -> ( T e. H <-> ( T e. dom A /\ ( A ` T ) = T ) ) )