Metamath Proof Explorer

Theorem mulsub2

Description: Swap the order of subtraction in a multiplication. (Contributed by Scott Fenton, 24-Jun-2013)

Ref Expression
Assertion mulsub2 
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A - B ) x. ( C - D ) ) = ( ( B - A ) x. ( D - C ) ) )

Proof

Step Hyp Ref Expression
1 subcl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A - B ) e. CC )
2 subcl 
 |-  ( ( C e. CC /\ D e. CC ) -> ( C - D ) e. CC )
3 mul2neg 
 |-  ( ( ( A - B ) e. CC /\ ( C - D ) e. CC ) -> ( -u ( A - B ) x. -u ( C - D ) ) = ( ( A - B ) x. ( C - D ) ) )
4 1 2 3 syl2an 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( -u ( A - B ) x. -u ( C - D ) ) = ( ( A - B ) x. ( C - D ) ) )
5 negsubdi2 
 |-  ( ( A e. CC /\ B e. CC ) -> -u ( A - B ) = ( B - A ) )
6 negsubdi2 
 |-  ( ( C e. CC /\ D e. CC ) -> -u ( C - D ) = ( D - C ) )
7 5 6 oveqan12d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( -u ( A - B ) x. -u ( C - D ) ) = ( ( B - A ) x. ( D - C ) ) )
8 4 7 eqtr3d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A - B ) x. ( C - D ) ) = ( ( B - A ) x. ( D - C ) ) )