Step | Hyp | Ref
| Expression |
1 | | elhmop 31113 |
. . . 4
โข (๐ โ HrmOp โ (๐: โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
(๐ฅ
ยทih (๐โ๐ฆ)) = ((๐โ๐ฅ) ยทih ๐ฆ))) |
2 | 1 | simprbi 497 |
. . 3
โข (๐ โ HrmOp โ
โ๐ฅ โ โ
โ๐ฆ โ โ
(๐ฅ
ยทih (๐โ๐ฆ)) = ((๐โ๐ฅ) ยทih ๐ฆ)) |
3 | 2 | 3ad2ant1 1133 |
. 2
โข ((๐ โ HrmOp โง ๐ด โ โ โง ๐ต โ โ) โ
โ๐ฅ โ โ
โ๐ฆ โ โ
(๐ฅ
ยทih (๐โ๐ฆ)) = ((๐โ๐ฅ) ยทih ๐ฆ)) |
4 | | oveq1 7412 |
. . . . 5
โข (๐ฅ = ๐ด โ (๐ฅ ยทih (๐โ๐ฆ)) = (๐ด ยทih (๐โ๐ฆ))) |
5 | | fveq2 6888 |
. . . . . 6
โข (๐ฅ = ๐ด โ (๐โ๐ฅ) = (๐โ๐ด)) |
6 | 5 | oveq1d 7420 |
. . . . 5
โข (๐ฅ = ๐ด โ ((๐โ๐ฅ) ยทih ๐ฆ) = ((๐โ๐ด) ยทih ๐ฆ)) |
7 | 4, 6 | eqeq12d 2748 |
. . . 4
โข (๐ฅ = ๐ด โ ((๐ฅ ยทih (๐โ๐ฆ)) = ((๐โ๐ฅ) ยทih ๐ฆ) โ (๐ด ยทih (๐โ๐ฆ)) = ((๐โ๐ด) ยทih ๐ฆ))) |
8 | | fveq2 6888 |
. . . . . 6
โข (๐ฆ = ๐ต โ (๐โ๐ฆ) = (๐โ๐ต)) |
9 | 8 | oveq2d 7421 |
. . . . 5
โข (๐ฆ = ๐ต โ (๐ด ยทih (๐โ๐ฆ)) = (๐ด ยทih (๐โ๐ต))) |
10 | | oveq2 7413 |
. . . . 5
โข (๐ฆ = ๐ต โ ((๐โ๐ด) ยทih ๐ฆ) = ((๐โ๐ด) ยทih ๐ต)) |
11 | 9, 10 | eqeq12d 2748 |
. . . 4
โข (๐ฆ = ๐ต โ ((๐ด ยทih (๐โ๐ฆ)) = ((๐โ๐ด) ยทih ๐ฆ) โ (๐ด ยทih (๐โ๐ต)) = ((๐โ๐ด) ยทih ๐ต))) |
12 | 7, 11 | rspc2v 3621 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โ๐ฅ โ โ
โ๐ฆ โ โ
(๐ฅ
ยทih (๐โ๐ฆ)) = ((๐โ๐ฅ) ยทih ๐ฆ) โ (๐ด ยทih (๐โ๐ต)) = ((๐โ๐ด) ยทih ๐ต))) |
13 | 12 | 3adant1 1130 |
. 2
โข ((๐ โ HrmOp โง ๐ด โ โ โง ๐ต โ โ) โ
(โ๐ฅ โ โ
โ๐ฆ โ โ
(๐ฅ
ยทih (๐โ๐ฆ)) = ((๐โ๐ฅ) ยทih ๐ฆ) โ (๐ด ยทih (๐โ๐ต)) = ((๐โ๐ด) ยทih ๐ต))) |
14 | 3, 13 | mpd 15 |
1
โข ((๐ โ HrmOp โง ๐ด โ โ โง ๐ต โ โ) โ (๐ด
ยทih (๐โ๐ต)) = ((๐โ๐ด) ยทih ๐ต)) |