Step |
Hyp |
Ref |
Expression |
1 |
|
lnopl.1 |
โข ๐ โ LinOp |
2 |
|
hvmulcl |
โข ( ( ๐ด โ โ โง ๐ต โ โ ) โ ( ๐ด ยทโ ๐ต ) โ โ ) |
3 |
1
|
lnopsubi |
โข ( ( ( ๐ด ยทโ ๐ต ) โ โ โง ๐ถ โ โ ) โ ( ๐ โ ( ( ๐ด ยทโ ๐ต ) โโ ๐ถ ) ) = ( ( ๐ โ ( ๐ด ยทโ ๐ต ) ) โโ ( ๐ โ ๐ถ ) ) ) |
4 |
2 3
|
stoic3 |
โข ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โ ( ๐ โ ( ( ๐ด ยทโ ๐ต ) โโ ๐ถ ) ) = ( ( ๐ โ ( ๐ด ยทโ ๐ต ) ) โโ ( ๐ โ ๐ถ ) ) ) |
5 |
1
|
lnopmuli |
โข ( ( ๐ด โ โ โง ๐ต โ โ ) โ ( ๐ โ ( ๐ด ยทโ ๐ต ) ) = ( ๐ด ยทโ ( ๐ โ ๐ต ) ) ) |
6 |
5
|
3adant3 |
โข ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โ ( ๐ โ ( ๐ด ยทโ ๐ต ) ) = ( ๐ด ยทโ ( ๐ โ ๐ต ) ) ) |
7 |
6
|
oveq1d |
โข ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โ ( ( ๐ โ ( ๐ด ยทโ ๐ต ) ) โโ ( ๐ โ ๐ถ ) ) = ( ( ๐ด ยทโ ( ๐ โ ๐ต ) ) โโ ( ๐ โ ๐ถ ) ) ) |
8 |
4 7
|
eqtrd |
โข ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โ ( ๐ โ ( ( ๐ด ยทโ ๐ต ) โโ ๐ถ ) ) = ( ( ๐ด ยทโ ( ๐ โ ๐ต ) ) โโ ( ๐ โ ๐ถ ) ) ) |