Step | Hyp | Ref
| Expression |
1 | | elunop 31407 |
. . . 4
โข (๐ โ UniOp โ (๐: โโontoโ โ โง โ๐ฅ โ โ โ๐ฆ โ โ ((๐โ๐ฅ) ยทih (๐โ๐ฆ)) = (๐ฅ ยทih ๐ฆ))) |
2 | 1 | simprbi 496 |
. . 3
โข (๐ โ UniOp โ
โ๐ฅ โ โ
โ๐ฆ โ โ
((๐โ๐ฅ)
ยทih (๐โ๐ฆ)) = (๐ฅ ยทih ๐ฆ)) |
3 | 2 | 3ad2ant1 1132 |
. 2
โข ((๐ โ UniOp โง ๐ด โ โ โง ๐ต โ โ) โ
โ๐ฅ โ โ
โ๐ฆ โ โ
((๐โ๐ฅ)
ยทih (๐โ๐ฆ)) = (๐ฅ ยทih ๐ฆ)) |
4 | | fveq2 6891 |
. . . . . 6
โข (๐ฅ = ๐ด โ (๐โ๐ฅ) = (๐โ๐ด)) |
5 | 4 | oveq1d 7427 |
. . . . 5
โข (๐ฅ = ๐ด โ ((๐โ๐ฅ) ยทih (๐โ๐ฆ)) = ((๐โ๐ด) ยทih (๐โ๐ฆ))) |
6 | | oveq1 7419 |
. . . . 5
โข (๐ฅ = ๐ด โ (๐ฅ ยทih ๐ฆ) = (๐ด ยทih ๐ฆ)) |
7 | 5, 6 | eqeq12d 2747 |
. . . 4
โข (๐ฅ = ๐ด โ (((๐โ๐ฅ) ยทih (๐โ๐ฆ)) = (๐ฅ ยทih ๐ฆ) โ ((๐โ๐ด) ยทih (๐โ๐ฆ)) = (๐ด ยทih ๐ฆ))) |
8 | | fveq2 6891 |
. . . . . 6
โข (๐ฆ = ๐ต โ (๐โ๐ฆ) = (๐โ๐ต)) |
9 | 8 | oveq2d 7428 |
. . . . 5
โข (๐ฆ = ๐ต โ ((๐โ๐ด) ยทih (๐โ๐ฆ)) = ((๐โ๐ด) ยทih (๐โ๐ต))) |
10 | | oveq2 7420 |
. . . . 5
โข (๐ฆ = ๐ต โ (๐ด ยทih ๐ฆ) = (๐ด ยทih ๐ต)) |
11 | 9, 10 | eqeq12d 2747 |
. . . 4
โข (๐ฆ = ๐ต โ (((๐โ๐ด) ยทih (๐โ๐ฆ)) = (๐ด ยทih ๐ฆ) โ ((๐โ๐ด) ยทih (๐โ๐ต)) = (๐ด ยทih ๐ต))) |
12 | 7, 11 | rspc2v 3622 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โ๐ฅ โ โ
โ๐ฆ โ โ
((๐โ๐ฅ)
ยทih (๐โ๐ฆ)) = (๐ฅ ยทih ๐ฆ) โ ((๐โ๐ด) ยทih (๐โ๐ต)) = (๐ด ยทih ๐ต))) |
13 | 12 | 3adant1 1129 |
. 2
โข ((๐ โ UniOp โง ๐ด โ โ โง ๐ต โ โ) โ
(โ๐ฅ โ โ
โ๐ฆ โ โ
((๐โ๐ฅ)
ยทih (๐โ๐ฆ)) = (๐ฅ ยทih ๐ฆ) โ ((๐โ๐ด) ยทih (๐โ๐ต)) = (๐ด ยทih ๐ต))) |
14 | 3, 13 | mpd 15 |
1
โข ((๐ โ UniOp โง ๐ด โ โ โง ๐ต โ โ) โ ((๐โ๐ด) ยทih (๐โ๐ต)) = (๐ด ยทih ๐ต)) |