# Metamath Proof Explorer

## Theorem eigrei

Description: A necessary and sufficient condition (that holds when T is a Hermitian operator) for an eigenvalue B to be real. Generalization of Equation 1.30 of Hughes p. 49. (Contributed by NM, 21-Jan-2005) (New usage is discouraged.)

Ref Expression
Hypotheses eigre.1 ${⊢}{A}\in ℋ$
eigre.2 ${⊢}{B}\in ℂ$
Assertion eigrei ${⊢}\left({T}\left({A}\right)={B}{\cdot }_{ℎ}{A}\wedge {A}\ne {0}_{ℎ}\right)\to \left({A}{\cdot }_{\mathrm{ih}}{T}\left({A}\right)={T}\left({A}\right){\cdot }_{\mathrm{ih}}{A}↔{B}\in ℝ\right)$

### Proof

Step Hyp Ref Expression
1 eigre.1 ${⊢}{A}\in ℋ$
2 eigre.2 ${⊢}{B}\in ℂ$
3 oveq2 ${⊢}{T}\left({A}\right)={B}{\cdot }_{ℎ}{A}\to {A}{\cdot }_{\mathrm{ih}}{T}\left({A}\right)={A}{\cdot }_{\mathrm{ih}}\left({B}{\cdot }_{ℎ}{A}\right)$
4 his5 ${⊢}\left({B}\in ℂ\wedge {A}\in ℋ\wedge {A}\in ℋ\right)\to {A}{\cdot }_{\mathrm{ih}}\left({B}{\cdot }_{ℎ}{A}\right)=\stackrel{‾}{{B}}\left({A}{\cdot }_{\mathrm{ih}}{A}\right)$
5 2 1 1 4 mp3an ${⊢}{A}{\cdot }_{\mathrm{ih}}\left({B}{\cdot }_{ℎ}{A}\right)=\stackrel{‾}{{B}}\left({A}{\cdot }_{\mathrm{ih}}{A}\right)$
6 3 5 syl6eq ${⊢}{T}\left({A}\right)={B}{\cdot }_{ℎ}{A}\to {A}{\cdot }_{\mathrm{ih}}{T}\left({A}\right)=\stackrel{‾}{{B}}\left({A}{\cdot }_{\mathrm{ih}}{A}\right)$
7 oveq1 ${⊢}{T}\left({A}\right)={B}{\cdot }_{ℎ}{A}\to {T}\left({A}\right){\cdot }_{\mathrm{ih}}{A}=\left({B}{\cdot }_{ℎ}{A}\right){\cdot }_{\mathrm{ih}}{A}$
8 ax-his3 ${⊢}\left({B}\in ℂ\wedge {A}\in ℋ\wedge {A}\in ℋ\right)\to \left({B}{\cdot }_{ℎ}{A}\right){\cdot }_{\mathrm{ih}}{A}={B}\left({A}{\cdot }_{\mathrm{ih}}{A}\right)$
9 2 1 1 8 mp3an ${⊢}\left({B}{\cdot }_{ℎ}{A}\right){\cdot }_{\mathrm{ih}}{A}={B}\left({A}{\cdot }_{\mathrm{ih}}{A}\right)$
10 7 9 syl6eq ${⊢}{T}\left({A}\right)={B}{\cdot }_{ℎ}{A}\to {T}\left({A}\right){\cdot }_{\mathrm{ih}}{A}={B}\left({A}{\cdot }_{\mathrm{ih}}{A}\right)$
11 6 10 eqeq12d ${⊢}{T}\left({A}\right)={B}{\cdot }_{ℎ}{A}\to \left({A}{\cdot }_{\mathrm{ih}}{T}\left({A}\right)={T}\left({A}\right){\cdot }_{\mathrm{ih}}{A}↔\stackrel{‾}{{B}}\left({A}{\cdot }_{\mathrm{ih}}{A}\right)={B}\left({A}{\cdot }_{\mathrm{ih}}{A}\right)\right)$
12 1 1 hicli ${⊢}{A}{\cdot }_{\mathrm{ih}}{A}\in ℂ$
13 ax-his4 ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to 0<{A}{\cdot }_{\mathrm{ih}}{A}$
14 1 13 mpan ${⊢}{A}\ne {0}_{ℎ}\to 0<{A}{\cdot }_{\mathrm{ih}}{A}$
15 14 gt0ne0d ${⊢}{A}\ne {0}_{ℎ}\to {A}{\cdot }_{\mathrm{ih}}{A}\ne 0$
16 2 cjcli ${⊢}\stackrel{‾}{{B}}\in ℂ$
17 mulcan2 ${⊢}\left(\stackrel{‾}{{B}}\in ℂ\wedge {B}\in ℂ\wedge \left({A}{\cdot }_{\mathrm{ih}}{A}\in ℂ\wedge {A}{\cdot }_{\mathrm{ih}}{A}\ne 0\right)\right)\to \left(\stackrel{‾}{{B}}\left({A}{\cdot }_{\mathrm{ih}}{A}\right)={B}\left({A}{\cdot }_{\mathrm{ih}}{A}\right)↔\stackrel{‾}{{B}}={B}\right)$
18 16 2 17 mp3an12 ${⊢}\left({A}{\cdot }_{\mathrm{ih}}{A}\in ℂ\wedge {A}{\cdot }_{\mathrm{ih}}{A}\ne 0\right)\to \left(\stackrel{‾}{{B}}\left({A}{\cdot }_{\mathrm{ih}}{A}\right)={B}\left({A}{\cdot }_{\mathrm{ih}}{A}\right)↔\stackrel{‾}{{B}}={B}\right)$
19 12 15 18 sylancr ${⊢}{A}\ne {0}_{ℎ}\to \left(\stackrel{‾}{{B}}\left({A}{\cdot }_{\mathrm{ih}}{A}\right)={B}\left({A}{\cdot }_{\mathrm{ih}}{A}\right)↔\stackrel{‾}{{B}}={B}\right)$
20 11 19 sylan9bb ${⊢}\left({T}\left({A}\right)={B}{\cdot }_{ℎ}{A}\wedge {A}\ne {0}_{ℎ}\right)\to \left({A}{\cdot }_{\mathrm{ih}}{T}\left({A}\right)={T}\left({A}\right){\cdot }_{\mathrm{ih}}{A}↔\stackrel{‾}{{B}}={B}\right)$
21 2 cjrebi ${⊢}{B}\in ℝ↔\stackrel{‾}{{B}}={B}$
22 20 21 syl6bbr ${⊢}\left({T}\left({A}\right)={B}{\cdot }_{ℎ}{A}\wedge {A}\ne {0}_{ℎ}\right)\to \left({A}{\cdot }_{\mathrm{ih}}{T}\left({A}\right)={T}\left({A}\right){\cdot }_{\mathrm{ih}}{A}↔{B}\in ℝ\right)$