Metamath Proof Explorer

Theorem int-leftdistd

Description: AdditionMultiplicationLeftDistribution generator rule. (Contributed by Stanislas Polu, 7-Apr-2020)

Ref Expression
Hypotheses int-leftdistd.1 
|- ( ph -> B e. RR )
int-leftdistd.2 
|- ( ph -> C e. RR )
int-leftdistd.3 
|- ( ph -> D e. RR )
int-leftdistd.4 
|- ( ph -> A = B )
Assertion int-leftdistd 
|- ( ph -> ( ( C + D ) x. B ) = ( ( C x. A ) + ( D x. A ) ) )

Proof

Step Hyp Ref Expression
1 int-leftdistd.1 
 |-  ( ph -> B e. RR )
2 int-leftdistd.2 
 |-  ( ph -> C e. RR )
3 int-leftdistd.3 
 |-  ( ph -> D e. RR )
4 int-leftdistd.4 
 |-  ( ph -> A = B )
5 2 recnd 
 |-  ( ph -> C e. CC )
6 3 recnd 
 |-  ( ph -> D e. CC )
7 1 recnd 
 |-  ( ph -> B e. CC )
8 5 6 7 adddird 
 |-  ( ph -> ( ( C + D ) x. B ) = ( ( C x. B ) + ( D x. B ) ) )
9 5 7 mulcld 
 |-  ( ph -> ( C x. B ) e. CC )
10 6 7 mulcld 
 |-  ( ph -> ( D x. B ) e. CC )
11 9 10 addcomd 
 |-  ( ph -> ( ( C x. B ) + ( D x. B ) ) = ( ( D x. B ) + ( C x. B ) ) )
12 10 9 addcomd 
 |-  ( ph -> ( ( D x. B ) + ( C x. B ) ) = ( ( C x. B ) + ( D x. B ) ) )
13 4 eqcomd 
 |-  ( ph -> B = A )
14 13 oveq2d 
 |-  ( ph -> ( C x. B ) = ( C x. A ) )
15 13 oveq2d 
 |-  ( ph -> ( D x. B ) = ( D x. A ) )
16 14 15 oveq12d 
 |-  ( ph -> ( ( C x. B ) + ( D x. B ) ) = ( ( C x. A ) + ( D x. A ) ) )
17 12 16 eqtrd 
 |-  ( ph -> ( ( D x. B ) + ( C x. B ) ) = ( ( C x. A ) + ( D x. A ) ) )
18 8 11 17 3eqtrd 
 |-  ( ph -> ( ( C + D ) x. B ) = ( ( C x. A ) + ( D x. A ) ) )