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

Metamath Proof Explorer

Theorem subaddmulsub

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

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

Proof

Step Hyp Ref Expression
1 addmulsub 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A + B ) x. ( C - D ) ) = ( ( ( A x. C ) + ( B x. C ) ) - ( ( A x. D ) + ( B x. D ) ) ) )
2 1 3adant3 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) /\ E e. CC ) -> ( ( A + B ) x. ( C - D ) ) = ( ( ( A x. C ) + ( B x. C ) ) - ( ( A x. D ) + ( B x. D ) ) ) )
3 2 oveq2d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) /\ E e. CC ) -> ( E - ( ( A + B ) x. ( C - D ) ) ) = ( E - ( ( ( A x. C ) + ( B x. C ) ) - ( ( A x. D ) + ( B x. D ) ) ) ) )
4 simp3 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) /\ E e. CC ) -> E e. CC )
5 simp1l 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) /\ E e. CC ) -> A e. CC )
6 simp2l 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) /\ E e. CC ) -> C e. CC )
7 5 6 mulcld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) /\ E e. CC ) -> ( A x. C ) e. CC )
8 simp1r 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) /\ E e. CC ) -> B e. CC )
9 8 6 mulcld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) /\ E e. CC ) -> ( B x. C ) e. CC )
10 7 9 addcld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) /\ E e. CC ) -> ( ( A x. C ) + ( B x. C ) ) e. CC )
11 simp2r 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) /\ E e. CC ) -> D e. CC )
12 5 11 mulcld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) /\ E e. CC ) -> ( A x. D ) e. CC )
13 8 11 mulcld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) /\ E e. CC ) -> ( B x. D ) e. CC )
14 12 13 addcld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) /\ E e. CC ) -> ( ( A x. D ) + ( B x. D ) ) e. CC )
15 4 10 14 subsubd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) /\ E e. CC ) -> ( E - ( ( ( A x. C ) + ( B x. C ) ) - ( ( A x. D ) + ( B x. D ) ) ) ) = ( ( E - ( ( A x. C ) + ( B x. C ) ) ) + ( ( A x. D ) + ( B x. D ) ) ) )
16 4 7 9 subsub4d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) /\ E e. CC ) -> ( ( E - ( A x. C ) ) - ( B x. C ) ) = ( E - ( ( A x. C ) + ( B x. C ) ) ) )
17 16 eqcomd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) /\ E e. CC ) -> ( E - ( ( A x. C ) + ( B x. C ) ) ) = ( ( E - ( A x. C ) ) - ( B x. C ) ) )
18 17 oveq1d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) /\ E e. CC ) -> ( ( E - ( ( A x. C ) + ( B x. C ) ) ) + ( ( A x. D ) + ( B x. D ) ) ) = ( ( ( E - ( A x. C ) ) - ( B x. C ) ) + ( ( A x. D ) + ( B x. D ) ) ) )
19 3 15 18 3eqtrd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) /\ E e. CC ) -> ( E - ( ( A + B ) x. ( C - D ) ) ) = ( ( ( E - ( A x. C ) ) - ( B x. C ) ) + ( ( A x. D ) + ( B x. D ) ) ) )