Metamath Proof Explorer


Theorem leoptri

Description: The positive operator ordering relation satisfies trichotomy. Exercise 1(iii) of Retherford p. 49. (Contributed by NM, 25-Jul-2006) (New usage is discouraged.)

Ref Expression
Assertion leoptri ( ( ๐‘‡ โˆˆ HrmOp โˆง ๐‘ˆ โˆˆ HrmOp ) โ†’ ( ( ๐‘‡ โ‰คop ๐‘ˆ โˆง ๐‘ˆ โ‰คop ๐‘‡ ) โ†” ๐‘‡ = ๐‘ˆ ) )

Proof

Step Hyp Ref Expression
1 leop2 โŠข ( ( ๐‘‡ โˆˆ HrmOp โˆง ๐‘ˆ โˆˆ HrmOp ) โ†’ ( ๐‘‡ โ‰คop ๐‘ˆ โ†” โˆ€ ๐‘ฅ โˆˆ โ„‹ ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ๐‘ฅ ) โ‰ค ( ( ๐‘ˆ โ€˜ ๐‘ฅ ) ยทih ๐‘ฅ ) ) )
2 leop2 โŠข ( ( ๐‘ˆ โˆˆ HrmOp โˆง ๐‘‡ โˆˆ HrmOp ) โ†’ ( ๐‘ˆ โ‰คop ๐‘‡ โ†” โˆ€ ๐‘ฅ โˆˆ โ„‹ ( ( ๐‘ˆ โ€˜ ๐‘ฅ ) ยทih ๐‘ฅ ) โ‰ค ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ๐‘ฅ ) ) )
3 2 ancoms โŠข ( ( ๐‘‡ โˆˆ HrmOp โˆง ๐‘ˆ โˆˆ HrmOp ) โ†’ ( ๐‘ˆ โ‰คop ๐‘‡ โ†” โˆ€ ๐‘ฅ โˆˆ โ„‹ ( ( ๐‘ˆ โ€˜ ๐‘ฅ ) ยทih ๐‘ฅ ) โ‰ค ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ๐‘ฅ ) ) )
4 1 3 anbi12d โŠข ( ( ๐‘‡ โˆˆ HrmOp โˆง ๐‘ˆ โˆˆ HrmOp ) โ†’ ( ( ๐‘‡ โ‰คop ๐‘ˆ โˆง ๐‘ˆ โ‰คop ๐‘‡ ) โ†” ( โˆ€ ๐‘ฅ โˆˆ โ„‹ ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ๐‘ฅ ) โ‰ค ( ( ๐‘ˆ โ€˜ ๐‘ฅ ) ยทih ๐‘ฅ ) โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ ( ( ๐‘ˆ โ€˜ ๐‘ฅ ) ยทih ๐‘ฅ ) โ‰ค ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ๐‘ฅ ) ) ) )
5 hmopre โŠข ( ( ๐‘‡ โˆˆ HrmOp โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ๐‘ฅ ) โˆˆ โ„ )
6 5 adantlr โŠข ( ( ( ๐‘‡ โˆˆ HrmOp โˆง ๐‘ˆ โˆˆ HrmOp ) โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ๐‘ฅ ) โˆˆ โ„ )
7 hmopre โŠข ( ( ๐‘ˆ โˆˆ HrmOp โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ( ๐‘ˆ โ€˜ ๐‘ฅ ) ยทih ๐‘ฅ ) โˆˆ โ„ )
8 7 adantll โŠข ( ( ( ๐‘‡ โˆˆ HrmOp โˆง ๐‘ˆ โˆˆ HrmOp ) โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ( ๐‘ˆ โ€˜ ๐‘ฅ ) ยทih ๐‘ฅ ) โˆˆ โ„ )
9 6 8 letri3d โŠข ( ( ( ๐‘‡ โˆˆ HrmOp โˆง ๐‘ˆ โˆˆ HrmOp ) โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ๐‘ฅ ) = ( ( ๐‘ˆ โ€˜ ๐‘ฅ ) ยทih ๐‘ฅ ) โ†” ( ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ๐‘ฅ ) โ‰ค ( ( ๐‘ˆ โ€˜ ๐‘ฅ ) ยทih ๐‘ฅ ) โˆง ( ( ๐‘ˆ โ€˜ ๐‘ฅ ) ยทih ๐‘ฅ ) โ‰ค ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ๐‘ฅ ) ) ) )
10 9 ralbidva โŠข ( ( ๐‘‡ โˆˆ HrmOp โˆง ๐‘ˆ โˆˆ HrmOp ) โ†’ ( โˆ€ ๐‘ฅ โˆˆ โ„‹ ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ๐‘ฅ ) = ( ( ๐‘ˆ โ€˜ ๐‘ฅ ) ยทih ๐‘ฅ ) โ†” โˆ€ ๐‘ฅ โˆˆ โ„‹ ( ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ๐‘ฅ ) โ‰ค ( ( ๐‘ˆ โ€˜ ๐‘ฅ ) ยทih ๐‘ฅ ) โˆง ( ( ๐‘ˆ โ€˜ ๐‘ฅ ) ยทih ๐‘ฅ ) โ‰ค ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ๐‘ฅ ) ) ) )
11 r19.26 โŠข ( โˆ€ ๐‘ฅ โˆˆ โ„‹ ( ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ๐‘ฅ ) โ‰ค ( ( ๐‘ˆ โ€˜ ๐‘ฅ ) ยทih ๐‘ฅ ) โˆง ( ( ๐‘ˆ โ€˜ ๐‘ฅ ) ยทih ๐‘ฅ ) โ‰ค ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ๐‘ฅ ) ) โ†” ( โˆ€ ๐‘ฅ โˆˆ โ„‹ ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ๐‘ฅ ) โ‰ค ( ( ๐‘ˆ โ€˜ ๐‘ฅ ) ยทih ๐‘ฅ ) โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ ( ( ๐‘ˆ โ€˜ ๐‘ฅ ) ยทih ๐‘ฅ ) โ‰ค ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ๐‘ฅ ) ) )
12 10 11 bitr2di โŠข ( ( ๐‘‡ โˆˆ HrmOp โˆง ๐‘ˆ โˆˆ HrmOp ) โ†’ ( ( โˆ€ ๐‘ฅ โˆˆ โ„‹ ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ๐‘ฅ ) โ‰ค ( ( ๐‘ˆ โ€˜ ๐‘ฅ ) ยทih ๐‘ฅ ) โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ ( ( ๐‘ˆ โ€˜ ๐‘ฅ ) ยทih ๐‘ฅ ) โ‰ค ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ๐‘ฅ ) ) โ†” โˆ€ ๐‘ฅ โˆˆ โ„‹ ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ๐‘ฅ ) = ( ( ๐‘ˆ โ€˜ ๐‘ฅ ) ยทih ๐‘ฅ ) ) )
13 hmoplin โŠข ( ๐‘‡ โˆˆ HrmOp โ†’ ๐‘‡ โˆˆ LinOp )
14 hmoplin โŠข ( ๐‘ˆ โˆˆ HrmOp โ†’ ๐‘ˆ โˆˆ LinOp )
15 lnopeq โŠข ( ( ๐‘‡ โˆˆ LinOp โˆง ๐‘ˆ โˆˆ LinOp ) โ†’ ( โˆ€ ๐‘ฅ โˆˆ โ„‹ ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ๐‘ฅ ) = ( ( ๐‘ˆ โ€˜ ๐‘ฅ ) ยทih ๐‘ฅ ) โ†” ๐‘‡ = ๐‘ˆ ) )
16 13 14 15 syl2an โŠข ( ( ๐‘‡ โˆˆ HrmOp โˆง ๐‘ˆ โˆˆ HrmOp ) โ†’ ( โˆ€ ๐‘ฅ โˆˆ โ„‹ ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ๐‘ฅ ) = ( ( ๐‘ˆ โ€˜ ๐‘ฅ ) ยทih ๐‘ฅ ) โ†” ๐‘‡ = ๐‘ˆ ) )
17 4 12 16 3bitrd โŠข ( ( ๐‘‡ โˆˆ HrmOp โˆง ๐‘ˆ โˆˆ HrmOp ) โ†’ ( ( ๐‘‡ โ‰คop ๐‘ˆ โˆง ๐‘ˆ โ‰คop ๐‘‡ ) โ†” ๐‘‡ = ๐‘ˆ ) )