Metamath Proof Explorer

Theorem eighmorth

Description: Eigenvectors of a Hermitian operator with distinct eigenvalues are orthogonal. Equation 1.31 of Hughes p. 49. (Contributed by NM, 23-Mar-2006) (New usage is discouraged.)

Ref Expression
Assertion eighmorth ( ( ( 𝑇 ∈ HrmOp ∧ 𝐴 ∈ ( eigvec ‘ 𝑇 ) ) ∧ ( 𝐵 ∈ ( eigvec ‘ 𝑇 ) ∧ ( ( eigval ‘ 𝑇 ) ‘ 𝐴 ) ≠ ( ( eigval ‘ 𝑇 ) ‘ 𝐵 ) ) ) → ( 𝐴 ·ih 𝐵 ) = 0 )

Proof

Step Hyp Ref Expression
1 hmopf ⊢ ( 𝑇 ∈ HrmOp → 𝑇 : ℋ ⟶ ℋ )
2 eleigveccl ⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝐴 ∈ ( eigvec ‘ 𝑇 ) ) → 𝐴 ∈ ℋ )
3 1 2 sylan ⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝐴 ∈ ( eigvec ‘ 𝑇 ) ) → 𝐴 ∈ ℋ )
4 3 adantr ⊢ ( ( ( 𝑇 ∈ HrmOp ∧ 𝐴 ∈ ( eigvec ‘ 𝑇 ) ) ∧ 𝐵 ∈ ( eigvec ‘ 𝑇 ) ) → 𝐴 ∈ ℋ )
5 eleigveccl ⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝐵 ∈ ( eigvec ‘ 𝑇 ) ) → 𝐵 ∈ ℋ )
6 1 5 sylan ⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝐵 ∈ ( eigvec ‘ 𝑇 ) ) → 𝐵 ∈ ℋ )
7 6 adantlr ⊢ ( ( ( 𝑇 ∈ HrmOp ∧ 𝐴 ∈ ( eigvec ‘ 𝑇 ) ) ∧ 𝐵 ∈ ( eigvec ‘ 𝑇 ) ) → 𝐵 ∈ ℋ )
8 4 7 jca ⊢ ( ( ( 𝑇 ∈ HrmOp ∧ 𝐴 ∈ ( eigvec ‘ 𝑇 ) ) ∧ 𝐵 ∈ ( eigvec ‘ 𝑇 ) ) → ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) )
9 eighmre ⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝐴 ∈ ( eigvec ‘ 𝑇 ) ) → ( ( eigval ‘ 𝑇 ) ‘ 𝐴 ) ∈ ℝ )
10 9 recnd ⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝐴 ∈ ( eigvec ‘ 𝑇 ) ) → ( ( eigval ‘ 𝑇 ) ‘ 𝐴 ) ∈ ℂ )
11 10 adantr ⊢ ( ( ( 𝑇 ∈ HrmOp ∧ 𝐴 ∈ ( eigvec ‘ 𝑇 ) ) ∧ 𝐵 ∈ ( eigvec ‘ 𝑇 ) ) → ( ( eigval ‘ 𝑇 ) ‘ 𝐴 ) ∈ ℂ )
12 eighmre ⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝐵 ∈ ( eigvec ‘ 𝑇 ) ) → ( ( eigval ‘ 𝑇 ) ‘ 𝐵 ) ∈ ℝ )
13 12 recnd ⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝐵 ∈ ( eigvec ‘ 𝑇 ) ) → ( ( eigval ‘ 𝑇 ) ‘ 𝐵 ) ∈ ℂ )
14 13 adantlr ⊢ ( ( ( 𝑇 ∈ HrmOp ∧ 𝐴 ∈ ( eigvec ‘ 𝑇 ) ) ∧ 𝐵 ∈ ( eigvec ‘ 𝑇 ) ) → ( ( eigval ‘ 𝑇 ) ‘ 𝐵 ) ∈ ℂ )
15 11 14 jca ⊢ ( ( ( 𝑇 ∈ HrmOp ∧ 𝐴 ∈ ( eigvec ‘ 𝑇 ) ) ∧ 𝐵 ∈ ( eigvec ‘ 𝑇 ) ) → ( ( ( eigval ‘ 𝑇 ) ‘ 𝐴 ) ∈ ℂ ∧ ( ( eigval ‘ 𝑇 ) ‘ 𝐵 ) ∈ ℂ ) )
16 8 15 jca ⊢ ( ( ( 𝑇 ∈ HrmOp ∧ 𝐴 ∈ ( eigvec ‘ 𝑇 ) ) ∧ 𝐵 ∈ ( eigvec ‘ 𝑇 ) ) → ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( ( ( eigval ‘ 𝑇 ) ‘ 𝐴 ) ∈ ℂ ∧ ( ( eigval ‘ 𝑇 ) ‘ 𝐵 ) ∈ ℂ ) ) )
17 16 adantrr ⊢ ( ( ( 𝑇 ∈ HrmOp ∧ 𝐴 ∈ ( eigvec ‘ 𝑇 ) ) ∧ ( 𝐵 ∈ ( eigvec ‘ 𝑇 ) ∧ ( ( eigval ‘ 𝑇 ) ‘ 𝐴 ) ≠ ( ( eigval ‘ 𝑇 ) ‘ 𝐵 ) ) ) → ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( ( ( eigval ‘ 𝑇 ) ‘ 𝐴 ) ∈ ℂ ∧ ( ( eigval ‘ 𝑇 ) ‘ 𝐵 ) ∈ ℂ ) ) )
18 eigvec1 ⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝐴 ∈ ( eigvec ‘ 𝑇 ) ) → ( ( 𝑇 ‘ 𝐴 ) = ( ( ( eigval ‘ 𝑇 ) ‘ 𝐴 ) ·ℎ 𝐴 ) ∧ 𝐴 ≠ 0ℎ ) )
19 18 simpld ⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝐴 ∈ ( eigvec ‘ 𝑇 ) ) → ( 𝑇 ‘ 𝐴 ) = ( ( ( eigval ‘ 𝑇 ) ‘ 𝐴 ) ·ℎ 𝐴 ) )
20 1 19 sylan ⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝐴 ∈ ( eigvec ‘ 𝑇 ) ) → ( 𝑇 ‘ 𝐴 ) = ( ( ( eigval ‘ 𝑇 ) ‘ 𝐴 ) ·ℎ 𝐴 ) )
21 20 adantr ⊢ ( ( ( 𝑇 ∈ HrmOp ∧ 𝐴 ∈ ( eigvec ‘ 𝑇 ) ) ∧ 𝐵 ∈ ( eigvec ‘ 𝑇 ) ) → ( 𝑇 ‘ 𝐴 ) = ( ( ( eigval ‘ 𝑇 ) ‘ 𝐴 ) ·ℎ 𝐴 ) )
22 eigvec1 ⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝐵 ∈ ( eigvec ‘ 𝑇 ) ) → ( ( 𝑇 ‘ 𝐵 ) = ( ( ( eigval ‘ 𝑇 ) ‘ 𝐵 ) ·ℎ 𝐵 ) ∧ 𝐵 ≠ 0ℎ ) )
23 22 simpld ⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝐵 ∈ ( eigvec ‘ 𝑇 ) ) → ( 𝑇 ‘ 𝐵 ) = ( ( ( eigval ‘ 𝑇 ) ‘ 𝐵 ) ·ℎ 𝐵 ) )
24 1 23 sylan ⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝐵 ∈ ( eigvec ‘ 𝑇 ) ) → ( 𝑇 ‘ 𝐵 ) = ( ( ( eigval ‘ 𝑇 ) ‘ 𝐵 ) ·ℎ 𝐵 ) )
25 24 adantlr ⊢ ( ( ( 𝑇 ∈ HrmOp ∧ 𝐴 ∈ ( eigvec ‘ 𝑇 ) ) ∧ 𝐵 ∈ ( eigvec ‘ 𝑇 ) ) → ( 𝑇 ‘ 𝐵 ) = ( ( ( eigval ‘ 𝑇 ) ‘ 𝐵 ) ·ℎ 𝐵 ) )
26 21 25 jca ⊢ ( ( ( 𝑇 ∈ HrmOp ∧ 𝐴 ∈ ( eigvec ‘ 𝑇 ) ) ∧ 𝐵 ∈ ( eigvec ‘ 𝑇 ) ) → ( ( 𝑇 ‘ 𝐴 ) = ( ( ( eigval ‘ 𝑇 ) ‘ 𝐴 ) ·ℎ 𝐴 ) ∧ ( 𝑇 ‘ 𝐵 ) = ( ( ( eigval ‘ 𝑇 ) ‘ 𝐵 ) ·ℎ 𝐵 ) ) )
27 26 adantrr ⊢ ( ( ( 𝑇 ∈ HrmOp ∧ 𝐴 ∈ ( eigvec ‘ 𝑇 ) ) ∧ ( 𝐵 ∈ ( eigvec ‘ 𝑇 ) ∧ ( ( eigval ‘ 𝑇 ) ‘ 𝐴 ) ≠ ( ( eigval ‘ 𝑇 ) ‘ 𝐵 ) ) ) → ( ( 𝑇 ‘ 𝐴 ) = ( ( ( eigval ‘ 𝑇 ) ‘ 𝐴 ) ·ℎ 𝐴 ) ∧ ( 𝑇 ‘ 𝐵 ) = ( ( ( eigval ‘ 𝑇 ) ‘ 𝐵 ) ·ℎ 𝐵 ) ) )
28 12 cjred ⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝐵 ∈ ( eigvec ‘ 𝑇 ) ) → ( ∗ ‘ ( ( eigval ‘ 𝑇 ) ‘ 𝐵 ) ) = ( ( eigval ‘ 𝑇 ) ‘ 𝐵 ) )
29 28 neeq2d ⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝐵 ∈ ( eigvec ‘ 𝑇 ) ) → ( ( ( eigval ‘ 𝑇 ) ‘ 𝐴 ) ≠ ( ∗ ‘ ( ( eigval ‘ 𝑇 ) ‘ 𝐵 ) ) ↔ ( ( eigval ‘ 𝑇 ) ‘ 𝐴 ) ≠ ( ( eigval ‘ 𝑇 ) ‘ 𝐵 ) ) )
30 29 biimpar ⊢ ( ( ( 𝑇 ∈ HrmOp ∧ 𝐵 ∈ ( eigvec ‘ 𝑇 ) ) ∧ ( ( eigval ‘ 𝑇 ) ‘ 𝐴 ) ≠ ( ( eigval ‘ 𝑇 ) ‘ 𝐵 ) ) → ( ( eigval ‘ 𝑇 ) ‘ 𝐴 ) ≠ ( ∗ ‘ ( ( eigval ‘ 𝑇 ) ‘ 𝐵 ) ) )
31 30 anasss ⊢ ( ( 𝑇 ∈ HrmOp ∧ ( 𝐵 ∈ ( eigvec ‘ 𝑇 ) ∧ ( ( eigval ‘ 𝑇 ) ‘ 𝐴 ) ≠ ( ( eigval ‘ 𝑇 ) ‘ 𝐵 ) ) ) → ( ( eigval ‘ 𝑇 ) ‘ 𝐴 ) ≠ ( ∗ ‘ ( ( eigval ‘ 𝑇 ) ‘ 𝐵 ) ) )
32 31 adantlr ⊢ ( ( ( 𝑇 ∈ HrmOp ∧ 𝐴 ∈ ( eigvec ‘ 𝑇 ) ) ∧ ( 𝐵 ∈ ( eigvec ‘ 𝑇 ) ∧ ( ( eigval ‘ 𝑇 ) ‘ 𝐴 ) ≠ ( ( eigval ‘ 𝑇 ) ‘ 𝐵 ) ) ) → ( ( eigval ‘ 𝑇 ) ‘ 𝐴 ) ≠ ( ∗ ‘ ( ( eigval ‘ 𝑇 ) ‘ 𝐵 ) ) )
33 27 32 jca ⊢ ( ( ( 𝑇 ∈ HrmOp ∧ 𝐴 ∈ ( eigvec ‘ 𝑇 ) ) ∧ ( 𝐵 ∈ ( eigvec ‘ 𝑇 ) ∧ ( ( eigval ‘ 𝑇 ) ‘ 𝐴 ) ≠ ( ( eigval ‘ 𝑇 ) ‘ 𝐵 ) ) ) → ( ( ( 𝑇 ‘ 𝐴 ) = ( ( ( eigval ‘ 𝑇 ) ‘ 𝐴 ) ·ℎ 𝐴 ) ∧ ( 𝑇 ‘ 𝐵 ) = ( ( ( eigval ‘ 𝑇 ) ‘ 𝐵 ) ·ℎ 𝐵 ) ) ∧ ( ( eigval ‘ 𝑇 ) ‘ 𝐴 ) ≠ ( ∗ ‘ ( ( eigval ‘ 𝑇 ) ‘ 𝐵 ) ) ) )
34 simpll ⊢ ( ( ( 𝑇 ∈ HrmOp ∧ 𝐴 ∈ ( eigvec ‘ 𝑇 ) ) ∧ 𝐵 ∈ ( eigvec ‘ 𝑇 ) ) → 𝑇 ∈ HrmOp )
35 hmop ⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 ·ih ( 𝑇 ‘ 𝐵 ) ) = ( ( 𝑇 ‘ 𝐴 ) ·ih 𝐵 ) )
36 34 4 7 35 syl3anc ⊢ ( ( ( 𝑇 ∈ HrmOp ∧ 𝐴 ∈ ( eigvec ‘ 𝑇 ) ) ∧ 𝐵 ∈ ( eigvec ‘ 𝑇 ) ) → ( 𝐴 ·ih ( 𝑇 ‘ 𝐵 ) ) = ( ( 𝑇 ‘ 𝐴 ) ·ih 𝐵 ) )
37 36 adantrr ⊢ ( ( ( 𝑇 ∈ HrmOp ∧ 𝐴 ∈ ( eigvec ‘ 𝑇 ) ) ∧ ( 𝐵 ∈ ( eigvec ‘ 𝑇 ) ∧ ( ( eigval ‘ 𝑇 ) ‘ 𝐴 ) ≠ ( ( eigval ‘ 𝑇 ) ‘ 𝐵 ) ) ) → ( 𝐴 ·ih ( 𝑇 ‘ 𝐵 ) ) = ( ( 𝑇 ‘ 𝐴 ) ·ih 𝐵 ) )
38 eigorth ⊢ ( ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( ( ( eigval ‘ 𝑇 ) ‘ 𝐴 ) ∈ ℂ ∧ ( ( eigval ‘ 𝑇 ) ‘ 𝐵 ) ∈ ℂ ) ) ∧ ( ( ( 𝑇 ‘ 𝐴 ) = ( ( ( eigval ‘ 𝑇 ) ‘ 𝐴 ) ·ℎ 𝐴 ) ∧ ( 𝑇 ‘ 𝐵 ) = ( ( ( eigval ‘ 𝑇 ) ‘ 𝐵 ) ·ℎ 𝐵 ) ) ∧ ( ( eigval ‘ 𝑇 ) ‘ 𝐴 ) ≠ ( ∗ ‘ ( ( eigval ‘ 𝑇 ) ‘ 𝐵 ) ) ) ) → ( ( 𝐴 ·ih ( 𝑇 ‘ 𝐵 ) ) = ( ( 𝑇 ‘ 𝐴 ) ·ih 𝐵 ) ↔ ( 𝐴 ·ih 𝐵 ) = 0 ) )
39 38 biimpa ⊢ ( ( ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( ( ( eigval ‘ 𝑇 ) ‘ 𝐴 ) ∈ ℂ ∧ ( ( eigval ‘ 𝑇 ) ‘ 𝐵 ) ∈ ℂ ) ) ∧ ( ( ( 𝑇 ‘ 𝐴 ) = ( ( ( eigval ‘ 𝑇 ) ‘ 𝐴 ) ·ℎ 𝐴 ) ∧ ( 𝑇 ‘ 𝐵 ) = ( ( ( eigval ‘ 𝑇 ) ‘ 𝐵 ) ·ℎ 𝐵 ) ) ∧ ( ( eigval ‘ 𝑇 ) ‘ 𝐴 ) ≠ ( ∗ ‘ ( ( eigval ‘ 𝑇 ) ‘ 𝐵 ) ) ) ) ∧ ( 𝐴 ·ih ( 𝑇 ‘ 𝐵 ) ) = ( ( 𝑇 ‘ 𝐴 ) ·ih 𝐵 ) ) → ( 𝐴 ·ih 𝐵 ) = 0 )
40 17 33 37 39 syl21anc ⊢ ( ( ( 𝑇 ∈ HrmOp ∧ 𝐴 ∈ ( eigvec ‘ 𝑇 ) ) ∧ ( 𝐵 ∈ ( eigvec ‘ 𝑇 ) ∧ ( ( eigval ‘ 𝑇 ) ‘ 𝐴 ) ≠ ( ( eigval ‘ 𝑇 ) ‘ 𝐵 ) ) ) → ( 𝐴 ·ih 𝐵 ) = 0 )