This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mul4r

Description: Rearrangement of 4 factors: swap the right factors in the factors of a product of two products. (Contributed by AV, 4-Mar-2023)

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

Proof

Step Hyp Ref Expression
1 mulcom 
 |-  ( ( C e. CC /\ D e. CC ) -> ( C x. D ) = ( D x. C ) )
2 1 adantl 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( C x. D ) = ( D x. C ) )
3 2 oveq2d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A x. B ) x. ( C x. D ) ) = ( ( A x. B ) x. ( D x. C ) ) )
4 mul4 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( D e. CC /\ C e. CC ) ) -> ( ( A x. B ) x. ( D x. C ) ) = ( ( A x. D ) x. ( B x. C ) ) )
5 4 ancom2s 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A x. B ) x. ( D x. C ) ) = ( ( A x. D ) x. ( B x. C ) ) )
6 simplr 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> B e. CC )
7 simprl 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> C e. CC )
8 6 7 mulcomd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( B x. C ) = ( C x. B ) )
9 8 oveq2d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A x. D ) x. ( B x. C ) ) = ( ( A x. D ) x. ( C x. B ) ) )
10 3 5 9 3eqtrd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A x. B ) x. ( C x. D ) ) = ( ( A x. D ) x. ( C x. B ) ) )