This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mulsubaddmulsub

Description: A special difference of a product with a product of a sum and a difference. (Contributed by AV, 5-Mar-2023)

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

Proof

Step Hyp Ref Expression
1 simplr 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> B e. CC )
2 simprl 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> C e. CC )
3 1 2 mulcld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( B x. C ) e. CC )
4 subaddmulsub 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) /\ ( B x. C ) e. CC ) -> ( ( B x. C ) - ( ( A + B ) x. ( C - D ) ) ) = ( ( ( ( B x. C ) - ( A x. C ) ) - ( B x. C ) ) + ( ( A x. D ) + ( B x. D ) ) ) )
5 3 4 mpd3an3 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( B x. C ) - ( ( A + B ) x. ( C - D ) ) ) = ( ( ( ( B x. C ) - ( A x. C ) ) - ( B x. C ) ) + ( ( A x. D ) + ( B x. D ) ) ) )
6 simpll 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> A e. CC )
7 6 2 mulcld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( A x. C ) e. CC )
8 3 7 3 sub32d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( B x. C ) - ( A x. C ) ) - ( B x. C ) ) = ( ( ( B x. C ) - ( B x. C ) ) - ( A x. C ) ) )
9 3 subidd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( B x. C ) - ( B x. C ) ) = 0 )
10 9 oveq1d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( B x. C ) - ( B x. C ) ) - ( A x. C ) ) = ( 0 - ( A x. C ) ) )
11 8 10 eqtrd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( B x. C ) - ( A x. C ) ) - ( B x. C ) ) = ( 0 - ( A x. C ) ) )
12 df-neg 
 |-  -u ( A x. C ) = ( 0 - ( A x. C ) )
13 11 12 eqtr4di 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( B x. C ) - ( A x. C ) ) - ( B x. C ) ) = -u ( A x. C ) )
14 13 oveq1d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( ( B x. C ) - ( A x. C ) ) - ( B x. C ) ) + ( ( A x. D ) + ( B x. D ) ) ) = ( -u ( A x. C ) + ( ( A x. D ) + ( B x. D ) ) ) )
15 7 negcld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> -u ( A x. C ) e. CC )
16 simprr 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> D e. CC )
17 6 16 mulcld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( A x. D ) e. CC )
18 1 16 mulcld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( B x. D ) e. CC )
19 17 18 addcld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A x. D ) + ( B x. D ) ) e. CC )
20 15 19 addcomd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( -u ( A x. C ) + ( ( A x. D ) + ( B x. D ) ) ) = ( ( ( A x. D ) + ( B x. D ) ) + -u ( A x. C ) ) )
21 19 7 negsubd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( A x. D ) + ( B x. D ) ) + -u ( A x. C ) ) = ( ( ( A x. D ) + ( B x. D ) ) - ( A x. C ) ) )
22 20 21 eqtrd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( -u ( A x. C ) + ( ( A x. D ) + ( B x. D ) ) ) = ( ( ( A x. D ) + ( B x. D ) ) - ( A x. C ) ) )
23 14 22 eqtrd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( ( B x. C ) - ( A x. C ) ) - ( B x. C ) ) + ( ( A x. D ) + ( B x. D ) ) ) = ( ( ( A x. D ) + ( B x. D ) ) - ( A x. C ) ) )
24 5 23 eqtrd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( B x. C ) - ( ( A + B ) x. ( C - D ) ) ) = ( ( ( A x. D ) + ( B x. D ) ) - ( A x. C ) ) )