Step |
Hyp |
Ref |
Expression |
1 |
|
remulneg2d.a |
|- ( ph -> A e. RR ) |
2 |
|
remulneg2d.b |
|- ( ph -> B e. RR ) |
3 |
|
0red |
|- ( ph -> 0 e. RR ) |
4 |
|
resubdi |
|- ( ( A e. RR /\ 0 e. RR /\ B e. RR ) -> ( A x. ( 0 -R B ) ) = ( ( A x. 0 ) -R ( A x. B ) ) ) |
5 |
1 3 2 4
|
syl3anc |
|- ( ph -> ( A x. ( 0 -R B ) ) = ( ( A x. 0 ) -R ( A x. B ) ) ) |
6 |
|
remul01 |
|- ( A e. RR -> ( A x. 0 ) = 0 ) |
7 |
1 6
|
syl |
|- ( ph -> ( A x. 0 ) = 0 ) |
8 |
7
|
oveq1d |
|- ( ph -> ( ( A x. 0 ) -R ( A x. B ) ) = ( 0 -R ( A x. B ) ) ) |
9 |
5 8
|
eqtrd |
|- ( ph -> ( A x. ( 0 -R B ) ) = ( 0 -R ( A x. B ) ) ) |