# 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 ${⊢}\left({T}\in \mathrm{HrmOp}\wedge {A}\in \mathrm{eigvec}\left({T}\right)\right)\to \mathrm{eigval}\left({T}\right)\left({A}\right)\in ℝ$

### Proof

Step Hyp Ref Expression
1 hmopf ${⊢}{T}\in \mathrm{HrmOp}\to {T}:ℋ⟶ℋ$
2 eleigveccl ${⊢}\left({T}:ℋ⟶ℋ\wedge {A}\in \mathrm{eigvec}\left({T}\right)\right)\to {A}\in ℋ$
3 eigvalcl ${⊢}\left({T}:ℋ⟶ℋ\wedge {A}\in \mathrm{eigvec}\left({T}\right)\right)\to \mathrm{eigval}\left({T}\right)\left({A}\right)\in ℂ$
4 2 3 jca ${⊢}\left({T}:ℋ⟶ℋ\wedge {A}\in \mathrm{eigvec}\left({T}\right)\right)\to \left({A}\in ℋ\wedge \mathrm{eigval}\left({T}\right)\left({A}\right)\in ℂ\right)$
5 eigvec1 ${⊢}\left({T}:ℋ⟶ℋ\wedge {A}\in \mathrm{eigvec}\left({T}\right)\right)\to \left({T}\left({A}\right)=\mathrm{eigval}\left({T}\right)\left({A}\right){\cdot }_{ℎ}{A}\wedge {A}\ne {0}_{ℎ}\right)$
6 4 5 jca ${⊢}\left({T}:ℋ⟶ℋ\wedge {A}\in \mathrm{eigvec}\left({T}\right)\right)\to \left(\left({A}\in ℋ\wedge \mathrm{eigval}\left({T}\right)\left({A}\right)\in ℂ\right)\wedge \left({T}\left({A}\right)=\mathrm{eigval}\left({T}\right)\left({A}\right){\cdot }_{ℎ}{A}\wedge {A}\ne {0}_{ℎ}\right)\right)$
7 1 6 sylan ${⊢}\left({T}\in \mathrm{HrmOp}\wedge {A}\in \mathrm{eigvec}\left({T}\right)\right)\to \left(\left({A}\in ℋ\wedge \mathrm{eigval}\left({T}\right)\left({A}\right)\in ℂ\right)\wedge \left({T}\left({A}\right)=\mathrm{eigval}\left({T}\right)\left({A}\right){\cdot }_{ℎ}{A}\wedge {A}\ne {0}_{ℎ}\right)\right)$
8 2 2 jca ${⊢}\left({T}:ℋ⟶ℋ\wedge {A}\in \mathrm{eigvec}\left({T}\right)\right)\to \left({A}\in ℋ\wedge {A}\in ℋ\right)$
9 1 8 sylan ${⊢}\left({T}\in \mathrm{HrmOp}\wedge {A}\in \mathrm{eigvec}\left({T}\right)\right)\to \left({A}\in ℋ\wedge {A}\in ℋ\right)$
10 hmop ${⊢}\left({T}\in \mathrm{HrmOp}\wedge {A}\in ℋ\wedge {A}\in ℋ\right)\to {A}{\cdot }_{\mathrm{ih}}{T}\left({A}\right)={T}\left({A}\right){\cdot }_{\mathrm{ih}}{A}$
11 10 3expb ${⊢}\left({T}\in \mathrm{HrmOp}\wedge \left({A}\in ℋ\wedge {A}\in ℋ\right)\right)\to {A}{\cdot }_{\mathrm{ih}}{T}\left({A}\right)={T}\left({A}\right){\cdot }_{\mathrm{ih}}{A}$
12 9 11 syldan ${⊢}\left({T}\in \mathrm{HrmOp}\wedge {A}\in \mathrm{eigvec}\left({T}\right)\right)\to {A}{\cdot }_{\mathrm{ih}}{T}\left({A}\right)={T}\left({A}\right){\cdot }_{\mathrm{ih}}{A}$
13 eigre ${⊢}\left(\left({A}\in ℋ\wedge \mathrm{eigval}\left({T}\right)\left({A}\right)\in ℂ\right)\wedge \left({T}\left({A}\right)=\mathrm{eigval}\left({T}\right)\left({A}\right){\cdot }_{ℎ}{A}\wedge {A}\ne {0}_{ℎ}\right)\right)\to \left({A}{\cdot }_{\mathrm{ih}}{T}\left({A}\right)={T}\left({A}\right){\cdot }_{\mathrm{ih}}{A}↔\mathrm{eigval}\left({T}\right)\left({A}\right)\in ℝ\right)$
14 13 biimpa ${⊢}\left(\left(\left({A}\in ℋ\wedge \mathrm{eigval}\left({T}\right)\left({A}\right)\in ℂ\right)\wedge \left({T}\left({A}\right)=\mathrm{eigval}\left({T}\right)\left({A}\right){\cdot }_{ℎ}{A}\wedge {A}\ne {0}_{ℎ}\right)\right)\wedge {A}{\cdot }_{\mathrm{ih}}{T}\left({A}\right)={T}\left({A}\right){\cdot }_{\mathrm{ih}}{A}\right)\to \mathrm{eigval}\left({T}\right)\left({A}\right)\in ℝ$
15 7 12 14 syl2anc ${⊢}\left({T}\in \mathrm{HrmOp}\wedge {A}\in \mathrm{eigvec}\left({T}\right)\right)\to \mathrm{eigval}\left({T}\right)\left({A}\right)\in ℝ$