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⋅ihT⁡B=T⁡A⋅ihB↔A⋅ihB=0

Proof

Step Hyp Ref Expression
1 fveq2 ⊢A=ifA∈ℋA0ℎ→T⁡A=T⁡ifA∈ℋA0ℎ
2 oveq2 ⊢A=ifA∈ℋA0ℎ→C⋅ℎA=C⋅ℎifA∈ℋA0ℎ
3 1 2 eqeq12d ⊢A=ifA∈ℋA0ℎ→T⁡A=C⋅ℎA↔T⁡ifA∈ℋA0ℎ=C⋅ℎifA∈ℋA0ℎ
4 3 anbi1d ⊢A=ifA∈ℋA0ℎ→T⁡A=C⋅ℎA∧T⁡B=D⋅ℎB↔T⁡ifA∈ℋA0ℎ=C⋅ℎifA∈ℋA0ℎ∧T⁡B=D⋅ℎB
5 4 anbi1d ⊢A=ifA∈ℋA0ℎ→T⁡A=C⋅ℎA∧T⁡B=D⋅ℎB∧C≠D‾↔T⁡ifA∈ℋA0ℎ=C⋅ℎifA∈ℋA0ℎ∧T⁡B=D⋅ℎB∧C≠D‾
6 oveq1 ⊢A=ifA∈ℋA0ℎ→A⋅ihT⁡B=ifA∈ℋA0ℎ⋅ihT⁡B
7 1 oveq1d ⊢A=ifA∈ℋA0ℎ→T⁡A⋅ihB=T⁡ifA∈ℋA0ℎ⋅ihB
8 6 7 eqeq12d ⊢A=ifA∈ℋA0ℎ→A⋅ihT⁡B=T⁡A⋅ihB↔ifA∈ℋA0ℎ⋅ihT⁡B=T⁡ifA∈ℋA0ℎ⋅ihB
9 oveq1 ⊢A=ifA∈ℋA0ℎ→A⋅ihB=ifA∈ℋA0ℎ⋅ihB
10 9 eqeq1d ⊢A=ifA∈ℋA0ℎ→A⋅ihB=0↔ifA∈ℋA0ℎ⋅ihB=0
11 8 10 bibi12d ⊢A=ifA∈ℋA0ℎ→A⋅ihT⁡B=T⁡A⋅ihB↔A⋅ihB=0↔ifA∈ℋA0ℎ⋅ihT⁡B=T⁡ifA∈ℋA0ℎ⋅ihB↔ifA∈ℋA0ℎ⋅ihB=0
12 5 11 imbi12d ⊢A=ifA∈ℋA0ℎ→T⁡A=C⋅ℎA∧T⁡B=D⋅ℎB∧C≠D‾→A⋅ihT⁡B=T⁡A⋅ihB↔A⋅ihB=0↔T⁡ifA∈ℋA0ℎ=C⋅ℎifA∈ℋA0ℎ∧T⁡B=D⋅ℎB∧C≠D‾→ifA∈ℋA0ℎ⋅ihT⁡B=T⁡ifA∈ℋA0ℎ⋅ihB↔ifA∈ℋA0ℎ⋅ihB=0
13 fveq2 ⊢B=ifB∈ℋB0ℎ→T⁡B=T⁡ifB∈ℋB0ℎ
14 oveq2 ⊢B=ifB∈ℋB0ℎ→D⋅ℎB=D⋅ℎifB∈ℋB0ℎ
15 13 14 eqeq12d ⊢B=ifB∈ℋB0ℎ→T⁡B=D⋅ℎB↔T⁡ifB∈ℋB0ℎ=D⋅ℎifB∈ℋB0ℎ
16 15 anbi2d ⊢B=ifB∈ℋB0ℎ→T⁡ifA∈ℋA0ℎ=C⋅ℎifA∈ℋA0ℎ∧T⁡B=D⋅ℎB↔T⁡ifA∈ℋA0ℎ=C⋅ℎifA∈ℋA0ℎ∧T⁡ifB∈ℋB0ℎ=D⋅ℎifB∈ℋB0ℎ
17 16 anbi1d ⊢B=ifB∈ℋB0ℎ→T⁡ifA∈ℋA0ℎ=C⋅ℎifA∈ℋA0ℎ∧T⁡B=D⋅ℎB∧C≠D‾↔T⁡ifA∈ℋA0ℎ=C⋅ℎifA∈ℋA0ℎ∧T⁡ifB∈ℋB0ℎ=D⋅ℎifB∈ℋB0ℎ∧C≠D‾
18 13 oveq2d ⊢B=ifB∈ℋB0ℎ→ifA∈ℋA0ℎ⋅ihT⁡B=ifA∈ℋA0ℎ⋅ihT⁡ifB∈ℋB0ℎ
19 oveq2 ⊢B=ifB∈ℋB0ℎ→T⁡ifA∈ℋA0ℎ⋅ihB=T⁡ifA∈ℋA0ℎ⋅ihifB∈ℋB0ℎ
20 18 19 eqeq12d ⊢B=ifB∈ℋB0ℎ→ifA∈ℋA0ℎ⋅ihT⁡B=T⁡ifA∈ℋA0ℎ⋅ihB↔ifA∈ℋA0ℎ⋅ihT⁡ifB∈ℋB0ℎ=T⁡ifA∈ℋA0ℎ⋅ihifB∈ℋB0ℎ
21 oveq2 ⊢B=ifB∈ℋB0ℎ→ifA∈ℋA0ℎ⋅ihB=ifA∈ℋA0ℎ⋅ihifB∈ℋB0ℎ
22 21 eqeq1d ⊢B=ifB∈ℋB0ℎ→ifA∈ℋA0ℎ⋅ihB=0↔ifA∈ℋA0ℎ⋅ihifB∈ℋB0ℎ=0
23 20 22 bibi12d ⊢B=ifB∈ℋB0ℎ→ifA∈ℋA0ℎ⋅ihT⁡B=T⁡ifA∈ℋA0ℎ⋅ihB↔ifA∈ℋA0ℎ⋅ihB=0↔ifA∈ℋA0ℎ⋅ihT⁡ifB∈ℋB0ℎ=T⁡ifA∈ℋA0ℎ⋅ihifB∈ℋB0ℎ↔ifA∈ℋA0ℎ⋅ihifB∈ℋB0ℎ=0
24 17 23 imbi12d ⊢B=ifB∈ℋB0ℎ→T⁡ifA∈ℋA0ℎ=C⋅ℎifA∈ℋA0ℎ∧T⁡B=D⋅ℎB∧C≠D‾→ifA∈ℋA0ℎ⋅ihT⁡B=T⁡ifA∈ℋA0ℎ⋅ihB↔ifA∈ℋA0ℎ⋅ihB=0↔T⁡ifA∈ℋA0ℎ=C⋅ℎifA∈ℋA0ℎ∧T⁡ifB∈ℋB0ℎ=D⋅ℎifB∈ℋB0ℎ∧C≠D‾→ifA∈ℋA0ℎ⋅ihT⁡ifB∈ℋB0ℎ=T⁡ifA∈ℋA0ℎ⋅ihifB∈ℋB0ℎ↔ifA∈ℋA0ℎ⋅ihifB∈ℋB0ℎ=0
25 oveq1 ⊢C=ifC∈ℂC0→C⋅ℎifA∈ℋA0ℎ=ifC∈ℂC0⋅ℎifA∈ℋA0ℎ
26 25 eqeq2d ⊢C=ifC∈ℂC0→T⁡ifA∈ℋA0ℎ=C⋅ℎifA∈ℋA0ℎ↔T⁡ifA∈ℋA0ℎ=ifC∈ℂC0⋅ℎifA∈ℋA0ℎ
27 26 anbi1d ⊢C=ifC∈ℂC0→T⁡ifA∈ℋA0ℎ=C⋅ℎifA∈ℋA0ℎ∧T⁡ifB∈ℋB0ℎ=D⋅ℎifB∈ℋB0ℎ↔T⁡ifA∈ℋA0ℎ=ifC∈ℂC0⋅ℎifA∈ℋA0ℎ∧T⁡ifB∈ℋB0ℎ=D⋅ℎifB∈ℋB0ℎ
28 neeq1 ⊢C=ifC∈ℂC0→C≠D‾↔ifC∈ℂC0≠D‾
29 27 28 anbi12d ⊢C=ifC∈ℂC0→T⁡ifA∈ℋA0ℎ=C⋅ℎifA∈ℋA0ℎ∧T⁡ifB∈ℋB0ℎ=D⋅ℎifB∈ℋB0ℎ∧C≠D‾↔T⁡ifA∈ℋA0ℎ=ifC∈ℂC0⋅ℎifA∈ℋA0ℎ∧T⁡ifB∈ℋB0ℎ=D⋅ℎifB∈ℋB0ℎ∧ifC∈ℂC0≠D‾
30 29 imbi1d ⊢C=ifC∈ℂC0→T⁡ifA∈ℋA0ℎ=C⋅ℎifA∈ℋA0ℎ∧T⁡ifB∈ℋB0ℎ=D⋅ℎifB∈ℋB0ℎ∧C≠D‾→ifA∈ℋA0ℎ⋅ihT⁡ifB∈ℋB0ℎ=T⁡ifA∈ℋA0ℎ⋅ihifB∈ℋB0ℎ↔ifA∈ℋA0ℎ⋅ihifB∈ℋB0ℎ=0↔T⁡ifA∈ℋA0ℎ=ifC∈ℂC0⋅ℎifA∈ℋA0ℎ∧T⁡ifB∈ℋB0ℎ=D⋅ℎifB∈ℋB0ℎ∧ifC∈ℂC0≠D‾→ifA∈ℋA0ℎ⋅ihT⁡ifB∈ℋB0ℎ=T⁡ifA∈ℋA0ℎ⋅ihifB∈ℋB0ℎ↔ifA∈ℋA0ℎ⋅ihifB∈ℋB0ℎ=0
31 oveq1 ⊢D=ifD∈ℂD0→D⋅ℎifB∈ℋB0ℎ=ifD∈ℂD0⋅ℎifB∈ℋB0ℎ
32 31 eqeq2d ⊢D=ifD∈ℂD0→T⁡ifB∈ℋB0ℎ=D⋅ℎifB∈ℋB0ℎ↔T⁡ifB∈ℋB0ℎ=ifD∈ℂD0⋅ℎifB∈ℋB0ℎ
33 32 anbi2d ⊢D=ifD∈ℂD0→T⁡ifA∈ℋA0ℎ=ifC∈ℂC0⋅ℎifA∈ℋA0ℎ∧T⁡ifB∈ℋB0ℎ=D⋅ℎifB∈ℋB0ℎ↔T⁡ifA∈ℋA0ℎ=ifC∈ℂC0⋅ℎifA∈ℋA0ℎ∧T⁡ifB∈ℋB0ℎ=ifD∈ℂD0⋅ℎifB∈ℋB0ℎ
34 fveq2 ⊢D=ifD∈ℂD0→D‾=ifD∈ℂD0‾
35 34 neeq2d ⊢D=ifD∈ℂD0→ifC∈ℂC0≠D‾↔ifC∈ℂC0≠ifD∈ℂD0‾
36 33 35 anbi12d ⊢D=ifD∈ℂD0→T⁡ifA∈ℋA0ℎ=ifC∈ℂC0⋅ℎifA∈ℋA0ℎ∧T⁡ifB∈ℋB0ℎ=D⋅ℎifB∈ℋB0ℎ∧ifC∈ℂC0≠D‾↔T⁡ifA∈ℋA0ℎ=ifC∈ℂC0⋅ℎifA∈ℋA0ℎ∧T⁡ifB∈ℋB0ℎ=ifD∈ℂD0⋅ℎifB∈ℋB0ℎ∧ifC∈ℂC0≠ifD∈ℂD0‾
37 36 imbi1d ⊢D=ifD∈ℂD0→T⁡ifA∈ℋA0ℎ=ifC∈ℂC0⋅ℎifA∈ℋA0ℎ∧T⁡ifB∈ℋB0ℎ=D⋅ℎifB∈ℋB0ℎ∧ifC∈ℂC0≠D‾→ifA∈ℋA0ℎ⋅ihT⁡ifB∈ℋB0ℎ=T⁡ifA∈ℋA0ℎ⋅ihifB∈ℋB0ℎ↔ifA∈ℋA0ℎ⋅ihifB∈ℋB0ℎ=0↔T⁡ifA∈ℋA0ℎ=ifC∈ℂC0⋅ℎifA∈ℋA0ℎ∧T⁡ifB∈ℋB0ℎ=ifD∈ℂD0⋅ℎifB∈ℋB0ℎ∧ifC∈ℂC0≠ifD∈ℂD0‾→ifA∈ℋA0ℎ⋅ihT⁡ifB∈ℋB0ℎ=T⁡ifA∈ℋA0ℎ⋅ihifB∈ℋB0ℎ↔ifA∈ℋA0ℎ⋅ihifB∈ℋB0ℎ=0
38 ifhvhv0 ⊢ifA∈ℋA0ℎ∈ℋ
39 ifhvhv0 ⊢ifB∈ℋB0ℎ∈ℋ
40 0cn ⊢0∈ℂ
41 40 elimel ⊢ifC∈ℂC0∈ℂ
42 40 elimel ⊢ifD∈ℂD0∈ℂ
43 38 39 41 42 eigorthi ⊢T⁡ifA∈ℋA0ℎ=ifC∈ℂC0⋅ℎifA∈ℋA0ℎ∧T⁡ifB∈ℋB0ℎ=ifD∈ℂD0⋅ℎifB∈ℋB0ℎ∧ifC∈ℂC0≠ifD∈ℂD0‾→ifA∈ℋA0ℎ⋅ihT⁡ifB∈ℋB0ℎ=T⁡ifA∈ℋA0ℎ⋅ihifB∈ℋB0ℎ↔ifA∈ℋA0ℎ⋅ihifB∈ℋB0ℎ=0
44 12 24 30 37 43 dedth4h ⊢A∈ℋ∧B∈ℋ∧C∈ℂ∧D∈ℂ→T⁡A=C⋅ℎA∧T⁡B=D⋅ℎB∧C≠D‾→A⋅ihT⁡B=T⁡A⋅ihB↔A⋅ihB=0
45 44 imp ⊢A∈ℋ∧B∈ℋ∧C∈ℂ∧D∈ℂ∧T⁡A=C⋅ℎA∧T⁡B=D⋅ℎB∧C≠D‾→A⋅ihT⁡B=T⁡A⋅ihB↔A⋅ihB=0