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⋅ihT⁡B=T⁡A⋅ihB↔A⋅ihB=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⋅ihT⁡B=A⋅ihD⋅ℎB
6 his5 ⊢D∈ℂ∧A∈ℋ∧B∈ℋ→A⋅ihD⋅ℎB=D‾⁢A⋅ihB
7 4 1 2 6 mp3an ⊢A⋅ihD⋅ℎB=D‾⁢A⋅ihB
8 5 7 eqtrdi ⊢T⁡B=D⋅ℎB→A⋅ihT⁡B=D‾⁢A⋅ihB
9 oveq1 ⊢T⁡A=C⋅ℎA→T⁡A⋅ihB=C⋅ℎA⋅ihB
10 ax-his3 ⊢C∈ℂ∧A∈ℋ∧B∈ℋ→C⋅ℎA⋅ihB=C⁢A⋅ihB
11 3 1 2 10 mp3an ⊢C⋅ℎA⋅ihB=C⁢A⋅ihB
12 9 11 eqtrdi ⊢T⁡A=C⋅ℎA→T⁡A⋅ihB=C⁢A⋅ihB
13 8 12 eqeqan12rd ⊢T⁡A=C⋅ℎA∧T⁡B=D⋅ℎB→A⋅ihT⁡B=T⁡A⋅ihB↔D‾⁢A⋅ihB=C⁢A⋅ihB
14 1 2 hicli ⊢A⋅ihB∈ℂ
15 4 cjcli ⊢D‾∈ℂ
16 mulcan2 ⊢D‾∈ℂ∧C∈ℂ∧A⋅ihB∈ℂ∧A⋅ihB≠0→D‾⁢A⋅ihB=C⁢A⋅ihB↔D‾=C
17 15 3 16 mp3an12 ⊢A⋅ihB∈ℂ∧A⋅ihB≠0→D‾⁢A⋅ihB=C⁢A⋅ihB↔D‾=C
18 14 17 mpan ⊢A⋅ihB≠0→D‾⁢A⋅ihB=C⁢A⋅ihB↔D‾=C
19 eqcom ⊢D‾=C↔C=D‾
20 18 19 bitrdi ⊢A⋅ihB≠0→D‾⁢A⋅ihB=C⁢A⋅ihB↔C=D‾
21 20 biimpcd ⊢D‾⁢A⋅ihB=C⁢A⋅ihB→A⋅ihB≠0→C=D‾
22 21 necon1d ⊢D‾⁢A⋅ihB=C⁢A⋅ihB→C≠D‾→A⋅ihB=0
23 22 com12 ⊢C≠D‾→D‾⁢A⋅ihB=C⁢A⋅ihB→A⋅ihB=0
24 oveq2 ⊢A⋅ihB=0→D‾⁢A⋅ihB=D‾⋅0
25 oveq2 ⊢A⋅ihB=0→C⁢A⋅ihB=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⋅ihB=0→C⁢A⋅ihB=D‾⋅0
30 24 29 eqtr4d ⊢A⋅ihB=0→D‾⁢A⋅ihB=C⁢A⋅ihB
31 23 30 impbid1 ⊢C≠D‾→D‾⁢A⋅ihB=C⁢A⋅ihB↔A⋅ihB=0
32 13 31 sylan9bb ⊢T⁡A=C⋅ℎA∧T⁡B=D⋅ℎB∧C≠D‾→A⋅ihT⁡B=T⁡A⋅ihB↔A⋅ihB=0