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	⊢ 𝐴 ∈ ℋ
	eigpos.2	⊢ 𝐵 ∈ ℂ
Assertion	eigposi	⊢ ( ( ( ( 𝐴 ·ih ( 𝑇 ‘ 𝐴 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐴 ·ih ( 𝑇 ‘ 𝐴 ) ) ) ∧ ( ( 𝑇 ‘ 𝐴 ) = ( 𝐵 ·ℎ 𝐴 ) ∧ 𝐴 ≠ 0ℎ ) ) → ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) )

Proof

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