Theorem leop

Description: Ordering relation for operators. Definition of positive operator ordering in Kreyszig p. 470. (Contributed by NM, 23-Jul-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	leop	|- ( ( T e. HrmOp /\ U e. HrmOp ) -> ( T <_op U <-> A. x e. ~H 0 <_ ( ( ( U -op T ) ` x ) .ih x ) ) )

Proof

Step	Hyp	Ref	Expression
1		leopg	|- ( ( T e. HrmOp /\ U e. HrmOp ) -> ( T <_op U <-> ( ( U -op T ) e. HrmOp /\ A. x e. ~H 0 <_ ( ( ( U -op T ) ` x ) .ih x ) ) ) )
2		hmopd	|- ( ( U e. HrmOp /\ T e. HrmOp ) -> ( U -op T ) e. HrmOp )
3	2	ancoms	|- ( ( T e. HrmOp /\ U e. HrmOp ) -> ( U -op T ) e. HrmOp )
4	3	biantrurd	|- ( ( T e. HrmOp /\ U e. HrmOp ) -> ( A. x e. ~H 0 <_ ( ( ( U -op T ) ` x ) .ih x ) <-> ( ( U -op T ) e. HrmOp /\ A. x e. ~H 0 <_ ( ( ( U -op T ) ` x ) .ih x ) ) ) )
5	1 4	bitr4d	|- ( ( T e. HrmOp /\ U e. HrmOp ) -> ( T <_op U <-> A. x e. ~H 0 <_ ( ( ( U -op T ) ` x ) .ih x ) ) )