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→AGBGC=AGCGB

Proof

Step Hyp Ref Expression
1 ablcom.1 ⊢X=ran⁡G
2 1 ablocom ⊢G∈AbelOp∧B∈X∧C∈X→BGC=CGB
3 2 3adant3r1 ⊢G∈AbelOp∧A∈X∧B∈X∧C∈X→BGC=CGB
4 3 oveq2d ⊢G∈AbelOp∧A∈X∧B∈X∧C∈X→AGBGC=AGCGB
5 ablogrpo ⊢G∈AbelOp→G∈GrpOp
6 1 grpoass ⊢G∈GrpOp∧A∈X∧B∈X∧C∈X→AGBGC=AGBGC
7 5 6 sylan ⊢G∈AbelOp∧A∈X∧B∈X∧C∈X→AGBGC=AGBGC
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→AGCGB=AGCGB
10 8 9 sylan2b ⊢G∈GrpOp∧A∈X∧B∈X∧C∈X→AGCGB=AGCGB
11 5 10 sylan ⊢G∈AbelOp∧A∈X∧B∈X∧C∈X→AGCGB=AGCGB
12 4 7 11 3eqtr4d ⊢G∈AbelOp∧A∈X∧B∈X∧C∈X→AGBGC=AGCGB