Metamath Proof Explorer

Theorem mul4

Description: Rearrangement of 4 factors. (Contributed by NM, 8-Oct-1999)

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

Proof

Step Hyp Ref Expression
1 mul32 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. B ) x. C ) = ( ( A x. C ) x. B ) )
2 1 oveq1d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( ( A x. B ) x. C ) x. D ) = ( ( ( A x. C ) x. B ) x. D ) )
3 2 3expa 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ C e. CC ) -> ( ( ( A x. B ) x. C ) x. D ) = ( ( ( A x. C ) x. B ) x. D ) )
4 3 adantrr 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( A x. B ) x. C ) x. D ) = ( ( ( A x. C ) x. B ) x. D ) )
5 mulcl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )
6 mulass 
 |-  ( ( ( A x. B ) e. CC /\ C e. CC /\ D e. CC ) -> ( ( ( A x. B ) x. C ) x. D ) = ( ( A x. B ) x. ( C x. D ) ) )
7 6 3expb 
 |-  ( ( ( A x. B ) e. CC /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( A x. B ) x. C ) x. D ) = ( ( A x. B ) x. ( C x. D ) ) )
8 5 7 sylan 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( A x. B ) x. C ) x. D ) = ( ( A x. B ) x. ( C x. D ) ) )
9 mulcl 
 |-  ( ( A e. CC /\ C e. CC ) -> ( A x. C ) e. CC )
10 mulass 
 |-  ( ( ( A x. C ) e. CC /\ B e. CC /\ D e. CC ) -> ( ( ( A x. C ) x. B ) x. D ) = ( ( A x. C ) x. ( B x. D ) ) )
11 10 3expb 
 |-  ( ( ( A x. C ) e. CC /\ ( B e. CC /\ D e. CC ) ) -> ( ( ( A x. C ) x. B ) x. D ) = ( ( A x. C ) x. ( B x. D ) ) )
12 9 11 sylan 
 |-  ( ( ( A e. CC /\ C e. CC ) /\ ( B e. CC /\ D e. CC ) ) -> ( ( ( A x. C ) x. B ) x. D ) = ( ( A x. C ) x. ( B x. D ) ) )
13 12 an4s 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( A x. C ) x. B ) x. D ) = ( ( A x. C ) x. ( B x. D ) ) )
14 4 8 13 3eqtr3d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A x. B ) x. ( C x. D ) ) = ( ( A x. C ) x. ( B x. D ) ) )