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 = 1 st ⁡ R
crngm.2 ⊢ H = 2 nd ⁡ R
crngm.3 ⊢ X = ran ⁡ G
Assertion crngm4 ⊢ R ∈ CRingOps ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ D ∈ X → A H B H C H D = A H C H B H D

Proof

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