Metamath Proof Explorer

Theorem ablo4pnp

Description: A commutative/associative law for Abelian groups. (Contributed by Jeff Madsen, 11-Jun-2010)

Ref Expression
Hypotheses abl4pnp.1 ⊢ X = ran ⁡ G
abl4pnp.2 ⊢ D = / g ⁡ G
Assertion ablo4pnp ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ F ∈ X → A G B D C G F = A D C G B D F

Proof

Step Hyp Ref Expression
1 abl4pnp.1 ⊢ X = ran ⁡ G
2 abl4pnp.2 ⊢ D = / g ⁡ G
3 df-3an ⊢ A ∈ X ∧ B ∈ X ∧ C ∈ X ↔ A ∈ X ∧ B ∈ X ∧ C ∈ X
4 1 2 ablomuldiv ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A G B D C = A D C G B
5 3 4 sylan2br ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A G B D C = A D C G B
6 5 adantrrr ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ F ∈ X → A G B D C = A D C G B
7 6 oveq1d ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ F ∈ X → A G B D C D F = A D C G B D F
8 ablogrpo ⊢ G ∈ AbelOp → G ∈ GrpOp
9 1 grpocl ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X → A G B ∈ X
10 9 3expib ⊢ G ∈ GrpOp → A ∈ X ∧ B ∈ X → A G B ∈ X
11 8 10 syl ⊢ G ∈ AbelOp → A ∈ X ∧ B ∈ X → A G B ∈ X
12 11 anim1d ⊢ G ∈ AbelOp → A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ F ∈ X → A G B ∈ X ∧ C ∈ X ∧ F ∈ X
13 3anass ⊢ A G B ∈ X ∧ C ∈ X ∧ F ∈ X ↔ A G B ∈ X ∧ C ∈ X ∧ F ∈ X
14 12 13 imbitrrdi ⊢ G ∈ AbelOp → A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ F ∈ X → A G B ∈ X ∧ C ∈ X ∧ F ∈ X
15 14 imp ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ F ∈ X → A G B ∈ X ∧ C ∈ X ∧ F ∈ X
16 1 2 ablodivdiv4 ⊢ G ∈ AbelOp ∧ A G B ∈ X ∧ C ∈ X ∧ F ∈ X → A G B D C D F = A G B D C G F
17 15 16 syldan ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ F ∈ X → A G B D C D F = A G B D C G F
18 1 2 grpodivcl ⊢ G ∈ GrpOp ∧ A ∈ X ∧ C ∈ X → A D C ∈ X
19 18 3expib ⊢ G ∈ GrpOp → A ∈ X ∧ C ∈ X → A D C ∈ X
20 19 anim1d ⊢ G ∈ GrpOp → A ∈ X ∧ C ∈ X ∧ B ∈ X ∧ F ∈ X → A D C ∈ X ∧ B ∈ X ∧ F ∈ X
21 an4 ⊢ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ F ∈ X ↔ A ∈ X ∧ C ∈ X ∧ B ∈ X ∧ F ∈ X
22 3anass ⊢ A D C ∈ X ∧ B ∈ X ∧ F ∈ X ↔ A D C ∈ X ∧ B ∈ X ∧ F ∈ X
23 20 21 22 3imtr4g ⊢ G ∈ GrpOp → A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ F ∈ X → A D C ∈ X ∧ B ∈ X ∧ F ∈ X
24 23 imp ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ F ∈ X → A D C ∈ X ∧ B ∈ X ∧ F ∈ X
25 1 2 grpomuldivass ⊢ G ∈ GrpOp ∧ A D C ∈ X ∧ B ∈ X ∧ F ∈ X → A D C G B D F = A D C G B D F
26 24 25 syldan ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ F ∈ X → A D C G B D F = A D C G B D F
27 8 26 sylan ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ F ∈ X → A D C G B D F = A D C G B D F
28 7 17 27 3eqtr3d ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ F ∈ X → A G B D C G F = A D C G B D F