Metamath Proof Explorer

Theorem ablo4

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 ablo4 ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ D ∈ X → A G B G C G D = A G C G B G D

Proof

Step Hyp Ref Expression
1 ablcom.1 ⊢ X = ran ⁡ G
2 simprll ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ D ∈ X → A ∈ X
3 simprlr ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ D ∈ X → B ∈ X
4 simprrl ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ D ∈ X → C ∈ X
5 2 3 4 3jca ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ D ∈ X → A ∈ X ∧ B ∈ X ∧ C ∈ X
6 1 ablo32 ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A G B G C = A G C G B
7 5 6 syldan ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ D ∈ X → A G B G C = A G C G B
8 7 oveq1d ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ D ∈ X → A G B G C G D = A G C G B G D
9 ablogrpo ⊢ G ∈ AbelOp → G ∈ GrpOp
10 1 grpocl ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X → A G B ∈ X
11 10 3expb ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X → A G B ∈ X
12 11 adantrr ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ D ∈ X → A G B ∈ X
13 simprrl ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ D ∈ X → C ∈ X
14 simprrr ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ D ∈ X → D ∈ X
15 12 13 14 3jca ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ D ∈ X → A G B ∈ X ∧ C ∈ X ∧ D ∈ X
16 1 grpoass ⊢ G ∈ GrpOp ∧ A G B ∈ X ∧ C ∈ X ∧ D ∈ X → A G B G C G D = A G B G C G D
17 15 16 syldan ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ D ∈ X → A G B G C G D = A G B G C G D
18 9 17 sylan ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ D ∈ X → A G B G C G D = A G B G C G D
19 1 grpocl ⊢ G ∈ GrpOp ∧ A ∈ X ∧ C ∈ X → A G C ∈ X
20 19 3expb ⊢ G ∈ GrpOp ∧ A ∈ X ∧ C ∈ X → A G C ∈ X
21 20 adantrlr ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A G C ∈ X
22 21 adantrrr ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ D ∈ X → A G C ∈ X
23 simprlr ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ D ∈ X → B ∈ X
24 22 23 14 3jca ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ D ∈ X → A G C ∈ X ∧ B ∈ X ∧ D ∈ X
25 1 grpoass ⊢ G ∈ GrpOp ∧ A G C ∈ X ∧ B ∈ X ∧ D ∈ X → A G C G B G D = A G C G B G D
26 24 25 syldan ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ D ∈ X → A G C G B G D = A G C G B G D
27 9 26 sylan ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ D ∈ X → A G C G B G D = A G C G B G D
28 8 18 27 3eqtr3d ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ D ∈ X → A G B G C G D = A G C G B G D
29 28 3impb ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ D ∈ X → A G B G C G D = A G C G B G D