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 NrmCVec T H T 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 NrmCVec H = t dom A | A t = t
4 3 eleq2d U NrmCVec T H T t 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 t dom A | A t = t T dom A A T = T
9 4 8 bitrdi U NrmCVec T H T dom A A T = T