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

Metamath Proof Explorer

Theorem crng12d

Description: Commutative/associative law that swaps the first two factors in a triple product in a commutative ring. See also mul12d . (Contributed by SN, 8-Mar-2025)

Ref Expression
Hypotheses crng12d.b 
|- B = ( Base ` R )
crng12d.t 
|- .x. = ( .r ` R )
crng12d.r 
|- ( ph -> R e. CRing )
crng12d.1 
|- ( ph -> X e. B )
crng12d.2 
|- ( ph -> Y e. B )
crng12d.3 
|- ( ph -> Z e. B )
Assertion crng12d 
|- ( ph -> ( X .x. ( Y .x. Z ) ) = ( Y .x. ( X .x. Z ) ) )

Proof

Step Hyp Ref Expression
1 crng12d.b 
 |-  B = ( Base ` R )
2 crng12d.t 
 |-  .x. = ( .r ` R )
3 crng12d.r 
 |-  ( ph -> R e. CRing )
4 crng12d.1 
 |-  ( ph -> X e. B )
5 crng12d.2 
 |-  ( ph -> Y e. B )
6 crng12d.3 
 |-  ( ph -> Z e. B )
7 1 2 3 4 5 crngcomd 
 |-  ( ph -> ( X .x. Y ) = ( Y .x. X ) )
8 7 oveq1d 
 |-  ( ph -> ( ( X .x. Y ) .x. Z ) = ( ( Y .x. X ) .x. Z ) )
9 3 crngringd 
 |-  ( ph -> R e. Ring )
10 1 2 9 4 5 6 ringassd 
 |-  ( ph -> ( ( X .x. Y ) .x. Z ) = ( X .x. ( Y .x. Z ) ) )
11 1 2 9 5 4 6 ringassd 
 |-  ( ph -> ( ( Y .x. X ) .x. Z ) = ( Y .x. ( X .x. Z ) ) )
12 8 10 11 3eqtr3d 
 |-  ( ph -> ( X .x. ( Y .x. Z ) ) = ( Y .x. ( X .x. Z ) ) )