Metamath Proof Explorer

Theorem eighmre

Description: The eigenvalues of a Hermitian operator are real. Equation 1.30 of Hughes p. 49. (Contributed by NM, 19-Mar-2006) (New usage is discouraged.)

Ref Expression
Assertion eighmre 
|- ( ( T e. HrmOp /\ A e. ( eigvec ` T ) ) -> ( ( eigval ` T ) ` A ) e. RR )

Proof

Step Hyp Ref Expression
1 hmopf 
 |-  ( T e. HrmOp -> T : ~H --> ~H )
2 eleigveccl 
 |-  ( ( T : ~H --> ~H /\ A e. ( eigvec ` T ) ) -> A e. ~H )
3 eigvalcl 
 |-  ( ( T : ~H --> ~H /\ A e. ( eigvec ` T ) ) -> ( ( eigval ` T ) ` A ) e. CC )
4 2 3 jca 
 |-  ( ( T : ~H --> ~H /\ A e. ( eigvec ` T ) ) -> ( A e. ~H /\ ( ( eigval ` T ) ` A ) e. CC ) )
5 eigvec1 
 |-  ( ( T : ~H --> ~H /\ A e. ( eigvec ` T ) ) -> ( ( T ` A ) = ( ( ( eigval ` T ) ` A ) .h A ) /\ A =/= 0h ) )
6 4 5 jca 
 |-  ( ( T : ~H --> ~H /\ A e. ( eigvec ` T ) ) -> ( ( A e. ~H /\ ( ( eigval ` T ) ` A ) e. CC ) /\ ( ( T ` A ) = ( ( ( eigval ` T ) ` A ) .h A ) /\ A =/= 0h ) ) )
7 1 6 sylan 
 |-  ( ( T e. HrmOp /\ A e. ( eigvec ` T ) ) -> ( ( A e. ~H /\ ( ( eigval ` T ) ` A ) e. CC ) /\ ( ( T ` A ) = ( ( ( eigval ` T ) ` A ) .h A ) /\ A =/= 0h ) ) )
8 2 2 jca 
 |-  ( ( T : ~H --> ~H /\ A e. ( eigvec ` T ) ) -> ( A e. ~H /\ A e. ~H ) )
9 1 8 sylan 
 |-  ( ( T e. HrmOp /\ A e. ( eigvec ` T ) ) -> ( A e. ~H /\ A e. ~H ) )
10 hmop 
 |-  ( ( T e. HrmOp /\ A e. ~H /\ A e. ~H ) -> ( A .ih ( T ` A ) ) = ( ( T ` A ) .ih A ) )
11 10 3expb 
 |-  ( ( T e. HrmOp /\ ( A e. ~H /\ A e. ~H ) ) -> ( A .ih ( T ` A ) ) = ( ( T ` A ) .ih A ) )
12 9 11 syldan 
 |-  ( ( T e. HrmOp /\ A e. ( eigvec ` T ) ) -> ( A .ih ( T ` A ) ) = ( ( T ` A ) .ih A ) )
13 eigre 
 |-  ( ( ( A e. ~H /\ ( ( eigval ` T ) ` A ) e. CC ) /\ ( ( T ` A ) = ( ( ( eigval ` T ) ` A ) .h A ) /\ A =/= 0h ) ) -> ( ( A .ih ( T ` A ) ) = ( ( T ` A ) .ih A ) <-> ( ( eigval ` T ) ` A ) e. RR ) )
14 13 biimpa 
 |-  ( ( ( ( A e. ~H /\ ( ( eigval ` T ) ` A ) e. CC ) /\ ( ( T ` A ) = ( ( ( eigval ` T ) ` A ) .h A ) /\ A =/= 0h ) ) /\ ( A .ih ( T ` A ) ) = ( ( T ` A ) .ih A ) ) -> ( ( eigval ` T ) ` A ) e. RR )
15 7 12 14 syl2anc 
 |-  ( ( T e. HrmOp /\ A e. ( eigvec ` T ) ) -> ( ( eigval ` T ) ` A ) e. RR )