Metamath Proof Explorer

Theorem eigposi

Description: A sufficient condition (first conjunct pair, that holds when T is a positive operator) for an eigenvalue B (second conjunct pair) to be nonnegative. Remark (ii) in Hughes p. 137. (Contributed by NM, 2-Jul-2005) (New usage is discouraged.)

Ref Expression
Hypotheses eigpos.1 ⊢ A ∈ ℋ
eigpos.2 ⊢ B ∈ ℂ
Assertion eigposi ⊢ A ⋅ ih T ⁡ A ∈ ℝ ∧ 0 ≤ A ⋅ ih T ⁡ A ∧ T ⁡ A = B ⋅ ℎ A ∧ A ≠ 0 ℎ → B ∈ ℝ ∧ 0 ≤ B

Proof

Step Hyp Ref Expression
1 eigpos.1 ⊢ A ∈ ℋ
2 eigpos.2 ⊢ B ∈ ℂ
3 oveq2 ⊢ T ⁡ A = B ⋅ ℎ A → A ⋅ ih T ⁡ A = A ⋅ ih B ⋅ ℎ A
4 3 eleq1d ⊢ T ⁡ A = B ⋅ ℎ A → A ⋅ ih T ⁡ A ∈ ℝ ↔ A ⋅ ih B ⋅ ℎ A ∈ ℝ
5 2 1 hvmulcli ⊢ B ⋅ ℎ A ∈ ℋ
6 hire ⊢ A ∈ ℋ ∧ B ⋅ ℎ A ∈ ℋ → A ⋅ ih B ⋅ ℎ A ∈ ℝ ↔ A ⋅ ih B ⋅ ℎ A = B ⋅ ℎ A ⋅ ih A
7 1 5 6 mp2an ⊢ A ⋅ ih B ⋅ ℎ A ∈ ℝ ↔ A ⋅ ih B ⋅ ℎ A = B ⋅ ℎ A ⋅ ih A
8 oveq1 ⊢ T ⁡ A = B ⋅ ℎ A → T ⁡ A ⋅ ih A = B ⋅ ℎ A ⋅ ih A
9 3 8 eqeq12d ⊢ T ⁡ A = B ⋅ ℎ A → A ⋅ ih T ⁡ A = T ⁡ A ⋅ ih A ↔ A ⋅ ih B ⋅ ℎ A = B ⋅ ℎ A ⋅ ih A
10 7 9 bitr4id ⊢ T ⁡ A = B ⋅ ℎ A → A ⋅ ih B ⋅ ℎ A ∈ ℝ ↔ A ⋅ ih T ⁡ A = T ⁡ A ⋅ ih A
11 4 10 bitrd ⊢ T ⁡ A = B ⋅ ℎ A → A ⋅ ih T ⁡ A ∈ ℝ ↔ A ⋅ ih T ⁡ A = T ⁡ A ⋅ ih A
12 11 adantr ⊢ T ⁡ A = B ⋅ ℎ A ∧ A ≠ 0 ℎ → A ⋅ ih T ⁡ A ∈ ℝ ↔ A ⋅ ih T ⁡ A = T ⁡ A ⋅ ih A
13 1 2 eigrei ⊢ T ⁡ A = B ⋅ ℎ A ∧ A ≠ 0 ℎ → A ⋅ ih T ⁡ A = T ⁡ A ⋅ ih A ↔ B ∈ ℝ
14 12 13 bitrd ⊢ T ⁡ A = B ⋅ ℎ A ∧ A ≠ 0 ℎ → A ⋅ ih T ⁡ A ∈ ℝ ↔ B ∈ ℝ
15 14 biimpac ⊢ A ⋅ ih T ⁡ A ∈ ℝ ∧ T ⁡ A = B ⋅ ℎ A ∧ A ≠ 0 ℎ → B ∈ ℝ
16 15 adantlr ⊢ A ⋅ ih T ⁡ A ∈ ℝ ∧ 0 ≤ A ⋅ ih T ⁡ A ∧ T ⁡ A = B ⋅ ℎ A ∧ A ≠ 0 ℎ → B ∈ ℝ
17 hiidrcl ⊢ A ∈ ℋ → A ⋅ ih A ∈ ℝ
18 1 17 mp1i ⊢ A ⋅ ih T ⁡ A ∈ ℝ ∧ 0 ≤ A ⋅ ih T ⁡ A ∧ T ⁡ A = B ⋅ ℎ A ∧ A ≠ 0 ℎ → A ⋅ ih A ∈ ℝ
19 ax-his4 ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → 0 < A ⋅ ih A
20 1 19 mpan ⊢ A ≠ 0 ℎ → 0 < A ⋅ ih A
21 20 ad2antll ⊢ A ⋅ ih T ⁡ A ∈ ℝ ∧ 0 ≤ A ⋅ ih T ⁡ A ∧ T ⁡ A = B ⋅ ℎ A ∧ A ≠ 0 ℎ → 0 < A ⋅ ih A
22 18 21 elrpd ⊢ A ⋅ ih T ⁡ A ∈ ℝ ∧ 0 ≤ A ⋅ ih T ⁡ A ∧ T ⁡ A = B ⋅ ℎ A ∧ A ≠ 0 ℎ → A ⋅ ih A ∈ ℝ +
23 simplr ⊢ A ⋅ ih T ⁡ A ∈ ℝ ∧ 0 ≤ A ⋅ ih T ⁡ A ∧ T ⁡ A = B ⋅ ℎ A ∧ A ≠ 0 ℎ → 0 ≤ A ⋅ ih T ⁡ A
24 3 ad2antrl ⊢ A ⋅ ih T ⁡ A ∈ ℝ ∧ 0 ≤ A ⋅ ih T ⁡ A ∧ T ⁡ A = B ⋅ ℎ A ∧ A ≠ 0 ℎ → A ⋅ ih T ⁡ A = A ⋅ ih B ⋅ ℎ A
25 his5 ⊢ B ∈ ℂ ∧ A ∈ ℋ ∧ A ∈ ℋ → A ⋅ ih B ⋅ ℎ A = B ‾ ⁢ A ⋅ ih A
26 2 1 1 25 mp3an ⊢ A ⋅ ih B ⋅ ℎ A = B ‾ ⁢ A ⋅ ih A
27 16 cjred ⊢ A ⋅ ih T ⁡ A ∈ ℝ ∧ 0 ≤ A ⋅ ih T ⁡ A ∧ T ⁡ A = B ⋅ ℎ A ∧ A ≠ 0 ℎ → B ‾ = B
28 27 oveq1d ⊢ A ⋅ ih T ⁡ A ∈ ℝ ∧ 0 ≤ A ⋅ ih T ⁡ A ∧ T ⁡ A = B ⋅ ℎ A ∧ A ≠ 0 ℎ → B ‾ ⁢ A ⋅ ih A = B ⁢ A ⋅ ih A
29 26 28 syl5eq ⊢ A ⋅ ih T ⁡ A ∈ ℝ ∧ 0 ≤ A ⋅ ih T ⁡ A ∧ T ⁡ A = B ⋅ ℎ A ∧ A ≠ 0 ℎ → A ⋅ ih B ⋅ ℎ A = B ⁢ A ⋅ ih A
30 24 29 eqtrd ⊢ A ⋅ ih T ⁡ A ∈ ℝ ∧ 0 ≤ A ⋅ ih T ⁡ A ∧ T ⁡ A = B ⋅ ℎ A ∧ A ≠ 0 ℎ → A ⋅ ih T ⁡ A = B ⁢ A ⋅ ih A
31 23 30 breqtrd ⊢ A ⋅ ih T ⁡ A ∈ ℝ ∧ 0 ≤ A ⋅ ih T ⁡ A ∧ T ⁡ A = B ⋅ ℎ A ∧ A ≠ 0 ℎ → 0 ≤ B ⁢ A ⋅ ih A
32 16 22 31 prodge0ld ⊢ A ⋅ ih T ⁡ A ∈ ℝ ∧ 0 ≤ A ⋅ ih T ⁡ A ∧ T ⁡ A = B ⋅ ℎ A ∧ A ≠ 0 ℎ → 0 ≤ B
33 16 32 jca ⊢ A ⋅ ih T ⁡ A ∈ ℝ ∧ 0 ≤ A ⋅ ih T ⁡ A ∧ T ⁡ A = B ⋅ ℎ A ∧ A ≠ 0 ℎ → B ∈ ℝ ∧ 0 ≤ B