This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )