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

Metamath Proof Explorer

Theorem crngm4

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 crngm4 
|- ( ( R e. CRingOps /\ ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) -> ( ( A H B ) H ( C H D ) ) = ( ( A H C ) H ( B H D ) ) )

Proof

Step Hyp Ref Expression
1 crngm.1 
 |-  G = ( 1st ` R )
2 crngm.2 
 |-  H = ( 2nd ` R )
3 crngm.3 
 |-  X = ran G
4 df-3an 
 |-  ( ( A e. X /\ B e. X /\ C e. X ) <-> ( ( A e. X /\ B e. X ) /\ C e. X ) )
5 1 2 3 crngm23 
 |-  ( ( R e. CRingOps /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A H B ) H C ) = ( ( A H C ) H B ) )
6 4 5 sylan2br 
 |-  ( ( R e. CRingOps /\ ( ( A e. X /\ B e. X ) /\ C e. X ) ) -> ( ( A H B ) H C ) = ( ( A H C ) H B ) )
7 6 adantrrr 
 |-  ( ( R e. CRingOps /\ ( ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) ) -> ( ( A H B ) H C ) = ( ( A H C ) H B ) )
8 7 oveq1d 
 |-  ( ( R e. CRingOps /\ ( ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) ) -> ( ( ( A H B ) H C ) H D ) = ( ( ( A H C ) H B ) H D ) )
9 crngorngo 
 |-  ( R e. CRingOps -> R e. RingOps )
10 1 2 3 rngocl 
 |-  ( ( R e. RingOps /\ A e. X /\ B e. X ) -> ( A H B ) e. X )
11 10 3expb 
 |-  ( ( R e. RingOps /\ ( A e. X /\ B e. X ) ) -> ( A H B ) e. X )
12 11 adantrr 
 |-  ( ( R e. RingOps /\ ( ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) ) -> ( A H B ) e. X )
13 simprrl 
 |-  ( ( R e. RingOps /\ ( ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) ) -> C e. X )
14 simprrr 
 |-  ( ( R e. RingOps /\ ( ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) ) -> D e. X )
15 12 13 14 3jca 
 |-  ( ( R e. RingOps /\ ( ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) ) -> ( ( A H B ) e. X /\ C e. X /\ D e. X ) )
16 1 2 3 rngoass 
 |-  ( ( R e. RingOps /\ ( ( A H B ) e. X /\ C e. X /\ D e. X ) ) -> ( ( ( A H B ) H C ) H D ) = ( ( A H B ) H ( C H D ) ) )
17 15 16 syldan 
 |-  ( ( R e. RingOps /\ ( ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) ) -> ( ( ( A H B ) H C ) H D ) = ( ( A H B ) H ( C H D ) ) )
18 9 17 sylan 
 |-  ( ( R e. CRingOps /\ ( ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) ) -> ( ( ( A H B ) H C ) H D ) = ( ( A H B ) H ( C H D ) ) )
19 1 2 3 rngocl 
 |-  ( ( R e. RingOps /\ A e. X /\ C e. X ) -> ( A H C ) e. X )
20 19 3expb 
 |-  ( ( R e. RingOps /\ ( A e. X /\ C e. X ) ) -> ( A H C ) e. X )
21 20 adantrlr 
 |-  ( ( R e. RingOps /\ ( ( A e. X /\ B e. X ) /\ C e. X ) ) -> ( A H C ) e. X )
22 21 adantrrr 
 |-  ( ( R e. RingOps /\ ( ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) ) -> ( A H C ) e. X )
23 simprlr 
 |-  ( ( R e. RingOps /\ ( ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) ) -> B e. X )
24 22 23 14 3jca 
 |-  ( ( R e. RingOps /\ ( ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) ) -> ( ( A H C ) e. X /\ B e. X /\ D e. X ) )
25 1 2 3 rngoass 
 |-  ( ( R e. RingOps /\ ( ( A H C ) e. X /\ B e. X /\ D e. X ) ) -> ( ( ( A H C ) H B ) H D ) = ( ( A H C ) H ( B H D ) ) )
26 24 25 syldan 
 |-  ( ( R e. RingOps /\ ( ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) ) -> ( ( ( A H C ) H B ) H D ) = ( ( A H C ) H ( B H D ) ) )
27 9 26 sylan 
 |-  ( ( R e. CRingOps /\ ( ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) ) -> ( ( ( A H C ) H B ) H D ) = ( ( A H C ) H ( B H D ) ) )
28 8 18 27 3eqtr3d 
 |-  ( ( R e. CRingOps /\ ( ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) ) -> ( ( A H B ) H ( C H D ) ) = ( ( A H C ) H ( B H D ) ) )
29 28 3impb 
 |-  ( ( R e. CRingOps /\ ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) -> ( ( A H B ) H ( C H D ) ) = ( ( A H C ) H ( B H D ) ) )