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

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 1 2 3 crngocom ⊢ R ∈ CRingOps ∧ B ∈ X ∧ C ∈ X → B H C = C H B
5 4 3adant3r1 ⊢ R ∈ CRingOps ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → B H C = C H B
6 5 oveq2d ⊢ R ∈ CRingOps ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A H B H C = A H C H B
7 crngorngo ⊢ R ∈ CRingOps → R ∈ RingOps
8 1 2 3 rngoass ⊢ R ∈ RingOps ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A H B H C = A H B H C
9 7 8 sylan ⊢ R ∈ CRingOps ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A H B H C = A H B H C
10 1 2 3 rngoass ⊢ R ∈ RingOps ∧ A ∈ X ∧ C ∈ X ∧ B ∈ X → A H C H B = A H C H B
11 10 3exp2 ⊢ R ∈ RingOps → A ∈ X → C ∈ X → B ∈ X → A H C H B = A H C H B
12 11 com34 ⊢ R ∈ RingOps → A ∈ X → B ∈ X → C ∈ X → A H C H B = A H C H B
13 12 3imp2 ⊢ R ∈ RingOps ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A H C H B = A H C H B
14 7 13 sylan ⊢ R ∈ CRingOps ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A H C H B = A H C H B
15 6 9 14 3eqtr4d ⊢ R ∈ CRingOps ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A H B H C = A H C H B