Metamath Proof Explorer

Theorem leopsq

Description: The square of a Hermitian operator is positive. (Contributed by NM, 23-Aug-2006) (New usage is discouraged.)

Ref Expression
Assertion leopsq 
|- ( T e. HrmOp -> 0hop <_op ( T o. T ) )

Proof

Step Hyp Ref Expression
1 hmopf 
 |-  ( T e. HrmOp -> T : ~H --> ~H )
2 1 ffvelrnda 
 |-  ( ( T e. HrmOp /\ x e. ~H ) -> ( T ` x ) e. ~H )
3 hiidge0 
 |-  ( ( T ` x ) e. ~H -> 0 <_ ( ( T ` x ) .ih ( T ` x ) ) )
4 2 3 syl 
 |-  ( ( T e. HrmOp /\ x e. ~H ) -> 0 <_ ( ( T ` x ) .ih ( T ` x ) ) )
5 simpl 
 |-  ( ( T e. HrmOp /\ x e. ~H ) -> T e. HrmOp )
6 simpr 
 |-  ( ( T e. HrmOp /\ x e. ~H ) -> x e. ~H )
7 hmop 
 |-  ( ( T e. HrmOp /\ ( T ` x ) e. ~H /\ x e. ~H ) -> ( ( T ` x ) .ih ( T ` x ) ) = ( ( T ` ( T ` x ) ) .ih x ) )
8 5 2 6 7 syl3anc 
 |-  ( ( T e. HrmOp /\ x e. ~H ) -> ( ( T ` x ) .ih ( T ` x ) ) = ( ( T ` ( T ` x ) ) .ih x ) )
9 fvco3 
 |-  ( ( T : ~H --> ~H /\ x e. ~H ) -> ( ( T o. T ) ` x ) = ( T ` ( T ` x ) ) )
10 1 9 sylan 
 |-  ( ( T e. HrmOp /\ x e. ~H ) -> ( ( T o. T ) ` x ) = ( T ` ( T ` x ) ) )
11 10 oveq1d 
 |-  ( ( T e. HrmOp /\ x e. ~H ) -> ( ( ( T o. T ) ` x ) .ih x ) = ( ( T ` ( T ` x ) ) .ih x ) )
12 8 11 eqtr4d 
 |-  ( ( T e. HrmOp /\ x e. ~H ) -> ( ( T ` x ) .ih ( T ` x ) ) = ( ( ( T o. T ) ` x ) .ih x ) )
13 4 12 breqtrd 
 |-  ( ( T e. HrmOp /\ x e. ~H ) -> 0 <_ ( ( ( T o. T ) ` x ) .ih x ) )
14 13 ralrimiva 
 |-  ( T e. HrmOp -> A. x e. ~H 0 <_ ( ( ( T o. T ) ` x ) .ih x ) )
15 eqid 
 |-  ( T o. T ) = ( T o. T )
16 hmopco 
 |-  ( ( T e. HrmOp /\ T e. HrmOp /\ ( T o. T ) = ( T o. T ) ) -> ( T o. T ) e. HrmOp )
17 15 16 mp3an3 
 |-  ( ( T e. HrmOp /\ T e. HrmOp ) -> ( T o. T ) e. HrmOp )
18 17 anidms 
 |-  ( T e. HrmOp -> ( T o. T ) e. HrmOp )
19 leoppos 
 |-  ( ( T o. T ) e. HrmOp -> ( 0hop <_op ( T o. T ) <-> A. x e. ~H 0 <_ ( ( ( T o. T ) ` x ) .ih x ) ) )
20 18 19 syl 
 |-  ( T e. HrmOp -> ( 0hop <_op ( T o. T ) <-> A. x e. ~H 0 <_ ( ( ( T o. T ) ` x ) .ih x ) ) )
21 14 20 mpbird 
 |-  ( T e. HrmOp -> 0hop <_op ( T o. T ) )