Metamath Proof Explorer

Theorem eigorth

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-Mar-2006) (New usage is discouraged.)

Ref Expression
Assertion eigorth ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℂ ∧ D ∈ ℂ ∧ 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 fveq2 ⊢ A = if A ∈ ℋ A 0 ℎ → T ⁡ A = T ⁡ if A ∈ ℋ A 0 ℎ
2 oveq2 ⊢ A = if A ∈ ℋ A 0 ℎ → C ⋅ ℎ A = C ⋅ ℎ if A ∈ ℋ A 0 ℎ
3 1 2 eqeq12d ⊢ A = if A ∈ ℋ A 0 ℎ → T ⁡ A = C ⋅ ℎ A ↔ T ⁡ if A ∈ ℋ A 0 ℎ = C ⋅ ℎ if A ∈ ℋ A 0 ℎ
4 3 anbi1d ⊢ A = if A ∈ ℋ A 0 ℎ → T ⁡ A = C ⋅ ℎ A ∧ T ⁡ B = D ⋅ ℎ B ↔ T ⁡ if A ∈ ℋ A 0 ℎ = C ⋅ ℎ if A ∈ ℋ A 0 ℎ ∧ T ⁡ B = D ⋅ ℎ B
5 4 anbi1d ⊢ A = if A ∈ ℋ A 0 ℎ → T ⁡ A = C ⋅ ℎ A ∧ T ⁡ B = D ⋅ ℎ B ∧ C ≠ D ‾ ↔ T ⁡ if A ∈ ℋ A 0 ℎ = C ⋅ ℎ if A ∈ ℋ A 0 ℎ ∧ T ⁡ B = D ⋅ ℎ B ∧ C ≠ D ‾
6 oveq1 ⊢ A = if A ∈ ℋ A 0 ℎ → A ⋅ ih T ⁡ B = if A ∈ ℋ A 0 ℎ ⋅ ih T ⁡ B
7 1 oveq1d ⊢ A = if A ∈ ℋ A 0 ℎ → T ⁡ A ⋅ ih B = T ⁡ if A ∈ ℋ A 0 ℎ ⋅ ih B
8 6 7 eqeq12d ⊢ A = if A ∈ ℋ A 0 ℎ → A ⋅ ih T ⁡ B = T ⁡ A ⋅ ih B ↔ if A ∈ ℋ A 0 ℎ ⋅ ih T ⁡ B = T ⁡ if A ∈ ℋ A 0 ℎ ⋅ ih B
9 oveq1 ⊢ A = if A ∈ ℋ A 0 ℎ → A ⋅ ih B = if A ∈ ℋ A 0 ℎ ⋅ ih B
10 9 eqeq1d ⊢ A = if A ∈ ℋ A 0 ℎ → A ⋅ ih B = 0 ↔ if A ∈ ℋ A 0 ℎ ⋅ ih B = 0
11 8 10 bibi12d ⊢ A = if A ∈ ℋ A 0 ℎ → A ⋅ ih T ⁡ B = T ⁡ A ⋅ ih B ↔ A ⋅ ih B = 0 ↔ if A ∈ ℋ A 0 ℎ ⋅ ih T ⁡ B = T ⁡ if A ∈ ℋ A 0 ℎ ⋅ ih B ↔ if A ∈ ℋ A 0 ℎ ⋅ ih B = 0
12 5 11 imbi12d ⊢ A = if A ∈ ℋ A 0 ℎ → T ⁡ A = C ⋅ ℎ A ∧ T ⁡ B = D ⋅ ℎ B ∧ C ≠ D ‾ → A ⋅ ih T ⁡ B = T ⁡ A ⋅ ih B ↔ A ⋅ ih B = 0 ↔ T ⁡ if A ∈ ℋ A 0 ℎ = C ⋅ ℎ if A ∈ ℋ A 0 ℎ ∧ T ⁡ B = D ⋅ ℎ B ∧ C ≠ D ‾ → if A ∈ ℋ A 0 ℎ ⋅ ih T ⁡ B = T ⁡ if A ∈ ℋ A 0 ℎ ⋅ ih B ↔ if A ∈ ℋ A 0 ℎ ⋅ ih B = 0
13 fveq2 ⊢ B = if B ∈ ℋ B 0 ℎ → T ⁡ B = T ⁡ if B ∈ ℋ B 0 ℎ
14 oveq2 ⊢ B = if B ∈ ℋ B 0 ℎ → D ⋅ ℎ B = D ⋅ ℎ if B ∈ ℋ B 0 ℎ
15 13 14 eqeq12d ⊢ B = if B ∈ ℋ B 0 ℎ → T ⁡ B = D ⋅ ℎ B ↔ T ⁡ if B ∈ ℋ B 0 ℎ = D ⋅ ℎ if B ∈ ℋ B 0 ℎ
16 15 anbi2d ⊢ B = if B ∈ ℋ B 0 ℎ → T ⁡ if A ∈ ℋ A 0 ℎ = C ⋅ ℎ if A ∈ ℋ A 0 ℎ ∧ T ⁡ B = D ⋅ ℎ B ↔ T ⁡ if A ∈ ℋ A 0 ℎ = C ⋅ ℎ if A ∈ ℋ A 0 ℎ ∧ T ⁡ if B ∈ ℋ B 0 ℎ = D ⋅ ℎ if B ∈ ℋ B 0 ℎ
17 16 anbi1d ⊢ B = if B ∈ ℋ B 0 ℎ → T ⁡ if A ∈ ℋ A 0 ℎ = C ⋅ ℎ if A ∈ ℋ A 0 ℎ ∧ T ⁡ B = D ⋅ ℎ B ∧ C ≠ D ‾ ↔ T ⁡ if A ∈ ℋ A 0 ℎ = C ⋅ ℎ if A ∈ ℋ A 0 ℎ ∧ T ⁡ if B ∈ ℋ B 0 ℎ = D ⋅ ℎ if B ∈ ℋ B 0 ℎ ∧ C ≠ D ‾
18 13 oveq2d ⊢ B = if B ∈ ℋ B 0 ℎ → if A ∈ ℋ A 0 ℎ ⋅ ih T ⁡ B = if A ∈ ℋ A 0 ℎ ⋅ ih T ⁡ if B ∈ ℋ B 0 ℎ
19 oveq2 ⊢ B = if B ∈ ℋ B 0 ℎ → T ⁡ if A ∈ ℋ A 0 ℎ ⋅ ih B = T ⁡ if A ∈ ℋ A 0 ℎ ⋅ ih if B ∈ ℋ B 0 ℎ
20 18 19 eqeq12d ⊢ B = if B ∈ ℋ B 0 ℎ → if A ∈ ℋ A 0 ℎ ⋅ ih T ⁡ B = T ⁡ if A ∈ ℋ A 0 ℎ ⋅ ih B ↔ if A ∈ ℋ A 0 ℎ ⋅ ih T ⁡ if B ∈ ℋ B 0 ℎ = T ⁡ if A ∈ ℋ A 0 ℎ ⋅ ih if B ∈ ℋ B 0 ℎ
21 oveq2 ⊢ B = if B ∈ ℋ B 0 ℎ → if A ∈ ℋ A 0 ℎ ⋅ ih B = if A ∈ ℋ A 0 ℎ ⋅ ih if B ∈ ℋ B 0 ℎ
22 21 eqeq1d ⊢ B = if B ∈ ℋ B 0 ℎ → if A ∈ ℋ A 0 ℎ ⋅ ih B = 0 ↔ if A ∈ ℋ A 0 ℎ ⋅ ih if B ∈ ℋ B 0 ℎ = 0
23 20 22 bibi12d ⊢ B = if B ∈ ℋ B 0 ℎ → if A ∈ ℋ A 0 ℎ ⋅ ih T ⁡ B = T ⁡ if A ∈ ℋ A 0 ℎ ⋅ ih B ↔ if A ∈ ℋ A 0 ℎ ⋅ ih B = 0 ↔ if A ∈ ℋ A 0 ℎ ⋅ ih T ⁡ if B ∈ ℋ B 0 ℎ = T ⁡ if A ∈ ℋ A 0 ℎ ⋅ ih if B ∈ ℋ B 0 ℎ ↔ if A ∈ ℋ A 0 ℎ ⋅ ih if B ∈ ℋ B 0 ℎ = 0
24 17 23 imbi12d ⊢ B = if B ∈ ℋ B 0 ℎ → T ⁡ if A ∈ ℋ A 0 ℎ = C ⋅ ℎ if A ∈ ℋ A 0 ℎ ∧ T ⁡ B = D ⋅ ℎ B ∧ C ≠ D ‾ → if A ∈ ℋ A 0 ℎ ⋅ ih T ⁡ B = T ⁡ if A ∈ ℋ A 0 ℎ ⋅ ih B ↔ if A ∈ ℋ A 0 ℎ ⋅ ih B = 0 ↔ T ⁡ if A ∈ ℋ A 0 ℎ = C ⋅ ℎ if A ∈ ℋ A 0 ℎ ∧ T ⁡ if B ∈ ℋ B 0 ℎ = D ⋅ ℎ if B ∈ ℋ B 0 ℎ ∧ C ≠ D ‾ → if A ∈ ℋ A 0 ℎ ⋅ ih T ⁡ if B ∈ ℋ B 0 ℎ = T ⁡ if A ∈ ℋ A 0 ℎ ⋅ ih if B ∈ ℋ B 0 ℎ ↔ if A ∈ ℋ A 0 ℎ ⋅ ih if B ∈ ℋ B 0 ℎ = 0
25 oveq1 ⊢ C = if C ∈ ℂ C 0 → C ⋅ ℎ if A ∈ ℋ A 0 ℎ = if C ∈ ℂ C 0 ⋅ ℎ if A ∈ ℋ A 0 ℎ
26 25 eqeq2d ⊢ C = if C ∈ ℂ C 0 → T ⁡ if A ∈ ℋ A 0 ℎ = C ⋅ ℎ if A ∈ ℋ A 0 ℎ ↔ T ⁡ if A ∈ ℋ A 0 ℎ = if C ∈ ℂ C 0 ⋅ ℎ if A ∈ ℋ A 0 ℎ
27 26 anbi1d ⊢ C = if C ∈ ℂ C 0 → T ⁡ if A ∈ ℋ A 0 ℎ = C ⋅ ℎ if A ∈ ℋ A 0 ℎ ∧ T ⁡ if B ∈ ℋ B 0 ℎ = D ⋅ ℎ if B ∈ ℋ B 0 ℎ ↔ T ⁡ if A ∈ ℋ A 0 ℎ = if C ∈ ℂ C 0 ⋅ ℎ if A ∈ ℋ A 0 ℎ ∧ T ⁡ if B ∈ ℋ B 0 ℎ = D ⋅ ℎ if B ∈ ℋ B 0 ℎ
28 neeq1 ⊢ C = if C ∈ ℂ C 0 → C ≠ D ‾ ↔ if C ∈ ℂ C 0 ≠ D ‾
29 27 28 anbi12d ⊢ C = if C ∈ ℂ C 0 → T ⁡ if A ∈ ℋ A 0 ℎ = C ⋅ ℎ if A ∈ ℋ A 0 ℎ ∧ T ⁡ if B ∈ ℋ B 0 ℎ = D ⋅ ℎ if B ∈ ℋ B 0 ℎ ∧ C ≠ D ‾ ↔ T ⁡ if A ∈ ℋ A 0 ℎ = if C ∈ ℂ C 0 ⋅ ℎ if A ∈ ℋ A 0 ℎ ∧ T ⁡ if B ∈ ℋ B 0 ℎ = D ⋅ ℎ if B ∈ ℋ B 0 ℎ ∧ if C ∈ ℂ C 0 ≠ D ‾
30 29 imbi1d ⊢ C = if C ∈ ℂ C 0 → T ⁡ if A ∈ ℋ A 0 ℎ = C ⋅ ℎ if A ∈ ℋ A 0 ℎ ∧ T ⁡ if B ∈ ℋ B 0 ℎ = D ⋅ ℎ if B ∈ ℋ B 0 ℎ ∧ C ≠ D ‾ → if A ∈ ℋ A 0 ℎ ⋅ ih T ⁡ if B ∈ ℋ B 0 ℎ = T ⁡ if A ∈ ℋ A 0 ℎ ⋅ ih if B ∈ ℋ B 0 ℎ ↔ if A ∈ ℋ A 0 ℎ ⋅ ih if B ∈ ℋ B 0 ℎ = 0 ↔ T ⁡ if A ∈ ℋ A 0 ℎ = if C ∈ ℂ C 0 ⋅ ℎ if A ∈ ℋ A 0 ℎ ∧ T ⁡ if B ∈ ℋ B 0 ℎ = D ⋅ ℎ if B ∈ ℋ B 0 ℎ ∧ if C ∈ ℂ C 0 ≠ D ‾ → if A ∈ ℋ A 0 ℎ ⋅ ih T ⁡ if B ∈ ℋ B 0 ℎ = T ⁡ if A ∈ ℋ A 0 ℎ ⋅ ih if B ∈ ℋ B 0 ℎ ↔ if A ∈ ℋ A 0 ℎ ⋅ ih if B ∈ ℋ B 0 ℎ = 0
31 oveq1 ⊢ D = if D ∈ ℂ D 0 → D ⋅ ℎ if B ∈ ℋ B 0 ℎ = if D ∈ ℂ D 0 ⋅ ℎ if B ∈ ℋ B 0 ℎ
32 31 eqeq2d ⊢ D = if D ∈ ℂ D 0 → T ⁡ if B ∈ ℋ B 0 ℎ = D ⋅ ℎ if B ∈ ℋ B 0 ℎ ↔ T ⁡ if B ∈ ℋ B 0 ℎ = if D ∈ ℂ D 0 ⋅ ℎ if B ∈ ℋ B 0 ℎ
33 32 anbi2d ⊢ D = if D ∈ ℂ D 0 → T ⁡ if A ∈ ℋ A 0 ℎ = if C ∈ ℂ C 0 ⋅ ℎ if A ∈ ℋ A 0 ℎ ∧ T ⁡ if B ∈ ℋ B 0 ℎ = D ⋅ ℎ if B ∈ ℋ B 0 ℎ ↔ T ⁡ if A ∈ ℋ A 0 ℎ = if C ∈ ℂ C 0 ⋅ ℎ if A ∈ ℋ A 0 ℎ ∧ T ⁡ if B ∈ ℋ B 0 ℎ = if D ∈ ℂ D 0 ⋅ ℎ if B ∈ ℋ B 0 ℎ
34 fveq2 ⊢ D = if D ∈ ℂ D 0 → D ‾ = if D ∈ ℂ D 0 ‾
35 34 neeq2d ⊢ D = if D ∈ ℂ D 0 → if C ∈ ℂ C 0 ≠ D ‾ ↔ if C ∈ ℂ C 0 ≠ if D ∈ ℂ D 0 ‾
36 33 35 anbi12d ⊢ D = if D ∈ ℂ D 0 → T ⁡ if A ∈ ℋ A 0 ℎ = if C ∈ ℂ C 0 ⋅ ℎ if A ∈ ℋ A 0 ℎ ∧ T ⁡ if B ∈ ℋ B 0 ℎ = D ⋅ ℎ if B ∈ ℋ B 0 ℎ ∧ if C ∈ ℂ C 0 ≠ D ‾ ↔ T ⁡ if A ∈ ℋ A 0 ℎ = if C ∈ ℂ C 0 ⋅ ℎ if A ∈ ℋ A 0 ℎ ∧ T ⁡ if B ∈ ℋ B 0 ℎ = if D ∈ ℂ D 0 ⋅ ℎ if B ∈ ℋ B 0 ℎ ∧ if C ∈ ℂ C 0 ≠ if D ∈ ℂ D 0 ‾
37 36 imbi1d ⊢ D = if D ∈ ℂ D 0 → T ⁡ if A ∈ ℋ A 0 ℎ = if C ∈ ℂ C 0 ⋅ ℎ if A ∈ ℋ A 0 ℎ ∧ T ⁡ if B ∈ ℋ B 0 ℎ = D ⋅ ℎ if B ∈ ℋ B 0 ℎ ∧ if C ∈ ℂ C 0 ≠ D ‾ → if A ∈ ℋ A 0 ℎ ⋅ ih T ⁡ if B ∈ ℋ B 0 ℎ = T ⁡ if A ∈ ℋ A 0 ℎ ⋅ ih if B ∈ ℋ B 0 ℎ ↔ if A ∈ ℋ A 0 ℎ ⋅ ih if B ∈ ℋ B 0 ℎ = 0 ↔ T ⁡ if A ∈ ℋ A 0 ℎ = if C ∈ ℂ C 0 ⋅ ℎ if A ∈ ℋ A 0 ℎ ∧ T ⁡ if B ∈ ℋ B 0 ℎ = if D ∈ ℂ D 0 ⋅ ℎ if B ∈ ℋ B 0 ℎ ∧ if C ∈ ℂ C 0 ≠ if D ∈ ℂ D 0 ‾ → if A ∈ ℋ A 0 ℎ ⋅ ih T ⁡ if B ∈ ℋ B 0 ℎ = T ⁡ if A ∈ ℋ A 0 ℎ ⋅ ih if B ∈ ℋ B 0 ℎ ↔ if A ∈ ℋ A 0 ℎ ⋅ ih if B ∈ ℋ B 0 ℎ = 0
38 ifhvhv0 ⊢ if A ∈ ℋ A 0 ℎ ∈ ℋ
39 ifhvhv0 ⊢ if B ∈ ℋ B 0 ℎ ∈ ℋ
40 0cn ⊢ 0 ∈ ℂ
41 40 elimel ⊢ if C ∈ ℂ C 0 ∈ ℂ
42 40 elimel ⊢ if D ∈ ℂ D 0 ∈ ℂ
43 38 39 41 42 eigorthi ⊢ T ⁡ if A ∈ ℋ A 0 ℎ = if C ∈ ℂ C 0 ⋅ ℎ if A ∈ ℋ A 0 ℎ ∧ T ⁡ if B ∈ ℋ B 0 ℎ = if D ∈ ℂ D 0 ⋅ ℎ if B ∈ ℋ B 0 ℎ ∧ if C ∈ ℂ C 0 ≠ if D ∈ ℂ D 0 ‾ → if A ∈ ℋ A 0 ℎ ⋅ ih T ⁡ if B ∈ ℋ B 0 ℎ = T ⁡ if A ∈ ℋ A 0 ℎ ⋅ ih if B ∈ ℋ B 0 ℎ ↔ if A ∈ ℋ A 0 ℎ ⋅ ih if B ∈ ℋ B 0 ℎ = 0
44 12 24 30 37 43 dedth4h ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℂ ∧ D ∈ ℂ → T ⁡ A = C ⋅ ℎ A ∧ T ⁡ B = D ⋅ ℎ B ∧ C ≠ D ‾ → A ⋅ ih T ⁡ B = T ⁡ A ⋅ ih B ↔ A ⋅ ih B = 0
45 44 imp ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℂ ∧ D ∈ ℂ ∧ T ⁡ A = C ⋅ ℎ A ∧ T ⁡ B = D ⋅ ℎ B ∧ C ≠ D ‾ → A ⋅ ih T ⁡ B = T ⁡ A ⋅ ih B ↔ A ⋅ ih B = 0