Step | Hyp | Ref
| Expression |
1 | | oveq2 7312 |
. . . 4
โข (๐ก = ๐ โ (๐ข โop ๐ก) = (๐ข โop ๐)) |
2 | 1 | eleq1d 2821 |
. . 3
โข (๐ก = ๐ โ ((๐ข โop ๐ก) โ HrmOp โ (๐ข โop ๐) โ HrmOp)) |
3 | 1 | fveq1d 6803 |
. . . . . 6
โข (๐ก = ๐ โ ((๐ข โop ๐ก)โ๐ฅ) = ((๐ข โop ๐)โ๐ฅ)) |
4 | 3 | oveq1d 7319 |
. . . . 5
โข (๐ก = ๐ โ (((๐ข โop ๐ก)โ๐ฅ) ยทih ๐ฅ) = (((๐ข โop ๐)โ๐ฅ) ยทih ๐ฅ)) |
5 | 4 | breq2d 5094 |
. . . 4
โข (๐ก = ๐ โ (0 โค (((๐ข โop ๐ก)โ๐ฅ) ยทih ๐ฅ) โ 0 โค (((๐ข โop ๐)โ๐ฅ) ยทih ๐ฅ))) |
6 | 5 | ralbidv 3171 |
. . 3
โข (๐ก = ๐ โ (โ๐ฅ โ โ 0 โค (((๐ข โop ๐ก)โ๐ฅ) ยทih ๐ฅ) โ โ๐ฅ โ โ 0 โค (((๐ข โop ๐)โ๐ฅ) ยทih ๐ฅ))) |
7 | 2, 6 | anbi12d 632 |
. 2
โข (๐ก = ๐ โ (((๐ข โop ๐ก) โ HrmOp โง โ๐ฅ โ โ 0 โค (((๐ข โop ๐ก)โ๐ฅ) ยทih ๐ฅ)) โ ((๐ข โop ๐) โ HrmOp โง โ๐ฅ โ โ 0 โค (((๐ข โop ๐)โ๐ฅ) ยทih ๐ฅ)))) |
8 | | oveq1 7311 |
. . . 4
โข (๐ข = ๐ โ (๐ข โop ๐) = (๐ โop ๐)) |
9 | 8 | eleq1d 2821 |
. . 3
โข (๐ข = ๐ โ ((๐ข โop ๐) โ HrmOp โ (๐ โop ๐) โ HrmOp)) |
10 | 8 | fveq1d 6803 |
. . . . . 6
โข (๐ข = ๐ โ ((๐ข โop ๐)โ๐ฅ) = ((๐ โop ๐)โ๐ฅ)) |
11 | 10 | oveq1d 7319 |
. . . . 5
โข (๐ข = ๐ โ (((๐ข โop ๐)โ๐ฅ) ยทih ๐ฅ) = (((๐ โop ๐)โ๐ฅ) ยทih ๐ฅ)) |
12 | 11 | breq2d 5094 |
. . . 4
โข (๐ข = ๐ โ (0 โค (((๐ข โop ๐)โ๐ฅ) ยทih ๐ฅ) โ 0 โค (((๐ โop ๐)โ๐ฅ) ยทih ๐ฅ))) |
13 | 12 | ralbidv 3171 |
. . 3
โข (๐ข = ๐ โ (โ๐ฅ โ โ 0 โค (((๐ข โop ๐)โ๐ฅ) ยทih ๐ฅ) โ โ๐ฅ โ โ 0 โค (((๐ โop ๐)โ๐ฅ) ยทih ๐ฅ))) |
14 | 9, 13 | anbi12d 632 |
. 2
โข (๐ข = ๐ โ (((๐ข โop ๐) โ HrmOp โง โ๐ฅ โ โ 0 โค (((๐ข โop ๐)โ๐ฅ) ยทih ๐ฅ)) โ ((๐ โop ๐) โ HrmOp โง โ๐ฅ โ โ 0 โค (((๐ โop ๐)โ๐ฅ) ยทih ๐ฅ)))) |
15 | | df-leop 30256 |
. 2
โข
โคop = {โจ๐ก, ๐ขโฉ โฃ ((๐ข โop ๐ก) โ HrmOp โง โ๐ฅ โ โ 0 โค (((๐ข โop ๐ก)โ๐ฅ) ยทih ๐ฅ))} |
16 | 7, 14, 15 | brabg 5462 |
1
โข ((๐ โ ๐ด โง ๐ โ ๐ต) โ (๐ โคop ๐ โ ((๐ โop ๐) โ HrmOp โง โ๐ฅ โ โ 0 โค (((๐ โop ๐)โ๐ฅ) ยทih ๐ฅ)))) |