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

Metamath Proof Explorer

Theorem muladd

Description: Product of two sums. (Contributed by NM, 14-Jan-2006) (Proof shortened by Andrew Salmon, 19-Nov-2011)

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

Proof

Step Hyp Ref Expression
1 addcl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
2 adddi 
 |-  ( ( ( A + B ) e. CC /\ C e. CC /\ D e. CC ) -> ( ( A + B ) x. ( C + D ) ) = ( ( ( A + B ) x. C ) + ( ( A + B ) x. D ) ) )
3 2 3expb 
 |-  ( ( ( A + B ) e. CC /\ ( C e. CC /\ D e. CC ) ) -> ( ( A + B ) x. ( C + D ) ) = ( ( ( A + B ) x. C ) + ( ( A + B ) x. D ) ) )
4 1 3 sylan 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A + B ) x. ( C + D ) ) = ( ( ( A + B ) x. C ) + ( ( A + B ) x. D ) ) )
5 adddir 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) x. C ) = ( ( A x. C ) + ( B x. C ) ) )
6 5 3expa 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ C e. CC ) -> ( ( A + B ) x. C ) = ( ( A x. C ) + ( B x. C ) ) )
7 6 adantrr 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A + B ) x. C ) = ( ( A x. C ) + ( B x. C ) ) )
8 adddir 
 |-  ( ( A e. CC /\ B e. CC /\ D e. CC ) -> ( ( A + B ) x. D ) = ( ( A x. D ) + ( B x. D ) ) )
9 8 3expa 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ D e. CC ) -> ( ( A + B ) x. D ) = ( ( A x. D ) + ( B x. D ) ) )
10 9 adantrl 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A + B ) x. D ) = ( ( A x. D ) + ( B x. D ) ) )
11 7 10 oveq12d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( A + B ) x. C ) + ( ( A + B ) x. D ) ) = ( ( ( A x. C ) + ( B x. C ) ) + ( ( A x. D ) + ( B x. D ) ) ) )
12 mulcl 
 |-  ( ( A e. CC /\ C e. CC ) -> ( A x. C ) e. CC )
13 12 ad2ant2r 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( A x. C ) e. CC )
14 mulcl 
 |-  ( ( B e. CC /\ C e. CC ) -> ( B x. C ) e. CC )
15 14 ad2ant2lr 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( B x. C ) e. CC )
16 mulcl 
 |-  ( ( A e. CC /\ D e. CC ) -> ( A x. D ) e. CC )
17 mulcl 
 |-  ( ( B e. CC /\ D e. CC ) -> ( B x. D ) e. CC )
18 addcl 
 |-  ( ( ( A x. D ) e. CC /\ ( B x. D ) e. CC ) -> ( ( A x. D ) + ( B x. D ) ) e. CC )
19 16 17 18 syl2an 
 |-  ( ( ( A e. CC /\ D e. CC ) /\ ( B e. CC /\ D e. CC ) ) -> ( ( A x. D ) + ( B x. D ) ) e. CC )
20 19 anandirs 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ D e. CC ) -> ( ( A x. D ) + ( B x. D ) ) e. CC )
21 20 adantrl 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A x. D ) + ( B x. D ) ) e. CC )
22 13 15 21 add32d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( A x. C ) + ( B x. C ) ) + ( ( A x. D ) + ( B x. D ) ) ) = ( ( ( A x. C ) + ( ( A x. D ) + ( B x. D ) ) ) + ( B x. C ) ) )
23 mulcom 
 |-  ( ( B e. CC /\ D e. CC ) -> ( B x. D ) = ( D x. B ) )
24 23 ad2ant2l 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( B x. D ) = ( D x. B ) )
25 24 oveq2d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( A x. C ) + ( A x. D ) ) + ( B x. D ) ) = ( ( ( A x. C ) + ( A x. D ) ) + ( D x. B ) ) )
26 16 ad2ant2rl 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( A x. D ) e. CC )
27 17 ad2ant2l 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( B x. D ) e. CC )
28 13 26 27 addassd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( A x. C ) + ( A x. D ) ) + ( B x. D ) ) = ( ( A x. C ) + ( ( A x. D ) + ( B x. D ) ) ) )
29 mulcl 
 |-  ( ( D e. CC /\ B e. CC ) -> ( D x. B ) e. CC )
30 29 ancoms 
 |-  ( ( B e. CC /\ D e. CC ) -> ( D x. B ) e. CC )
31 30 ad2ant2l 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( D x. B ) e. CC )
32 13 26 31 add32d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( A x. C ) + ( A x. D ) ) + ( D x. B ) ) = ( ( ( A x. C ) + ( D x. B ) ) + ( A x. D ) ) )
33 25 28 32 3eqtr3d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A x. C ) + ( ( A x. D ) + ( B x. D ) ) ) = ( ( ( A x. C ) + ( D x. B ) ) + ( A x. D ) ) )
34 mulcom 
 |-  ( ( B e. CC /\ C e. CC ) -> ( B x. C ) = ( C x. B ) )
35 34 ad2ant2lr 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( B x. C ) = ( C x. B ) )
36 33 35 oveq12d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( A x. C ) + ( ( A x. D ) + ( B x. D ) ) ) + ( B x. C ) ) = ( ( ( ( A x. C ) + ( D x. B ) ) + ( A x. D ) ) + ( C x. B ) ) )
37 addcl 
 |-  ( ( ( A x. C ) e. CC /\ ( D x. B ) e. CC ) -> ( ( A x. C ) + ( D x. B ) ) e. CC )
38 12 30 37 syl2an 
 |-  ( ( ( A e. CC /\ C e. CC ) /\ ( B e. CC /\ D e. CC ) ) -> ( ( A x. C ) + ( D x. B ) ) e. CC )
39 38 an4s 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A x. C ) + ( D x. B ) ) e. CC )
40 mulcl 
 |-  ( ( C e. CC /\ B e. CC ) -> ( C x. B ) e. CC )
41 40 ancoms 
 |-  ( ( B e. CC /\ C e. CC ) -> ( C x. B ) e. CC )
42 41 ad2ant2lr 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( C x. B ) e. CC )
43 39 26 42 addassd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( ( A x. C ) + ( D x. B ) ) + ( A x. D ) ) + ( C x. B ) ) = ( ( ( A x. C ) + ( D x. B ) ) + ( ( A x. D ) + ( C x. B ) ) ) )
44 22 36 43 3eqtrd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( A x. C ) + ( B x. C ) ) + ( ( A x. D ) + ( B x. D ) ) ) = ( ( ( A x. C ) + ( D x. B ) ) + ( ( A x. D ) + ( C x. B ) ) ) )
45 4 11 44 3eqtrd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A + B ) x. ( C + D ) ) = ( ( ( A x. C ) + ( D x. B ) ) + ( ( A x. D ) + ( C x. B ) ) ) )