# Metamath Proof Explorer

## Theorem eigorthi

Description: A necessary and sufficient condition (that holds when T is a Hermitian operator) for two eigenvectors A and B to be orthogonal. Generalization of Equation 1.31 of Hughes p. 49. (Contributed by NM, 23-Jan-2005) (New usage is discouraged.)

Ref Expression
Hypotheses eigorthi.1 ${⊢}{A}\in ℋ$
eigorthi.2 ${⊢}{B}\in ℋ$
eigorthi.3 ${⊢}{C}\in ℂ$
eigorthi.4 ${⊢}{D}\in ℂ$
Assertion eigorthi ${⊢}\left(\left({T}\left({A}\right)={C}{\cdot }_{ℎ}{A}\wedge {T}\left({B}\right)={D}{\cdot }_{ℎ}{B}\right)\wedge {C}\ne \stackrel{‾}{{D}}\right)\to \left({A}{\cdot }_{\mathrm{ih}}{T}\left({B}\right)={T}\left({A}\right){\cdot }_{\mathrm{ih}}{B}↔{A}{\cdot }_{\mathrm{ih}}{B}=0\right)$

### Proof

Step Hyp Ref Expression
1 eigorthi.1 ${⊢}{A}\in ℋ$
2 eigorthi.2 ${⊢}{B}\in ℋ$
3 eigorthi.3 ${⊢}{C}\in ℂ$
4 eigorthi.4 ${⊢}{D}\in ℂ$
5 oveq2 ${⊢}{T}\left({B}\right)={D}{\cdot }_{ℎ}{B}\to {A}{\cdot }_{\mathrm{ih}}{T}\left({B}\right)={A}{\cdot }_{\mathrm{ih}}\left({D}{\cdot }_{ℎ}{B}\right)$
6 his5 ${⊢}\left({D}\in ℂ\wedge {A}\in ℋ\wedge {B}\in ℋ\right)\to {A}{\cdot }_{\mathrm{ih}}\left({D}{\cdot }_{ℎ}{B}\right)=\stackrel{‾}{{D}}\left({A}{\cdot }_{\mathrm{ih}}{B}\right)$
7 4 1 2 6 mp3an ${⊢}{A}{\cdot }_{\mathrm{ih}}\left({D}{\cdot }_{ℎ}{B}\right)=\stackrel{‾}{{D}}\left({A}{\cdot }_{\mathrm{ih}}{B}\right)$
8 5 7 syl6eq ${⊢}{T}\left({B}\right)={D}{\cdot }_{ℎ}{B}\to {A}{\cdot }_{\mathrm{ih}}{T}\left({B}\right)=\stackrel{‾}{{D}}\left({A}{\cdot }_{\mathrm{ih}}{B}\right)$
9 oveq1 ${⊢}{T}\left({A}\right)={C}{\cdot }_{ℎ}{A}\to {T}\left({A}\right){\cdot }_{\mathrm{ih}}{B}=\left({C}{\cdot }_{ℎ}{A}\right){\cdot }_{\mathrm{ih}}{B}$
10 ax-his3 ${⊢}\left({C}\in ℂ\wedge {A}\in ℋ\wedge {B}\in ℋ\right)\to \left({C}{\cdot }_{ℎ}{A}\right){\cdot }_{\mathrm{ih}}{B}={C}\left({A}{\cdot }_{\mathrm{ih}}{B}\right)$
11 3 1 2 10 mp3an ${⊢}\left({C}{\cdot }_{ℎ}{A}\right){\cdot }_{\mathrm{ih}}{B}={C}\left({A}{\cdot }_{\mathrm{ih}}{B}\right)$
12 9 11 syl6eq ${⊢}{T}\left({A}\right)={C}{\cdot }_{ℎ}{A}\to {T}\left({A}\right){\cdot }_{\mathrm{ih}}{B}={C}\left({A}{\cdot }_{\mathrm{ih}}{B}\right)$
13 8 12 eqeqan12rd ${⊢}\left({T}\left({A}\right)={C}{\cdot }_{ℎ}{A}\wedge {T}\left({B}\right)={D}{\cdot }_{ℎ}{B}\right)\to \left({A}{\cdot }_{\mathrm{ih}}{T}\left({B}\right)={T}\left({A}\right){\cdot }_{\mathrm{ih}}{B}↔\stackrel{‾}{{D}}\left({A}{\cdot }_{\mathrm{ih}}{B}\right)={C}\left({A}{\cdot }_{\mathrm{ih}}{B}\right)\right)$
14 1 2 hicli ${⊢}{A}{\cdot }_{\mathrm{ih}}{B}\in ℂ$
15 4 cjcli ${⊢}\stackrel{‾}{{D}}\in ℂ$
16 mulcan2 ${⊢}\left(\stackrel{‾}{{D}}\in ℂ\wedge {C}\in ℂ\wedge \left({A}{\cdot }_{\mathrm{ih}}{B}\in ℂ\wedge {A}{\cdot }_{\mathrm{ih}}{B}\ne 0\right)\right)\to \left(\stackrel{‾}{{D}}\left({A}{\cdot }_{\mathrm{ih}}{B}\right)={C}\left({A}{\cdot }_{\mathrm{ih}}{B}\right)↔\stackrel{‾}{{D}}={C}\right)$
17 15 3 16 mp3an12 ${⊢}\left({A}{\cdot }_{\mathrm{ih}}{B}\in ℂ\wedge {A}{\cdot }_{\mathrm{ih}}{B}\ne 0\right)\to \left(\stackrel{‾}{{D}}\left({A}{\cdot }_{\mathrm{ih}}{B}\right)={C}\left({A}{\cdot }_{\mathrm{ih}}{B}\right)↔\stackrel{‾}{{D}}={C}\right)$
18 14 17 mpan ${⊢}{A}{\cdot }_{\mathrm{ih}}{B}\ne 0\to \left(\stackrel{‾}{{D}}\left({A}{\cdot }_{\mathrm{ih}}{B}\right)={C}\left({A}{\cdot }_{\mathrm{ih}}{B}\right)↔\stackrel{‾}{{D}}={C}\right)$
19 eqcom ${⊢}\stackrel{‾}{{D}}={C}↔{C}=\stackrel{‾}{{D}}$
20 18 19 syl6bb ${⊢}{A}{\cdot }_{\mathrm{ih}}{B}\ne 0\to \left(\stackrel{‾}{{D}}\left({A}{\cdot }_{\mathrm{ih}}{B}\right)={C}\left({A}{\cdot }_{\mathrm{ih}}{B}\right)↔{C}=\stackrel{‾}{{D}}\right)$
21 20 biimpcd ${⊢}\stackrel{‾}{{D}}\left({A}{\cdot }_{\mathrm{ih}}{B}\right)={C}\left({A}{\cdot }_{\mathrm{ih}}{B}\right)\to \left({A}{\cdot }_{\mathrm{ih}}{B}\ne 0\to {C}=\stackrel{‾}{{D}}\right)$
22 21 necon1d ${⊢}\stackrel{‾}{{D}}\left({A}{\cdot }_{\mathrm{ih}}{B}\right)={C}\left({A}{\cdot }_{\mathrm{ih}}{B}\right)\to \left({C}\ne \stackrel{‾}{{D}}\to {A}{\cdot }_{\mathrm{ih}}{B}=0\right)$
23 22 com12 ${⊢}{C}\ne \stackrel{‾}{{D}}\to \left(\stackrel{‾}{{D}}\left({A}{\cdot }_{\mathrm{ih}}{B}\right)={C}\left({A}{\cdot }_{\mathrm{ih}}{B}\right)\to {A}{\cdot }_{\mathrm{ih}}{B}=0\right)$
24 oveq2 ${⊢}{A}{\cdot }_{\mathrm{ih}}{B}=0\to \stackrel{‾}{{D}}\left({A}{\cdot }_{\mathrm{ih}}{B}\right)=\stackrel{‾}{{D}}\cdot 0$
25 oveq2 ${⊢}{A}{\cdot }_{\mathrm{ih}}{B}=0\to {C}\left({A}{\cdot }_{\mathrm{ih}}{B}\right)={C}\cdot 0$
26 3 mul01i ${⊢}{C}\cdot 0=0$
27 15 mul01i ${⊢}\stackrel{‾}{{D}}\cdot 0=0$
28 26 27 eqtr4i ${⊢}{C}\cdot 0=\stackrel{‾}{{D}}\cdot 0$
29 25 28 syl6eq ${⊢}{A}{\cdot }_{\mathrm{ih}}{B}=0\to {C}\left({A}{\cdot }_{\mathrm{ih}}{B}\right)=\stackrel{‾}{{D}}\cdot 0$
30 24 29 eqtr4d ${⊢}{A}{\cdot }_{\mathrm{ih}}{B}=0\to \stackrel{‾}{{D}}\left({A}{\cdot }_{\mathrm{ih}}{B}\right)={C}\left({A}{\cdot }_{\mathrm{ih}}{B}\right)$
31 23 30 impbid1 ${⊢}{C}\ne \stackrel{‾}{{D}}\to \left(\stackrel{‾}{{D}}\left({A}{\cdot }_{\mathrm{ih}}{B}\right)={C}\left({A}{\cdot }_{\mathrm{ih}}{B}\right)↔{A}{\cdot }_{\mathrm{ih}}{B}=0\right)$
32 13 31 sylan9bb ${⊢}\left(\left({T}\left({A}\right)={C}{\cdot }_{ℎ}{A}\wedge {T}\left({B}\right)={D}{\cdot }_{ℎ}{B}\right)\wedge {C}\ne \stackrel{‾}{{D}}\right)\to \left({A}{\cdot }_{\mathrm{ih}}{T}\left({B}\right)={T}\left({A}\right){\cdot }_{\mathrm{ih}}{B}↔{A}{\cdot }_{\mathrm{ih}}{B}=0\right)$