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 ๐ ) โ ๐ = ๐ ) ) |