This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐴 ∈ ℋ
eigorthi.2 ⊢ 𝐵 ∈ ℋ
eigorthi.3 ⊢ 𝐶 ∈ ℂ
eigorthi.4 ⊢ 𝐷 ∈ ℂ
Assertion eigorthi ( ( ( ( 𝑇 ‘ 𝐴 ) = ( 𝐶 ·ℎ 𝐴 ) ∧ ( 𝑇 ‘ 𝐵 ) = ( 𝐷 ·ℎ 𝐵 ) ) ∧ 𝐶 ≠ ( ∗ ‘ 𝐷 ) ) → ( ( 𝐴 ·ih ( 𝑇 ‘ 𝐵 ) ) = ( ( 𝑇 ‘ 𝐴 ) ·ih 𝐵 ) ↔ ( 𝐴 ·ih 𝐵 ) = 0 ) )

Proof

Step Hyp Ref Expression
1 eigorthi.1 ⊢ 𝐴 ∈ ℋ
2 eigorthi.2 ⊢ 𝐵 ∈ ℋ
3 eigorthi.3 ⊢ 𝐶 ∈ ℂ
4 eigorthi.4 ⊢ 𝐷 ∈ ℂ
5 oveq2 ⊢ ( ( 𝑇 ‘ 𝐵 ) = ( 𝐷 ·ℎ 𝐵 ) → ( 𝐴 ·ih ( 𝑇 ‘ 𝐵 ) ) = ( 𝐴 ·ih ( 𝐷 ·ℎ 𝐵 ) ) )
6 his5 ⊢ ( ( 𝐷 ∈ ℂ ∧ 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 ·ih ( 𝐷 ·ℎ 𝐵 ) ) = ( ( ∗ ‘ 𝐷 ) · ( 𝐴 ·ih 𝐵 ) ) )
7 4 1 2 6 mp3an ⊢ ( 𝐴 ·ih ( 𝐷 ·ℎ 𝐵 ) ) = ( ( ∗ ‘ 𝐷 ) · ( 𝐴 ·ih 𝐵 ) )
8 5 7 eqtrdi ⊢ ( ( 𝑇 ‘ 𝐵 ) = ( 𝐷 ·ℎ 𝐵 ) → ( 𝐴 ·ih ( 𝑇 ‘ 𝐵 ) ) = ( ( ∗ ‘ 𝐷 ) · ( 𝐴 ·ih 𝐵 ) ) )
9 oveq1 ⊢ ( ( 𝑇 ‘ 𝐴 ) = ( 𝐶 ·ℎ 𝐴 ) → ( ( 𝑇 ‘ 𝐴 ) ·ih 𝐵 ) = ( ( 𝐶 ·ℎ 𝐴 ) ·ih 𝐵 ) )
10 ax-his3 ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( 𝐶 ·ℎ 𝐴 ) ·ih 𝐵 ) = ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) )
11 3 1 2 10 mp3an ⊢ ( ( 𝐶 ·ℎ 𝐴 ) ·ih 𝐵 ) = ( 𝐶 · ( 𝐴 ·ih 𝐵 ) )
12 9 11 eqtrdi ⊢ ( ( 𝑇 ‘ 𝐴 ) = ( 𝐶 ·ℎ 𝐴 ) → ( ( 𝑇 ‘ 𝐴 ) ·ih 𝐵 ) = ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) )
13 8 12 eqeqan12rd ⊢ ( ( ( 𝑇 ‘ 𝐴 ) = ( 𝐶 ·ℎ 𝐴 ) ∧ ( 𝑇 ‘ 𝐵 ) = ( 𝐷 ·ℎ 𝐵 ) ) → ( ( 𝐴 ·ih ( 𝑇 ‘ 𝐵 ) ) = ( ( 𝑇 ‘ 𝐴 ) ·ih 𝐵 ) ↔ ( ( ∗ ‘ 𝐷 ) · ( 𝐴 ·ih 𝐵 ) ) = ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) ) )
14 1 2 hicli ⊢ ( 𝐴 ·ih 𝐵 ) ∈ ℂ
15 4 cjcli ⊢ ( ∗ ‘ 𝐷 ) ∈ ℂ
16 mulcan2 ⊢ ( ( ( ∗ ‘ 𝐷 ) ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ ( ( 𝐴 ·ih 𝐵 ) ∈ ℂ ∧ ( 𝐴 ·ih 𝐵 ) ≠ 0 ) ) → ( ( ( ∗ ‘ 𝐷 ) · ( 𝐴 ·ih 𝐵 ) ) = ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) ↔ ( ∗ ‘ 𝐷 ) = 𝐶 ) )
17 15 3 16 mp3an12 ⊢ ( ( ( 𝐴 ·ih 𝐵 ) ∈ ℂ ∧ ( 𝐴 ·ih 𝐵 ) ≠ 0 ) → ( ( ( ∗ ‘ 𝐷 ) · ( 𝐴 ·ih 𝐵 ) ) = ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) ↔ ( ∗ ‘ 𝐷 ) = 𝐶 ) )
18 14 17 mpan ⊢ ( ( 𝐴 ·ih 𝐵 ) ≠ 0 → ( ( ( ∗ ‘ 𝐷 ) · ( 𝐴 ·ih 𝐵 ) ) = ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) ↔ ( ∗ ‘ 𝐷 ) = 𝐶 ) )
19 eqcom ⊢ ( ( ∗ ‘ 𝐷 ) = 𝐶 ↔ 𝐶 = ( ∗ ‘ 𝐷 ) )
20 18 19 bitrdi ⊢ ( ( 𝐴 ·ih 𝐵 ) ≠ 0 → ( ( ( ∗ ‘ 𝐷 ) · ( 𝐴 ·ih 𝐵 ) ) = ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) ↔ 𝐶 = ( ∗ ‘ 𝐷 ) ) )
21 20 biimpcd ⊢ ( ( ( ∗ ‘ 𝐷 ) · ( 𝐴 ·ih 𝐵 ) ) = ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) → ( ( 𝐴 ·ih 𝐵 ) ≠ 0 → 𝐶 = ( ∗ ‘ 𝐷 ) ) )
22 21 necon1d ⊢ ( ( ( ∗ ‘ 𝐷 ) · ( 𝐴 ·ih 𝐵 ) ) = ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) → ( 𝐶 ≠ ( ∗ ‘ 𝐷 ) → ( 𝐴 ·ih 𝐵 ) = 0 ) )
23 22 com12 ⊢ ( 𝐶 ≠ ( ∗ ‘ 𝐷 ) → ( ( ( ∗ ‘ 𝐷 ) · ( 𝐴 ·ih 𝐵 ) ) = ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) → ( 𝐴 ·ih 𝐵 ) = 0 ) )
24 oveq2 ⊢ ( ( 𝐴 ·ih 𝐵 ) = 0 → ( ( ∗ ‘ 𝐷 ) · ( 𝐴 ·ih 𝐵 ) ) = ( ( ∗ ‘ 𝐷 ) · 0 ) )
25 oveq2 ⊢ ( ( 𝐴 ·ih 𝐵 ) = 0 → ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) = ( 𝐶 · 0 ) )
26 3 mul01i ⊢ ( 𝐶 · 0 ) = 0
27 15 mul01i ⊢ ( ( ∗ ‘ 𝐷 ) · 0 ) = 0
28 26 27 eqtr4i ⊢ ( 𝐶 · 0 ) = ( ( ∗ ‘ 𝐷 ) · 0 )
29 25 28 eqtrdi ⊢ ( ( 𝐴 ·ih 𝐵 ) = 0 → ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) = ( ( ∗ ‘ 𝐷 ) · 0 ) )
30 24 29 eqtr4d ⊢ ( ( 𝐴 ·ih 𝐵 ) = 0 → ( ( ∗ ‘ 𝐷 ) · ( 𝐴 ·ih 𝐵 ) ) = ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) )
31 23 30 impbid1 ⊢ ( 𝐶 ≠ ( ∗ ‘ 𝐷 ) → ( ( ( ∗ ‘ 𝐷 ) · ( 𝐴 ·ih 𝐵 ) ) = ( 𝐶 · ( 𝐴 ·ih 𝐵 ) ) ↔ ( 𝐴 ·ih 𝐵 ) = 0 ) )
32 13 31 sylan9bb ⊢ ( ( ( ( 𝑇 ‘ 𝐴 ) = ( 𝐶 ·ℎ 𝐴 ) ∧ ( 𝑇 ‘ 𝐵 ) = ( 𝐷 ·ℎ 𝐵 ) ) ∧ 𝐶 ≠ ( ∗ ‘ 𝐷 ) ) → ( ( 𝐴 ·ih ( 𝑇 ‘ 𝐵 ) ) = ( ( 𝑇 ‘ 𝐴 ) ·ih 𝐵 ) ↔ ( 𝐴 ·ih 𝐵 ) = 0 ) )