Step |
Hyp |
Ref |
Expression |
1 |
|
mulneg1 |
โข ( ( ๐ต โ โ โง ๐ด โ โ ) โ ( - ๐ต ยท ๐ด ) = - ( ๐ต ยท ๐ด ) ) |
2 |
1
|
ancoms |
โข ( ( ๐ด โ โ โง ๐ต โ โ ) โ ( - ๐ต ยท ๐ด ) = - ( ๐ต ยท ๐ด ) ) |
3 |
|
negcl |
โข ( ๐ต โ โ โ - ๐ต โ โ ) |
4 |
|
mulcom |
โข ( ( ๐ด โ โ โง - ๐ต โ โ ) โ ( ๐ด ยท - ๐ต ) = ( - ๐ต ยท ๐ด ) ) |
5 |
3 4
|
sylan2 |
โข ( ( ๐ด โ โ โง ๐ต โ โ ) โ ( ๐ด ยท - ๐ต ) = ( - ๐ต ยท ๐ด ) ) |
6 |
|
mulcom |
โข ( ( ๐ด โ โ โง ๐ต โ โ ) โ ( ๐ด ยท ๐ต ) = ( ๐ต ยท ๐ด ) ) |
7 |
6
|
negeqd |
โข ( ( ๐ด โ โ โง ๐ต โ โ ) โ - ( ๐ด ยท ๐ต ) = - ( ๐ต ยท ๐ด ) ) |
8 |
2 5 7
|
3eqtr4d |
โข ( ( ๐ด โ โ โง ๐ต โ โ ) โ ( ๐ด ยท - ๐ต ) = - ( ๐ด ยท ๐ต ) ) |