eighmorth

Description: Eigenvectors of a Hermitian operator with distinct eigenvalues are orthogonal. Equation 1.31 of Hughes p. 49. (Contributed by NM, 23-Mar-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	eighmorth	$⊢ ((T \in HrmOp \land A \in eigvec (T)) \land (B \in eigvec (T) \land eigval (T) (A) \neq eigval (T) (B))) \to A \cdot_{ih} B = 0$

Proof

Step	Hyp	Ref	Expression
1		hmopf	$⊢ T \in HrmOp \to T : ℋ ⟶ ℋ$
2		eleigveccl	$⊢ (T : ℋ ⟶ ℋ \land A \in eigvec (T)) \to A \in ℋ$
3	1 2	sylan	$⊢ (T \in HrmOp \land A \in eigvec (T)) \to A \in ℋ$
4	3	adantr	$⊢ ((T \in HrmOp \land A \in eigvec (T)) \land B \in eigvec (T)) \to A \in ℋ$
5		eleigveccl	$⊢ (T : ℋ ⟶ ℋ \land B \in eigvec (T)) \to B \in ℋ$
6	1 5	sylan	$⊢ (T \in HrmOp \land B \in eigvec (T)) \to B \in ℋ$
7	6	adantlr	$⊢ ((T \in HrmOp \land A \in eigvec (T)) \land B \in eigvec (T)) \to B \in ℋ$
8	4 7	jca	$⊢ ((T \in HrmOp \land A \in eigvec (T)) \land B \in eigvec (T)) \to (A \in ℋ \land B \in ℋ)$
9		eighmre	$⊢ (T \in HrmOp \land A \in eigvec (T)) \to eigval (T) (A) \in ℝ$
10	9	recnd	$⊢ (T \in HrmOp \land A \in eigvec (T)) \to eigval (T) (A) \in ℂ$
11	10	adantr	$⊢ ((T \in HrmOp \land A \in eigvec (T)) \land B \in eigvec (T)) \to eigval (T) (A) \in ℂ$
12		eighmre	$⊢ (T \in HrmOp \land B \in eigvec (T)) \to eigval (T) (B) \in ℝ$
13	12	recnd	$⊢ (T \in HrmOp \land B \in eigvec (T)) \to eigval (T) (B) \in ℂ$
14	13	adantlr	$⊢ ((T \in HrmOp \land A \in eigvec (T)) \land B \in eigvec (T)) \to eigval (T) (B) \in ℂ$
15	11 14	jca	$⊢ ((T \in HrmOp \land A \in eigvec (T)) \land B \in eigvec (T)) \to (eigval (T) (A) \in ℂ \land eigval (T) (B) \in ℂ)$
16	8 15	jca	$⊢ ((T \in HrmOp \land A \in eigvec (T)) \land B \in eigvec (T)) \to ((A \in ℋ \land B \in ℋ) \land (eigval (T) (A) \in ℂ \land eigval (T) (B) \in ℂ))$
17	16	adantrr	$⊢ ((T \in HrmOp \land A \in eigvec (T)) \land (B \in eigvec (T) \land eigval (T) (A) \neq eigval (T) (B))) \to ((A \in ℋ \land B \in ℋ) \land (eigval (T) (A) \in ℂ \land eigval (T) (B) \in ℂ))$
18		eigvec1	$⊢ (T : ℋ ⟶ ℋ \land A \in eigvec (T)) \to (T (A) = eigval (T) (A) \cdot_{ℎ} A \land A \neq 0_{ℎ})$
19	18	simpld	$⊢ (T : ℋ ⟶ ℋ \land A \in eigvec (T)) \to T (A) = eigval (T) (A) \cdot_{ℎ} A$
20	1 19	sylan	$⊢ (T \in HrmOp \land A \in eigvec (T)) \to T (A) = eigval (T) (A) \cdot_{ℎ} A$
21	20	adantr	$⊢ ((T \in HrmOp \land A \in eigvec (T)) \land B \in eigvec (T)) \to T (A) = eigval (T) (A) \cdot_{ℎ} A$
22		eigvec1	$⊢ (T : ℋ ⟶ ℋ \land B \in eigvec (T)) \to (T (B) = eigval (T) (B) \cdot_{ℎ} B \land B \neq 0_{ℎ})$
23	22	simpld	$⊢ (T : ℋ ⟶ ℋ \land B \in eigvec (T)) \to T (B) = eigval (T) (B) \cdot_{ℎ} B$
24	1 23	sylan	$⊢ (T \in HrmOp \land B \in eigvec (T)) \to T (B) = eigval (T) (B) \cdot_{ℎ} B$
25	24	adantlr	$⊢ ((T \in HrmOp \land A \in eigvec (T)) \land B \in eigvec (T)) \to T (B) = eigval (T) (B) \cdot_{ℎ} B$
26	21 25	jca	$⊢ ((T \in HrmOp \land A \in eigvec (T)) \land B \in eigvec (T)) \to (T (A) = eigval (T) (A) \cdot_{ℎ} A \land T (B) = eigval (T) (B) \cdot_{ℎ} B)$
27	26	adantrr	$⊢ ((T \in HrmOp \land A \in eigvec (T)) \land (B \in eigvec (T) \land eigval (T) (A) \neq eigval (T) (B))) \to (T (A) = eigval (T) (A) \cdot_{ℎ} A \land T (B) = eigval (T) (B) \cdot_{ℎ} B)$
28	12	cjred	$⊢ (T \in HrmOp \land B \in eigvec (T)) \to \overline{eigval (T) (B)} = eigval (T) (B)$
29	28	neeq2d	$⊢ (T \in HrmOp \land B \in eigvec (T)) \to (eigval (T) (A) \neq \overline{eigval (T) (B)} \leftrightarrow eigval (T) (A) \neq eigval (T) (B))$
30	29	biimpar	$⊢ ((T \in HrmOp \land B \in eigvec (T)) \land eigval (T) (A) \neq eigval (T) (B)) \to eigval (T) (A) \neq \overline{eigval (T) (B)}$
31	30	anasss	$⊢ (T \in HrmOp \land (B \in eigvec (T) \land eigval (T) (A) \neq eigval (T) (B))) \to eigval (T) (A) \neq \overline{eigval (T) (B)}$
32	31	adantlr	$⊢ ((T \in HrmOp \land A \in eigvec (T)) \land (B \in eigvec (T) \land eigval (T) (A) \neq eigval (T) (B))) \to eigval (T) (A) \neq \overline{eigval (T) (B)}$
33	27 32	jca	$⊢ ((T \in HrmOp \land A \in eigvec (T)) \land (B \in eigvec (T) \land eigval (T) (A) \neq eigval (T) (B))) \to ((T (A) = eigval (T) (A) \cdot_{ℎ} A \land T (B) = eigval (T) (B) \cdot_{ℎ} B) \land eigval (T) (A) \neq \overline{eigval (T) (B)})$
34		simpll	$⊢ ((T \in HrmOp \land A \in eigvec (T)) \land B \in eigvec (T)) \to T \in HrmOp$
35		hmop	$⊢ (T \in HrmOp \land A \in ℋ \land B \in ℋ) \to A \cdot_{ih} T (B) = T (A) \cdot_{ih} B$
36	34 4 7 35	syl3anc	$⊢ ((T \in HrmOp \land A \in eigvec (T)) \land B \in eigvec (T)) \to A \cdot_{ih} T (B) = T (A) \cdot_{ih} B$
37	36	adantrr	$⊢ ((T \in HrmOp \land A \in eigvec (T)) \land (B \in eigvec (T) \land eigval (T) (A) \neq eigval (T) (B))) \to A \cdot_{ih} T (B) = T (A) \cdot_{ih} B$
38		eigorth	$⊢ (((A \in ℋ \land B \in ℋ) \land (eigval (T) (A) \in ℂ \land eigval (T) (B) \in ℂ)) \land ((T (A) = eigval (T) (A) \cdot_{ℎ} A \land T (B) = eigval (T) (B) \cdot_{ℎ} B) \land eigval (T) (A) \neq \overline{eigval (T) (B)})) \to (A \cdot_{ih} T (B) = T (A) \cdot_{ih} B \leftrightarrow A \cdot_{ih} B = 0)$
39	38	biimpa	$⊢ ((((A \in ℋ \land B \in ℋ) \land (eigval (T) (A) \in ℂ \land eigval (T) (B) \in ℂ)) \land ((T (A) = eigval (T) (A) \cdot_{ℎ} A \land T (B) = eigval (T) (B) \cdot_{ℎ} B) \land eigval (T) (A) \neq \overline{eigval (T) (B)})) \land A \cdot_{ih} T (B) = T (A) \cdot_{ih} B) \to A \cdot_{ih} B = 0$
40	17 33 37 39	syl21anc	$⊢ ((T \in HrmOp \land A \in eigvec (T)) \land (B \in eigvec (T) \land eigval (T) (A) \neq eigval (T) (B))) \to A \cdot_{ih} B = 0$

Metamath Proof Explorer

Theorem eighmorth

Proof