Metamath Proof Explorer

Theorem int-rightdistd

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

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

Proof

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