Metamath Proof Explorer

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 ( ( ๐‘‡ โˆˆ HrmOp โˆง ๐‘ˆ โˆˆ HrmOp ) โ†’ ( ๐‘‡ โ‰คop ๐‘ˆ โ†” โˆ€ ๐‘ฅ โˆˆ โ„‹ 0 โ‰ค ( ( ( ๐‘ˆ โˆ’op ๐‘‡ ) โ€˜ ๐‘ฅ ) ยทih ๐‘ฅ ) ) )

Proof

Step Hyp Ref Expression
1 leopg โŠข ( ( ๐‘‡ โˆˆ HrmOp โˆง ๐‘ˆ โˆˆ HrmOp ) โ†’ ( ๐‘‡ โ‰คop ๐‘ˆ โ†” ( ( ๐‘ˆ โˆ’op ๐‘‡ ) โˆˆ HrmOp โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ 0 โ‰ค ( ( ( ๐‘ˆ โˆ’op ๐‘‡ ) โ€˜ ๐‘ฅ ) ยทih ๐‘ฅ ) ) ) )
2 hmopd โŠข ( ( ๐‘ˆ โˆˆ HrmOp โˆง ๐‘‡ โˆˆ HrmOp ) โ†’ ( ๐‘ˆ โˆ’op ๐‘‡ ) โˆˆ HrmOp )
3 2 ancoms โŠข ( ( ๐‘‡ โˆˆ HrmOp โˆง ๐‘ˆ โˆˆ HrmOp ) โ†’ ( ๐‘ˆ โˆ’op ๐‘‡ ) โˆˆ HrmOp )
4 3 biantrurd โŠข ( ( ๐‘‡ โˆˆ HrmOp โˆง ๐‘ˆ โˆˆ HrmOp ) โ†’ ( โˆ€ ๐‘ฅ โˆˆ โ„‹ 0 โ‰ค ( ( ( ๐‘ˆ โˆ’op ๐‘‡ ) โ€˜ ๐‘ฅ ) ยทih ๐‘ฅ ) โ†” ( ( ๐‘ˆ โˆ’op ๐‘‡ ) โˆˆ HrmOp โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ 0 โ‰ค ( ( ( ๐‘ˆ โˆ’op ๐‘‡ ) โ€˜ ๐‘ฅ ) ยทih ๐‘ฅ ) ) ) )
5 1 4 bitr4d โŠข ( ( ๐‘‡ โˆˆ HrmOp โˆง ๐‘ˆ โˆˆ HrmOp ) โ†’ ( ๐‘‡ โ‰คop ๐‘ˆ โ†” โˆ€ ๐‘ฅ โˆˆ โ„‹ 0 โ‰ค ( ( ( ๐‘ˆ โˆ’op ๐‘‡ ) โ€˜ ๐‘ฅ ) ยทih ๐‘ฅ ) ) )