Metamath Proof Explorer

Theorem addmuldir1d

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

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

Proof

Step Hyp Ref Expression
1 addmuldir1d.a 
 |-  ( ph -> A e. CC )
2 addmuldir1d.b 
 |-  ( ph -> B e. CC )
3 addmuldir1d.c 
 |-  ( ph -> C e. CC )
4 addmuldir1d.d 
 |-  ( ph -> D e. CC )
5 addmuldir1d.e 
 |-  ( ph -> E e. CC )
6 addmuldir1d.f 
 |-  ( ph -> F e. CC )
7 2 3 mulcld 
 |-  ( ph -> ( B x. C ) e. CC )
8 5 6 mulcld 
 |-  ( ph -> ( E x. F ) e. CC )
9 1 7 4 8 muladdd 
 |-  ( ph -> ( ( A + ( B x. C ) ) x. ( D + ( E x. F ) ) ) = ( ( ( A x. D ) + ( ( E x. F ) x. ( B x. C ) ) ) + ( ( A x. ( E x. F ) ) + ( D x. ( B x. C ) ) ) ) )
10 1 4 mulcld 
 |-  ( ph -> ( A x. D ) e. CC )
11 8 7 mulcld 
 |-  ( ph -> ( ( E x. F ) x. ( B x. C ) ) e. CC )
12 1 8 mulcld 
 |-  ( ph -> ( A x. ( E x. F ) ) e. CC )
13 4 7 mulcld 
 |-  ( ph -> ( D x. ( B x. C ) ) e. CC )
14 10 11 12 13 add42d 
 |-  ( ph -> ( ( ( A x. D ) + ( ( E x. F ) x. ( B x. C ) ) ) + ( ( A x. ( E x. F ) ) + ( D x. ( B x. C ) ) ) ) = ( ( ( A x. D ) + ( A x. ( E x. F ) ) ) + ( ( D x. ( B x. C ) ) + ( ( E x. F ) x. ( B x. C ) ) ) ) )
15 8 7 mulcomd 
 |-  ( ph -> ( ( E x. F ) x. ( B x. C ) ) = ( ( B x. C ) x. ( E x. F ) ) )
16 15 oveq2d 
 |-  ( ph -> ( ( D x. ( B x. C ) ) + ( ( E x. F ) x. ( B x. C ) ) ) = ( ( D x. ( B x. C ) ) + ( ( B x. C ) x. ( E x. F ) ) ) )
17 16 oveq2d 
 |-  ( ph -> ( ( ( A x. D ) + ( A x. ( E x. F ) ) ) + ( ( D x. ( B x. C ) ) + ( ( E x. F ) x. ( B x. C ) ) ) ) = ( ( ( A x. D ) + ( A x. ( E x. F ) ) ) + ( ( D x. ( B x. C ) ) + ( ( B x. C ) x. ( E x. F ) ) ) ) )
18 9 14 17 3eqtrd 
 |-  ( ph -> ( ( A + ( B x. C ) ) x. ( D + ( E x. F ) ) ) = ( ( ( A x. D ) + ( A x. ( E x. F ) ) ) + ( ( D x. ( B x. C ) ) + ( ( B x. C ) x. ( E x. F ) ) ) ) )