Metamath Proof Explorer

Theorem ablo32

Description: Commutative/associative law for Abelian groups. (Contributed by NM, 26-Apr-2007) (New usage is discouraged.)

Ref Expression
Hypothesis ablcom.1 ⊢ X = ran ⁡ G
Assertion ablo32 ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A G B G C = A G C G B

Proof

Step Hyp Ref Expression
1 ablcom.1 ⊢ X = ran ⁡ G
2 1 ablocom ⊢ G ∈ AbelOp ∧ B ∈ X ∧ C ∈ X → B G C = C G B
3 2 3adant3r1 ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → B G C = C G B
4 3 oveq2d ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A G B G C = A G C G B
5 ablogrpo ⊢ G ∈ AbelOp → G ∈ GrpOp
6 1 grpoass ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A G B G C = A G B G C
7 5 6 sylan ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A G B G C = A G B G C
8 3ancomb ⊢ A ∈ X ∧ B ∈ X ∧ C ∈ X ↔ A ∈ X ∧ C ∈ X ∧ B ∈ X
9 1 grpoass ⊢ G ∈ GrpOp ∧ A ∈ X ∧ C ∈ X ∧ B ∈ X → A G C G B = A G C G B
10 8 9 sylan2b ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A G C G B = A G C G B
11 5 10 sylan ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A G C G B = A G C G B
12 4 7 11 3eqtr4d ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A G B G C = A G C G B