Metamath Proof Explorer

Theorem crngm23

Description: Commutative/associative law for commutative rings. (Contributed by Jeff Madsen, 19-Jun-2010)

Ref Expression
Hypotheses crngm.1 
|- G = ( 1st ` R )
crngm.2 
|- H = ( 2nd ` R )
crngm.3 
|- X = ran G
Assertion crngm23 
|- ( ( R e. CRingOps /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A H B ) H C ) = ( ( A H C ) H B ) )

Proof

Step Hyp Ref Expression
1 crngm.1 
 |-  G = ( 1st ` R )
2 crngm.2 
 |-  H = ( 2nd ` R )
3 crngm.3 
 |-  X = ran G
4 1 2 3 crngocom 
 |-  ( ( R e. CRingOps /\ B e. X /\ C e. X ) -> ( B H C ) = ( C H B ) )
5 4 3adant3r1 
 |-  ( ( R e. CRingOps /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( B H C ) = ( C H B ) )
6 5 oveq2d 
 |-  ( ( R e. CRingOps /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A H ( B H C ) ) = ( A H ( C H B ) ) )
7 crngorngo 
 |-  ( R e. CRingOps -> R e. RingOps )
8 1 2 3 rngoass 
 |-  ( ( R e. RingOps /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A H B ) H C ) = ( A H ( B H C ) ) )
9 7 8 sylan 
 |-  ( ( R e. CRingOps /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A H B ) H C ) = ( A H ( B H C ) ) )
10 1 2 3 rngoass 
 |-  ( ( R e. RingOps /\ ( A e. X /\ C e. X /\ B e. X ) ) -> ( ( A H C ) H B ) = ( A H ( C H B ) ) )
11 10 3exp2 
 |-  ( R e. RingOps -> ( A e. X -> ( C e. X -> ( B e. X -> ( ( A H C ) H B ) = ( A H ( C H B ) ) ) ) ) )
12 11 com34 
 |-  ( R e. RingOps -> ( A e. X -> ( B e. X -> ( C e. X -> ( ( A H C ) H B ) = ( A H ( C H B ) ) ) ) ) )
13 12 3imp2 
 |-  ( ( R e. RingOps /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A H C ) H B ) = ( A H ( C H B ) ) )
14 7 13 sylan 
 |-  ( ( R e. CRingOps /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A H C ) H B ) = ( A H ( C H B ) ) )
15 6 9 14 3eqtr4d 
 |-  ( ( R e. CRingOps /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A H B ) H C ) = ( ( A H C ) H B ) )