Step | Hyp | Ref
| Expression |
1 | | r19.26 3111 |
. . . 4
โข
(โ๐ฅ โ
โ (0 โค ((๐โ๐ฅ) ยทih ๐ฅ) โง 0 โค ((๐โ๐ฅ) ยทih ๐ฅ)) โ (โ๐ฅ โ โ 0 โค ((๐โ๐ฅ) ยทih ๐ฅ) โง โ๐ฅ โ โ 0 โค ((๐โ๐ฅ) ยทih ๐ฅ))) |
2 | | hmopre 30907 |
. . . . . . . 8
โข ((๐ โ HrmOp โง ๐ฅ โ โ) โ ((๐โ๐ฅ) ยทih ๐ฅ) โ
โ) |
3 | | hmopre 30907 |
. . . . . . . 8
โข ((๐ โ HrmOp โง ๐ฅ โ โ) โ ((๐โ๐ฅ) ยทih ๐ฅ) โ
โ) |
4 | | addge0 11649 |
. . . . . . . . 9
โข
(((((๐โ๐ฅ)
ยทih ๐ฅ) โ โ โง ((๐โ๐ฅ) ยทih ๐ฅ) โ โ) โง (0 โค
((๐โ๐ฅ)
ยทih ๐ฅ) โง 0 โค ((๐โ๐ฅ) ยทih ๐ฅ))) โ 0 โค (((๐โ๐ฅ) ยทih ๐ฅ) + ((๐โ๐ฅ) ยทih ๐ฅ))) |
5 | 4 | ex 414 |
. . . . . . . 8
โข ((((๐โ๐ฅ) ยทih ๐ฅ) โ โ โง ((๐โ๐ฅ) ยทih ๐ฅ) โ โ) โ ((0
โค ((๐โ๐ฅ)
ยทih ๐ฅ) โง 0 โค ((๐โ๐ฅ) ยทih ๐ฅ)) โ 0 โค (((๐โ๐ฅ) ยทih ๐ฅ) + ((๐โ๐ฅ) ยทih ๐ฅ)))) |
6 | 2, 3, 5 | syl2an 597 |
. . . . . . 7
โข (((๐ โ HrmOp โง ๐ฅ โ โ) โง (๐ โ HrmOp โง ๐ฅ โ โ)) โ ((0
โค ((๐โ๐ฅ)
ยทih ๐ฅ) โง 0 โค ((๐โ๐ฅ) ยทih ๐ฅ)) โ 0 โค (((๐โ๐ฅ) ยทih ๐ฅ) + ((๐โ๐ฅ) ยทih ๐ฅ)))) |
7 | 6 | anandirs 678 |
. . . . . 6
โข (((๐ โ HrmOp โง ๐ โ HrmOp) โง ๐ฅ โ โ) โ ((0 โค
((๐โ๐ฅ)
ยทih ๐ฅ) โง 0 โค ((๐โ๐ฅ) ยทih ๐ฅ)) โ 0 โค (((๐โ๐ฅ) ยทih ๐ฅ) + ((๐โ๐ฅ) ยทih ๐ฅ)))) |
8 | | hmopf 30858 |
. . . . . . . . 9
โข (๐ โ HrmOp โ ๐: โโถ
โ) |
9 | | hmopf 30858 |
. . . . . . . . 9
โข (๐ โ HrmOp โ ๐: โโถ
โ) |
10 | 8, 9 | anim12i 614 |
. . . . . . . 8
โข ((๐ โ HrmOp โง ๐ โ HrmOp) โ (๐: โโถ โ โง
๐: โโถ
โ)) |
11 | | hosval 30724 |
. . . . . . . . . . 11
โข ((๐: โโถ โ โง
๐: โโถ โ
โง ๐ฅ โ โ)
โ ((๐ +op
๐)โ๐ฅ) = ((๐โ๐ฅ) +โ (๐โ๐ฅ))) |
12 | 11 | oveq1d 7373 |
. . . . . . . . . 10
โข ((๐: โโถ โ โง
๐: โโถ โ
โง ๐ฅ โ โ)
โ (((๐ +op
๐)โ๐ฅ) ยทih ๐ฅ) = (((๐โ๐ฅ) +โ (๐โ๐ฅ)) ยทih ๐ฅ)) |
13 | 12 | 3expa 1119 |
. . . . . . . . 9
โข (((๐: โโถ โ โง
๐: โโถ โ)
โง ๐ฅ โ โ)
โ (((๐ +op
๐)โ๐ฅ) ยทih ๐ฅ) = (((๐โ๐ฅ) +โ (๐โ๐ฅ)) ยทih ๐ฅ)) |
14 | | ffvelcdm 7033 |
. . . . . . . . . . 11
โข ((๐: โโถ โ โง
๐ฅ โ โ) โ
(๐โ๐ฅ) โ โ) |
15 | 14 | adantlr 714 |
. . . . . . . . . 10
โข (((๐: โโถ โ โง
๐: โโถ โ)
โง ๐ฅ โ โ)
โ (๐โ๐ฅ) โ
โ) |
16 | | ffvelcdm 7033 |
. . . . . . . . . . 11
โข ((๐: โโถ โ โง
๐ฅ โ โ) โ
(๐โ๐ฅ) โ โ) |
17 | 16 | adantll 713 |
. . . . . . . . . 10
โข (((๐: โโถ โ โง
๐: โโถ โ)
โง ๐ฅ โ โ)
โ (๐โ๐ฅ) โ
โ) |
18 | | simpr 486 |
. . . . . . . . . 10
โข (((๐: โโถ โ โง
๐: โโถ โ)
โง ๐ฅ โ โ)
โ ๐ฅ โ
โ) |
19 | | ax-his2 30067 |
. . . . . . . . . 10
โข (((๐โ๐ฅ) โ โ โง (๐โ๐ฅ) โ โ โง ๐ฅ โ โ) โ (((๐โ๐ฅ) +โ (๐โ๐ฅ)) ยทih ๐ฅ) = (((๐โ๐ฅ) ยทih ๐ฅ) + ((๐โ๐ฅ) ยทih ๐ฅ))) |
20 | 15, 17, 18, 19 | syl3anc 1372 |
. . . . . . . . 9
โข (((๐: โโถ โ โง
๐: โโถ โ)
โง ๐ฅ โ โ)
โ (((๐โ๐ฅ) +โ (๐โ๐ฅ)) ยทih ๐ฅ) = (((๐โ๐ฅ) ยทih ๐ฅ) + ((๐โ๐ฅ) ยทih ๐ฅ))) |
21 | 13, 20 | eqtrd 2773 |
. . . . . . . 8
โข (((๐: โโถ โ โง
๐: โโถ โ)
โง ๐ฅ โ โ)
โ (((๐ +op
๐)โ๐ฅ) ยทih ๐ฅ) = (((๐โ๐ฅ) ยทih ๐ฅ) + ((๐โ๐ฅ) ยทih ๐ฅ))) |
22 | 10, 21 | sylan 581 |
. . . . . . 7
โข (((๐ โ HrmOp โง ๐ โ HrmOp) โง ๐ฅ โ โ) โ (((๐ +op ๐)โ๐ฅ) ยทih ๐ฅ) = (((๐โ๐ฅ) ยทih ๐ฅ) + ((๐โ๐ฅ) ยทih ๐ฅ))) |
23 | 22 | breq2d 5118 |
. . . . . 6
โข (((๐ โ HrmOp โง ๐ โ HrmOp) โง ๐ฅ โ โ) โ (0 โค
(((๐ +op ๐)โ๐ฅ) ยทih ๐ฅ) โ 0 โค (((๐โ๐ฅ) ยทih ๐ฅ) + ((๐โ๐ฅ) ยทih ๐ฅ)))) |
24 | 7, 23 | sylibrd 259 |
. . . . 5
โข (((๐ โ HrmOp โง ๐ โ HrmOp) โง ๐ฅ โ โ) โ ((0 โค
((๐โ๐ฅ)
ยทih ๐ฅ) โง 0 โค ((๐โ๐ฅ) ยทih ๐ฅ)) โ 0 โค (((๐ +op ๐)โ๐ฅ) ยทih ๐ฅ))) |
25 | 24 | ralimdva 3161 |
. . . 4
โข ((๐ โ HrmOp โง ๐ โ HrmOp) โ
(โ๐ฅ โ โ
(0 โค ((๐โ๐ฅ)
ยทih ๐ฅ) โง 0 โค ((๐โ๐ฅ) ยทih ๐ฅ)) โ โ๐ฅ โ โ 0 โค (((๐ +op ๐)โ๐ฅ) ยทih ๐ฅ))) |
26 | 1, 25 | biimtrrid 242 |
. . 3
โข ((๐ โ HrmOp โง ๐ โ HrmOp) โ
((โ๐ฅ โ โ
0 โค ((๐โ๐ฅ)
ยทih ๐ฅ) โง โ๐ฅ โ โ 0 โค ((๐โ๐ฅ) ยทih ๐ฅ)) โ โ๐ฅ โ โ 0 โค (((๐ +op ๐)โ๐ฅ) ยทih ๐ฅ))) |
27 | | leoppos 31110 |
. . . 4
โข (๐ โ HrmOp โ (
0hop โคop ๐ โ โ๐ฅ โ โ 0 โค ((๐โ๐ฅ) ยทih ๐ฅ))) |
28 | | leoppos 31110 |
. . . 4
โข (๐ โ HrmOp โ (
0hop โคop ๐ โ โ๐ฅ โ โ 0 โค ((๐โ๐ฅ) ยทih ๐ฅ))) |
29 | 27, 28 | bi2anan9 638 |
. . 3
โข ((๐ โ HrmOp โง ๐ โ HrmOp) โ ((
0hop โคop ๐ โง 0hop โคop
๐) โ (โ๐ฅ โ โ 0 โค ((๐โ๐ฅ) ยทih ๐ฅ) โง โ๐ฅ โ โ 0 โค ((๐โ๐ฅ) ยทih ๐ฅ)))) |
30 | | hmops 31004 |
. . . 4
โข ((๐ โ HrmOp โง ๐ โ HrmOp) โ (๐ +op ๐) โ HrmOp) |
31 | | leoppos 31110 |
. . . 4
โข ((๐ +op ๐) โ HrmOp โ (
0hop โคop (๐ +op ๐) โ โ๐ฅ โ โ 0 โค (((๐ +op ๐)โ๐ฅ) ยทih ๐ฅ))) |
32 | 30, 31 | syl 17 |
. . 3
โข ((๐ โ HrmOp โง ๐ โ HrmOp) โ (
0hop โคop (๐ +op ๐) โ โ๐ฅ โ โ 0 โค (((๐ +op ๐)โ๐ฅ) ยทih ๐ฅ))) |
33 | 26, 29, 32 | 3imtr4d 294 |
. 2
โข ((๐ โ HrmOp โง ๐ โ HrmOp) โ ((
0hop โคop ๐ โง 0hop โคop
๐) โ 0hop
โคop (๐
+op ๐))) |
34 | 33 | imp 408 |
1
โข (((๐ โ HrmOp โง ๐ โ HrmOp) โง (
0hop โคop ๐ โง 0hop โคop
๐)) โ 0hop
โคop (๐
+op ๐)) |