Metamath Proof Explorer

Theorem addmuldir2d

Description: Distributive law with summands being products with a common factor. (Contributed by AV, 25-Oct-2026)

Ref Expression
Hypotheses addmuldir2d.a 
|- ( ph -> A e. CC )
addmuldir2d.b 
|- ( ph -> B e. CC )
addmuldir2d.c 
|- ( ph -> C e. CC )
addmuldir2d.d 
|- ( ph -> D e. CC )
addmuldir2d.e 
|- ( ph -> E e. CC )
Assertion addmuldir2d 
|- ( ph -> ( ( A + ( B x. C ) ) x. ( D + ( E x. C ) ) ) = ( ( ( A x. D ) + ( ( ( A x. E ) + ( D x. B ) ) x. C ) ) + ( ( B x. E ) x. ( C ^ 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 addmuldir2d.a 
 |-  ( ph -> A e. CC )
2 addmuldir2d.b 
 |-  ( ph -> B e. CC )
3 addmuldir2d.c 
 |-  ( ph -> C e. CC )
4 addmuldir2d.d 
 |-  ( ph -> D e. CC )
5 addmuldir2d.e 
 |-  ( ph -> E e. CC )
6 1 2 3 4 5 3 addmuldir1d 
 |-  ( ph -> ( ( A + ( B x. C ) ) x. ( D + ( E x. C ) ) ) = ( ( ( A x. D ) + ( A x. ( E x. C ) ) ) + ( ( D x. ( B x. C ) ) + ( ( B x. C ) x. ( E x. C ) ) ) ) )
7 1 4 mulcld 
 |-  ( ph -> ( A x. D ) e. CC )
8 5 3 mulcld 
 |-  ( ph -> ( E x. C ) e. CC )
9 1 8 mulcld 
 |-  ( ph -> ( A x. ( E x. C ) ) e. CC )
10 7 9 addcld 
 |-  ( ph -> ( ( A x. D ) + ( A x. ( E x. C ) ) ) e. CC )
11 2 3 mulcld 
 |-  ( ph -> ( B x. C ) e. CC )
12 4 11 mulcld 
 |-  ( ph -> ( D x. ( B x. C ) ) e. CC )
13 11 8 mulcld 
 |-  ( ph -> ( ( B x. C ) x. ( E x. C ) ) e. CC )
14 10 12 13 addassd 
 |-  ( ph -> ( ( ( ( A x. D ) + ( A x. ( E x. C ) ) ) + ( D x. ( B x. C ) ) ) + ( ( B x. C ) x. ( E x. C ) ) ) = ( ( ( A x. D ) + ( A x. ( E x. C ) ) ) + ( ( D x. ( B x. C ) ) + ( ( B x. C ) x. ( E x. C ) ) ) ) )
15 7 9 12 addassd 
 |-  ( ph -> ( ( ( A x. D ) + ( A x. ( E x. C ) ) ) + ( D x. ( B x. C ) ) ) = ( ( A x. D ) + ( ( A x. ( E x. C ) ) + ( D x. ( B x. C ) ) ) ) )
16 1 5 mulcld 
 |-  ( ph -> ( A x. E ) e. CC )
17 4 2 mulcld 
 |-  ( ph -> ( D x. B ) e. CC )
18 16 17 3 adddird 
 |-  ( ph -> ( ( ( A x. E ) + ( D x. B ) ) x. C ) = ( ( ( A x. E ) x. C ) + ( ( D x. B ) x. C ) ) )
19 1 5 3 mulassd 
 |-  ( ph -> ( ( A x. E ) x. C ) = ( A x. ( E x. C ) ) )
20 4 2 3 mulassd 
 |-  ( ph -> ( ( D x. B ) x. C ) = ( D x. ( B x. C ) ) )
21 19 20 oveq12d 
 |-  ( ph -> ( ( ( A x. E ) x. C ) + ( ( D x. B ) x. C ) ) = ( ( A x. ( E x. C ) ) + ( D x. ( B x. C ) ) ) )
22 18 21 eqtr2d 
 |-  ( ph -> ( ( A x. ( E x. C ) ) + ( D x. ( B x. C ) ) ) = ( ( ( A x. E ) + ( D x. B ) ) x. C ) )
23 22 oveq2d 
 |-  ( ph -> ( ( A x. D ) + ( ( A x. ( E x. C ) ) + ( D x. ( B x. C ) ) ) ) = ( ( A x. D ) + ( ( ( A x. E ) + ( D x. B ) ) x. C ) ) )
24 15 23 eqtrd 
 |-  ( ph -> ( ( ( A x. D ) + ( A x. ( E x. C ) ) ) + ( D x. ( B x. C ) ) ) = ( ( A x. D ) + ( ( ( A x. E ) + ( D x. B ) ) x. C ) ) )
25 2 3 5 3 mul4d 
 |-  ( ph -> ( ( B x. C ) x. ( E x. C ) ) = ( ( B x. E ) x. ( C x. C ) ) )
26 sqval 
 |-  ( C e. CC -> ( C ^ 2 ) = ( C x. C ) )
27 26 eqcomd 
 |-  ( C e. CC -> ( C x. C ) = ( C ^ 2 ) )
28 3 27 syl 
 |-  ( ph -> ( C x. C ) = ( C ^ 2 ) )
29 28 oveq2d 
 |-  ( ph -> ( ( B x. E ) x. ( C x. C ) ) = ( ( B x. E ) x. ( C ^ 2 ) ) )
30 25 29 eqtrd 
 |-  ( ph -> ( ( B x. C ) x. ( E x. C ) ) = ( ( B x. E ) x. ( C ^ 2 ) ) )
31 24 30 oveq12d 
 |-  ( ph -> ( ( ( ( A x. D ) + ( A x. ( E x. C ) ) ) + ( D x. ( B x. C ) ) ) + ( ( B x. C ) x. ( E x. C ) ) ) = ( ( ( A x. D ) + ( ( ( A x. E ) + ( D x. B ) ) x. C ) ) + ( ( B x. E ) x. ( C ^ 2 ) ) ) )
32 6 14 31 3eqtr2d 
 |-  ( ph -> ( ( A + ( B x. C ) ) x. ( D + ( E x. C ) ) ) = ( ( ( A x. D ) + ( ( ( A x. E ) + ( D x. B ) ) x. C ) ) + ( ( B x. E ) x. ( C ^ 2 ) ) ) )