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 e. ~H
eigpos.2 
|- B e. CC
Assertion eigposi 
|- ( ( ( ( A .ih ( T ` A ) ) e. RR /\ 0 <_ ( A .ih ( T ` A ) ) ) /\ ( ( T ` A ) = ( B .h A ) /\ A =/= 0h ) ) -> ( B e. RR /\ 0 <_ B ) )

Proof

Step Hyp Ref Expression
1 eigpos.1 
 |-  A e. ~H
2 eigpos.2 
 |-  B e. CC
3 oveq2 
 |-  ( ( T ` A ) = ( B .h A ) -> ( A .ih ( T ` A ) ) = ( A .ih ( B .h A ) ) )
4 3 eleq1d 
 |-  ( ( T ` A ) = ( B .h A ) -> ( ( A .ih ( T ` A ) ) e. RR <-> ( A .ih ( B .h A ) ) e. RR ) )
5 2 1 hvmulcli 
 |-  ( B .h A ) e. ~H
6 hire 
 |-  ( ( A e. ~H /\ ( B .h A ) e. ~H ) -> ( ( A .ih ( B .h A ) ) e. RR <-> ( A .ih ( B .h A ) ) = ( ( B .h A ) .ih A ) ) )
7 1 5 6 mp2an 
 |-  ( ( A .ih ( B .h A ) ) e. RR <-> ( A .ih ( B .h A ) ) = ( ( B .h A ) .ih A ) )
8 oveq1 
 |-  ( ( T ` A ) = ( B .h A ) -> ( ( T ` A ) .ih A ) = ( ( B .h A ) .ih A ) )
9 3 8 eqeq12d 
 |-  ( ( T ` A ) = ( B .h A ) -> ( ( A .ih ( T ` A ) ) = ( ( T ` A ) .ih A ) <-> ( A .ih ( B .h A ) ) = ( ( B .h A ) .ih A ) ) )
10 7 9 bitr4id 
 |-  ( ( T ` A ) = ( B .h A ) -> ( ( A .ih ( B .h A ) ) e. RR <-> ( A .ih ( T ` A ) ) = ( ( T ` A ) .ih A ) ) )
11 4 10 bitrd 
 |-  ( ( T ` A ) = ( B .h A ) -> ( ( A .ih ( T ` A ) ) e. RR <-> ( A .ih ( T ` A ) ) = ( ( T ` A ) .ih A ) ) )
12 11 adantr 
 |-  ( ( ( T ` A ) = ( B .h A ) /\ A =/= 0h ) -> ( ( A .ih ( T ` A ) ) e. RR <-> ( A .ih ( T ` A ) ) = ( ( T ` A ) .ih A ) ) )
13 1 2 eigrei 
 |-  ( ( ( T ` A ) = ( B .h A ) /\ A =/= 0h ) -> ( ( A .ih ( T ` A ) ) = ( ( T ` A ) .ih A ) <-> B e. RR ) )
14 12 13 bitrd 
 |-  ( ( ( T ` A ) = ( B .h A ) /\ A =/= 0h ) -> ( ( A .ih ( T ` A ) ) e. RR <-> B e. RR ) )
15 14 biimpac 
 |-  ( ( ( A .ih ( T ` A ) ) e. RR /\ ( ( T ` A ) = ( B .h A ) /\ A =/= 0h ) ) -> B e. RR )
16 15 adantlr 
 |-  ( ( ( ( A .ih ( T ` A ) ) e. RR /\ 0 <_ ( A .ih ( T ` A ) ) ) /\ ( ( T ` A ) = ( B .h A ) /\ A =/= 0h ) ) -> B e. RR )
17 hiidrcl 
 |-  ( A e. ~H -> ( A .ih A ) e. RR )
18 1 17 mp1i 
 |-  ( ( ( ( A .ih ( T ` A ) ) e. RR /\ 0 <_ ( A .ih ( T ` A ) ) ) /\ ( ( T ` A ) = ( B .h A ) /\ A =/= 0h ) ) -> ( A .ih A ) e. RR )
19 ax-his4 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> 0 < ( A .ih A ) )
20 1 19 mpan 
 |-  ( A =/= 0h -> 0 < ( A .ih A ) )
21 20 ad2antll 
 |-  ( ( ( ( A .ih ( T ` A ) ) e. RR /\ 0 <_ ( A .ih ( T ` A ) ) ) /\ ( ( T ` A ) = ( B .h A ) /\ A =/= 0h ) ) -> 0 < ( A .ih A ) )
22 18 21 elrpd 
 |-  ( ( ( ( A .ih ( T ` A ) ) e. RR /\ 0 <_ ( A .ih ( T ` A ) ) ) /\ ( ( T ` A ) = ( B .h A ) /\ A =/= 0h ) ) -> ( A .ih A ) e. RR+ )
23 simplr 
 |-  ( ( ( ( A .ih ( T ` A ) ) e. RR /\ 0 <_ ( A .ih ( T ` A ) ) ) /\ ( ( T ` A ) = ( B .h A ) /\ A =/= 0h ) ) -> 0 <_ ( A .ih ( T ` A ) ) )
24 3 ad2antrl 
 |-  ( ( ( ( A .ih ( T ` A ) ) e. RR /\ 0 <_ ( A .ih ( T ` A ) ) ) /\ ( ( T ` A ) = ( B .h A ) /\ A =/= 0h ) ) -> ( A .ih ( T ` A ) ) = ( A .ih ( B .h A ) ) )
25 his5 
 |-  ( ( B e. CC /\ A e. ~H /\ A e. ~H ) -> ( A .ih ( B .h A ) ) = ( ( * ` B ) x. ( A .ih A ) ) )
26 2 1 1 25 mp3an 
 |-  ( A .ih ( B .h A ) ) = ( ( * ` B ) x. ( A .ih A ) )
27 16 cjred 
 |-  ( ( ( ( A .ih ( T ` A ) ) e. RR /\ 0 <_ ( A .ih ( T ` A ) ) ) /\ ( ( T ` A ) = ( B .h A ) /\ A =/= 0h ) ) -> ( * ` B ) = B )
28 27 oveq1d 
 |-  ( ( ( ( A .ih ( T ` A ) ) e. RR /\ 0 <_ ( A .ih ( T ` A ) ) ) /\ ( ( T ` A ) = ( B .h A ) /\ A =/= 0h ) ) -> ( ( * ` B ) x. ( A .ih A ) ) = ( B x. ( A .ih A ) ) )
29 26 28 eqtrid 
 |-  ( ( ( ( A .ih ( T ` A ) ) e. RR /\ 0 <_ ( A .ih ( T ` A ) ) ) /\ ( ( T ` A ) = ( B .h A ) /\ A =/= 0h ) ) -> ( A .ih ( B .h A ) ) = ( B x. ( A .ih A ) ) )
30 24 29 eqtrd 
 |-  ( ( ( ( A .ih ( T ` A ) ) e. RR /\ 0 <_ ( A .ih ( T ` A ) ) ) /\ ( ( T ` A ) = ( B .h A ) /\ A =/= 0h ) ) -> ( A .ih ( T ` A ) ) = ( B x. ( A .ih A ) ) )
31 23 30 breqtrd 
 |-  ( ( ( ( A .ih ( T ` A ) ) e. RR /\ 0 <_ ( A .ih ( T ` A ) ) ) /\ ( ( T ` A ) = ( B .h A ) /\ A =/= 0h ) ) -> 0 <_ ( B x. ( A .ih A ) ) )
32 16 22 31 prodge0ld 
 |-  ( ( ( ( A .ih ( T ` A ) ) e. RR /\ 0 <_ ( A .ih ( T ` A ) ) ) /\ ( ( T ` A ) = ( B .h A ) /\ A =/= 0h ) ) -> 0 <_ B )
33 16 32 jca 
 |-  ( ( ( ( A .ih ( T ` A ) ) e. RR /\ 0 <_ ( A .ih ( T ` A ) ) ) /\ ( ( T ` A ) = ( B .h A ) /\ A =/= 0h ) ) -> ( B e. RR /\ 0 <_ B ) )