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 ) )