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

Metamath Proof Explorer

Theorem hmopre

Description: The inner product of the value and argument of a Hermitian operator is real. (Contributed by NM, 23-Jul-2006) (New usage is discouraged.)

Ref Expression
Assertion hmopre 
|- ( ( T e. HrmOp /\ A e. ~H ) -> ( ( T ` A ) .ih A ) e. RR )

Proof

Step Hyp Ref Expression
1 hmop 
 |-  ( ( T e. HrmOp /\ A e. ~H /\ A e. ~H ) -> ( A .ih ( T ` A ) ) = ( ( T ` A ) .ih A ) )
2 1 3anidm23 
 |-  ( ( T e. HrmOp /\ A e. ~H ) -> ( A .ih ( T ` A ) ) = ( ( T ` A ) .ih A ) )
3 2 eqcomd 
 |-  ( ( T e. HrmOp /\ A e. ~H ) -> ( ( T ` A ) .ih A ) = ( A .ih ( T ` A ) ) )
4 hmopf 
 |-  ( T e. HrmOp -> T : ~H --> ~H )
5 4 ffvelcdmda 
 |-  ( ( T e. HrmOp /\ A e. ~H ) -> ( T ` A ) e. ~H )
6 hire 
 |-  ( ( ( T ` A ) e. ~H /\ A e. ~H ) -> ( ( ( T ` A ) .ih A ) e. RR <-> ( ( T ` A ) .ih A ) = ( A .ih ( T ` A ) ) ) )
7 5 6 sylancom 
 |-  ( ( T e. HrmOp /\ A e. ~H ) -> ( ( ( T ` A ) .ih A ) e. RR <-> ( ( T ` A ) .ih A ) = ( A .ih ( T ` A ) ) ) )
8 3 7 mpbird 
 |-  ( ( T e. HrmOp /\ A e. ~H ) -> ( ( T ` A ) .ih A ) e. RR )