Step |
Hyp |
Ref |
Expression |
1 |
|
mulneg2 |
โข ( ( ๐ต โ โ โง ๐ถ โ โ ) โ ( ๐ต ยท - ๐ถ ) = - ( ๐ต ยท ๐ถ ) ) |
2 |
1
|
adantl |
โข ( ( ๐ด โ โ โง ( ๐ต โ โ โง ๐ถ โ โ ) ) โ ( ๐ต ยท - ๐ถ ) = - ( ๐ต ยท ๐ถ ) ) |
3 |
2
|
oveq2d |
โข ( ( ๐ด โ โ โง ( ๐ต โ โ โง ๐ถ โ โ ) ) โ ( ๐ด + ( ๐ต ยท - ๐ถ ) ) = ( ๐ด + - ( ๐ต ยท ๐ถ ) ) ) |
4 |
|
mulcl |
โข ( ( ๐ต โ โ โง ๐ถ โ โ ) โ ( ๐ต ยท ๐ถ ) โ โ ) |
5 |
|
negsub |
โข ( ( ๐ด โ โ โง ( ๐ต ยท ๐ถ ) โ โ ) โ ( ๐ด + - ( ๐ต ยท ๐ถ ) ) = ( ๐ด โ ( ๐ต ยท ๐ถ ) ) ) |
6 |
4 5
|
sylan2 |
โข ( ( ๐ด โ โ โง ( ๐ต โ โ โง ๐ถ โ โ ) ) โ ( ๐ด + - ( ๐ต ยท ๐ถ ) ) = ( ๐ด โ ( ๐ต ยท ๐ถ ) ) ) |
7 |
3 6
|
eqtr2d |
โข ( ( ๐ด โ โ โง ( ๐ต โ โ โง ๐ถ โ โ ) ) โ ( ๐ด โ ( ๐ต ยท ๐ถ ) ) = ( ๐ด + ( ๐ต ยท - ๐ถ ) ) ) |
8 |
7
|
3impb |
โข ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โ ( ๐ด โ ( ๐ต ยท ๐ถ ) ) = ( ๐ด + ( ๐ต ยท - ๐ถ ) ) ) |