Theorem leopg

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

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

Proof

Step	Hyp	Ref	Expression
1		oveq2	|- ( t = T -> ( u -op t ) = ( u -op T ) )
2	1	eleq1d	|- ( t = T -> ( ( u -op t ) e. HrmOp <-> ( u -op T ) e. HrmOp ) )
3	1	fveq1d	|- ( t = T -> ( ( u -op t ) ` x ) = ( ( u -op T ) ` x ) )
4	3	oveq1d	|- ( t = T -> ( ( ( u -op t ) ` x ) .ih x ) = ( ( ( u -op T ) ` x ) .ih x ) )
5	4	breq2d	|- ( t = T -> ( 0 <_ ( ( ( u -op t ) ` x ) .ih x ) <-> 0 <_ ( ( ( u -op T ) ` x ) .ih x ) ) )
6	5	ralbidv	|- ( t = T -> ( A. x e. ~H 0 <_ ( ( ( u -op t ) ` x ) .ih x ) <-> A. x e. ~H 0 <_ ( ( ( u -op T ) ` x ) .ih x ) ) )
7	2 6	anbi12d	|- ( t = T -> ( ( ( u -op t ) 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 ) ) ) )
8		oveq1	|- ( u = U -> ( u -op T ) = ( U -op T ) )
9	8	eleq1d	|- ( u = U -> ( ( u -op T ) e. HrmOp <-> ( U -op T ) e. HrmOp ) )
10	8	fveq1d	|- ( u = U -> ( ( u -op T ) ` x ) = ( ( U -op T ) ` x ) )
11	10	oveq1d	|- ( u = U -> ( ( ( u -op T ) ` x ) .ih x ) = ( ( ( U -op T ) ` x ) .ih x ) )
12	11	breq2d	|- ( u = U -> ( 0 <_ ( ( ( u -op T ) ` x ) .ih x ) <-> 0 <_ ( ( ( U -op T ) ` x ) .ih x ) ) )
13	12	ralbidv	|- ( u = U -> ( A. x e. ~H 0 <_ ( ( ( u -op T ) ` x ) .ih x ) <-> A. x e. ~H 0 <_ ( ( ( U -op T ) ` x ) .ih x ) ) )
14	9 13	anbi12d	|- ( u = U -> ( ( ( u -op T ) 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 ) ) ) )
15		df-leop	|- <_op = { <. t , u >. | ( ( u -op t ) e. HrmOp /\ A. x e. ~H 0 <_ ( ( ( u -op t ) ` x ) .ih x ) ) }
16	7 14 15	brabg	|- ( ( T e. A /\ U e. B ) -> ( T <_op U <-> ( ( U -op T ) e. HrmOp /\ A. x e. ~H 0 <_ ( ( ( U -op T ) ` x ) .ih x ) ) ) )