Step | Hyp | Ref
| Expression |
1 | | hmopf 31127 |
. . . 4
โข (๐ โ HrmOp โ ๐: โโถ
โ) |
2 | | hmopf 31127 |
. . . 4
โข (๐ โ HrmOp โ ๐: โโถ
โ) |
3 | | fco 6742 |
. . . 4
โข ((๐: โโถ โ โง
๐: โโถ โ)
โ (๐ โ ๐): โโถ
โ) |
4 | 1, 2, 3 | syl2an 597 |
. . 3
โข ((๐ โ HrmOp โง ๐ โ HrmOp) โ (๐ โ ๐): โโถ โ) |
5 | 4 | 3adant3 1133 |
. 2
โข ((๐ โ HrmOp โง ๐ โ HrmOp โง (๐ โ ๐) = (๐ โ ๐)) โ (๐ โ ๐): โโถ โ) |
6 | | fvco3 6991 |
. . . . . . . . . 10
โข ((๐: โโถ โ โง
๐ฆ โ โ) โ
((๐ โ ๐)โ๐ฆ) = (๐โ(๐โ๐ฆ))) |
7 | 2, 6 | sylan 581 |
. . . . . . . . 9
โข ((๐ โ HrmOp โง ๐ฆ โ โ) โ ((๐ โ ๐)โ๐ฆ) = (๐โ(๐โ๐ฆ))) |
8 | 7 | oveq2d 7425 |
. . . . . . . 8
โข ((๐ โ HrmOp โง ๐ฆ โ โ) โ (๐ฅ
ยทih ((๐ โ ๐)โ๐ฆ)) = (๐ฅ ยทih (๐โ(๐โ๐ฆ)))) |
9 | 8 | ad2ant2l 745 |
. . . . . . 7
โข (((๐ โ HrmOp โง ๐ โ HrmOp) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ (๐ฅ
ยทih ((๐ โ ๐)โ๐ฆ)) = (๐ฅ ยทih (๐โ(๐โ๐ฆ)))) |
10 | | simpll 766 |
. . . . . . . 8
โข (((๐ โ HrmOp โง ๐ โ HrmOp) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ ๐ โ HrmOp) |
11 | | simprl 770 |
. . . . . . . 8
โข (((๐ โ HrmOp โง ๐ โ HrmOp) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ ๐ฅ โ
โ) |
12 | 2 | ffvelcdmda 7087 |
. . . . . . . . 9
โข ((๐ โ HrmOp โง ๐ฆ โ โ) โ (๐โ๐ฆ) โ โ) |
13 | 12 | ad2ant2l 745 |
. . . . . . . 8
โข (((๐ โ HrmOp โง ๐ โ HrmOp) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ (๐โ๐ฆ) โ โ) |
14 | | hmop 31175 |
. . . . . . . 8
โข ((๐ โ HrmOp โง ๐ฅ โ โ โง (๐โ๐ฆ) โ โ) โ (๐ฅ ยทih (๐โ(๐โ๐ฆ))) = ((๐โ๐ฅ) ยทih (๐โ๐ฆ))) |
15 | 10, 11, 13, 14 | syl3anc 1372 |
. . . . . . 7
โข (((๐ โ HrmOp โง ๐ โ HrmOp) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ (๐ฅ
ยทih (๐โ(๐โ๐ฆ))) = ((๐โ๐ฅ) ยทih (๐โ๐ฆ))) |
16 | | simplr 768 |
. . . . . . . 8
โข (((๐ โ HrmOp โง ๐ โ HrmOp) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ ๐ โ HrmOp) |
17 | 1 | ffvelcdmda 7087 |
. . . . . . . . 9
โข ((๐ โ HrmOp โง ๐ฅ โ โ) โ (๐โ๐ฅ) โ โ) |
18 | 17 | ad2ant2r 746 |
. . . . . . . 8
โข (((๐ โ HrmOp โง ๐ โ HrmOp) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ (๐โ๐ฅ) โ โ) |
19 | | simprr 772 |
. . . . . . . 8
โข (((๐ โ HrmOp โง ๐ โ HrmOp) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ ๐ฆ โ
โ) |
20 | | hmop 31175 |
. . . . . . . 8
โข ((๐ โ HrmOp โง (๐โ๐ฅ) โ โ โง ๐ฆ โ โ) โ ((๐โ๐ฅ) ยทih (๐โ๐ฆ)) = ((๐โ(๐โ๐ฅ)) ยทih ๐ฆ)) |
21 | 16, 18, 19, 20 | syl3anc 1372 |
. . . . . . 7
โข (((๐ โ HrmOp โง ๐ โ HrmOp) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ ((๐โ๐ฅ) ยทih (๐โ๐ฆ)) = ((๐โ(๐โ๐ฅ)) ยทih ๐ฆ)) |
22 | 9, 15, 21 | 3eqtrd 2777 |
. . . . . 6
โข (((๐ โ HrmOp โง ๐ โ HrmOp) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ (๐ฅ
ยทih ((๐ โ ๐)โ๐ฆ)) = ((๐โ(๐โ๐ฅ)) ยทih ๐ฆ)) |
23 | | fvco3 6991 |
. . . . . . . . 9
โข ((๐: โโถ โ โง
๐ฅ โ โ) โ
((๐ โ ๐)โ๐ฅ) = (๐โ(๐โ๐ฅ))) |
24 | 1, 23 | sylan 581 |
. . . . . . . 8
โข ((๐ โ HrmOp โง ๐ฅ โ โ) โ ((๐ โ ๐)โ๐ฅ) = (๐โ(๐โ๐ฅ))) |
25 | 24 | oveq1d 7424 |
. . . . . . 7
โข ((๐ โ HrmOp โง ๐ฅ โ โ) โ (((๐ โ ๐)โ๐ฅ) ยทih ๐ฆ) = ((๐โ(๐โ๐ฅ)) ยทih ๐ฆ)) |
26 | 25 | ad2ant2r 746 |
. . . . . 6
โข (((๐ โ HrmOp โง ๐ โ HrmOp) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ
(((๐ โ ๐)โ๐ฅ) ยทih ๐ฆ) = ((๐โ(๐โ๐ฅ)) ยทih ๐ฆ)) |
27 | 22, 26 | eqtr4d 2776 |
. . . . 5
โข (((๐ โ HrmOp โง ๐ โ HrmOp) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ (๐ฅ
ยทih ((๐ โ ๐)โ๐ฆ)) = (((๐ โ ๐)โ๐ฅ) ยทih ๐ฆ)) |
28 | 27 | 3adantl3 1169 |
. . . 4
โข (((๐ โ HrmOp โง ๐ โ HrmOp โง (๐ โ ๐) = (๐ โ ๐)) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ (๐ฅ ยทih ((๐ โ ๐)โ๐ฆ)) = (((๐ โ ๐)โ๐ฅ) ยทih ๐ฆ)) |
29 | | fveq1 6891 |
. . . . . . 7
โข ((๐ โ ๐) = (๐ โ ๐) โ ((๐ โ ๐)โ๐ฅ) = ((๐ โ ๐)โ๐ฅ)) |
30 | 29 | oveq1d 7424 |
. . . . . 6
โข ((๐ โ ๐) = (๐ โ ๐) โ (((๐ โ ๐)โ๐ฅ) ยทih ๐ฆ) = (((๐ โ ๐)โ๐ฅ) ยทih ๐ฆ)) |
31 | 30 | 3ad2ant3 1136 |
. . . . 5
โข ((๐ โ HrmOp โง ๐ โ HrmOp โง (๐ โ ๐) = (๐ โ ๐)) โ (((๐ โ ๐)โ๐ฅ) ยทih ๐ฆ) = (((๐ โ ๐)โ๐ฅ) ยทih ๐ฆ)) |
32 | 31 | adantr 482 |
. . . 4
โข (((๐ โ HrmOp โง ๐ โ HrmOp โง (๐ โ ๐) = (๐ โ ๐)) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ (((๐ โ ๐)โ๐ฅ) ยทih ๐ฆ) = (((๐ โ ๐)โ๐ฅ) ยทih ๐ฆ)) |
33 | 28, 32 | eqtr4d 2776 |
. . 3
โข (((๐ โ HrmOp โง ๐ โ HrmOp โง (๐ โ ๐) = (๐ โ ๐)) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ (๐ฅ ยทih ((๐ โ ๐)โ๐ฆ)) = (((๐ โ ๐)โ๐ฅ) ยทih ๐ฆ)) |
34 | 33 | ralrimivva 3201 |
. 2
โข ((๐ โ HrmOp โง ๐ โ HrmOp โง (๐ โ ๐) = (๐ โ ๐)) โ โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ ยทih ((๐ โ ๐)โ๐ฆ)) = (((๐ โ ๐)โ๐ฅ) ยทih ๐ฆ)) |
35 | | elhmop 31126 |
. 2
โข ((๐ โ ๐) โ HrmOp โ ((๐ โ ๐): โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
(๐ฅ
ยทih ((๐ โ ๐)โ๐ฆ)) = (((๐ โ ๐)โ๐ฅ) ยทih ๐ฆ))) |
36 | 5, 34, 35 | sylanbrc 584 |
1
โข ((๐ โ HrmOp โง ๐ โ HrmOp โง (๐ โ ๐) = (๐ โ ๐)) โ (๐ โ ๐) โ HrmOp) |