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 ∈ ℋ
eigorthi.2 ⊢ B ∈ ℋ
eigorthi.3 ⊢ C ∈ ℂ
eigorthi.4 ⊢ D ∈ ℂ
Assertion eigorthi ⊢ T ⁡ A = C ⋅ ℎ A ∧ T ⁡ B = D ⋅ ℎ B ∧ C ≠ D ‾ → A ⋅ ih T ⁡ B = T ⁡ A ⋅ ih B ↔ A ⋅ ih B = 0

Proof

Step Hyp Ref Expression
1 eigorthi.1 ⊢ A ∈ ℋ
2 eigorthi.2 ⊢ B ∈ ℋ
3 eigorthi.3 ⊢ C ∈ ℂ
4 eigorthi.4 ⊢ D ∈ ℂ
5 oveq2 ⊢ T ⁡ B = D ⋅ ℎ B → A ⋅ ih T ⁡ B = A ⋅ ih D ⋅ ℎ B
6 his5 ⊢ D ∈ ℂ ∧ A ∈ ℋ ∧ B ∈ ℋ → A ⋅ ih D ⋅ ℎ B = D ‾ ⁢ A ⋅ ih B
7 4 1 2 6 mp3an ⊢ A ⋅ ih D ⋅ ℎ B = D ‾ ⁢ A ⋅ ih B
8 5 7 eqtrdi ⊢ T ⁡ B = D ⋅ ℎ B → A ⋅ ih T ⁡ B = D ‾ ⁢ A ⋅ ih B
9 oveq1 ⊢ T ⁡ A = C ⋅ ℎ A → T ⁡ A ⋅ ih B = C ⋅ ℎ A ⋅ ih B
10 ax-his3 ⊢ C ∈ ℂ ∧ A ∈ ℋ ∧ B ∈ ℋ → C ⋅ ℎ A ⋅ ih B = C ⁢ A ⋅ ih B
11 3 1 2 10 mp3an ⊢ C ⋅ ℎ A ⋅ ih B = C ⁢ A ⋅ ih B
12 9 11 eqtrdi ⊢ T ⁡ A = C ⋅ ℎ A → T ⁡ A ⋅ ih B = C ⁢ A ⋅ ih B
13 8 12 eqeqan12rd ⊢ T ⁡ A = C ⋅ ℎ A ∧ T ⁡ B = D ⋅ ℎ B → A ⋅ ih T ⁡ B = T ⁡ A ⋅ ih B ↔ D ‾ ⁢ A ⋅ ih B = C ⁢ A ⋅ ih B
14 1 2 hicli ⊢ A ⋅ ih B ∈ ℂ
15 4 cjcli ⊢ D ‾ ∈ ℂ
16 mulcan2 ⊢ D ‾ ∈ ℂ ∧ C ∈ ℂ ∧ A ⋅ ih B ∈ ℂ ∧ A ⋅ ih B ≠ 0 → D ‾ ⁢ A ⋅ ih B = C ⁢ A ⋅ ih B ↔ D ‾ = C
17 15 3 16 mp3an12 ⊢ A ⋅ ih B ∈ ℂ ∧ A ⋅ ih B ≠ 0 → D ‾ ⁢ A ⋅ ih B = C ⁢ A ⋅ ih B ↔ D ‾ = C
18 14 17 mpan ⊢ A ⋅ ih B ≠ 0 → D ‾ ⁢ A ⋅ ih B = C ⁢ A ⋅ ih B ↔ D ‾ = C
19 eqcom ⊢ D ‾ = C ↔ C = D ‾
20 18 19 bitrdi ⊢ A ⋅ ih B ≠ 0 → D ‾ ⁢ A ⋅ ih B = C ⁢ A ⋅ ih B ↔ C = D ‾
21 20 biimpcd ⊢ D ‾ ⁢ A ⋅ ih B = C ⁢ A ⋅ ih B → A ⋅ ih B ≠ 0 → C = D ‾
22 21 necon1d ⊢ D ‾ ⁢ A ⋅ ih B = C ⁢ A ⋅ ih B → C ≠ D ‾ → A ⋅ ih B = 0
23 22 com12 ⊢ C ≠ D ‾ → D ‾ ⁢ A ⋅ ih B = C ⁢ A ⋅ ih B → A ⋅ ih B = 0
24 oveq2 ⊢ A ⋅ ih B = 0 → D ‾ ⁢ A ⋅ ih B = D ‾ ⋅ 0
25 oveq2 ⊢ A ⋅ ih B = 0 → C ⁢ A ⋅ ih B = C ⋅ 0
26 3 mul01i ⊢ C ⋅ 0 = 0
27 15 mul01i ⊢ D ‾ ⋅ 0 = 0
28 26 27 eqtr4i ⊢ C ⋅ 0 = D ‾ ⋅ 0
29 25 28 eqtrdi ⊢ A ⋅ ih B = 0 → C ⁢ A ⋅ ih B = D ‾ ⋅ 0
30 24 29 eqtr4d ⊢ A ⋅ ih B = 0 → D ‾ ⁢ A ⋅ ih B = C ⁢ A ⋅ ih B
31 23 30 impbid1 ⊢ C ≠ D ‾ → D ‾ ⁢ A ⋅ ih B = C ⁢ A ⋅ ih B ↔ A ⋅ ih B = 0
32 13 31 sylan9bb ⊢ T ⁡ A = C ⋅ ℎ A ∧ T ⁡ B = D ⋅ ℎ B ∧ C ≠ D ‾ → A ⋅ ih T ⁡ B = T ⁡ A ⋅ ih B ↔ A ⋅ ih B = 0