Metamath Proof Explorer

Theorem ablomuldiv

Description: Law for group multiplication and division. (Contributed by NM, 15-Feb-2008) (New usage is discouraged.)

Ref Expression
Hypotheses abldiv.1 ⊢ X = ran ⁡ G
abldiv.3 ⊢ D = / g ⁡ G
Assertion ablomuldiv ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A G B D C = A D C G B

Proof

Step Hyp Ref Expression
1 abldiv.1 ⊢ X = ran ⁡ G
2 abldiv.3 ⊢ D = / g ⁡ G
3 1 ablocom ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X → A G B = B G A
4 3 3adant3r3 ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A G B = B G A
5 4 oveq1d ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A G B D C = B G A D C
6 3ancoma ⊢ A ∈ X ∧ B ∈ X ∧ C ∈ X ↔ B ∈ X ∧ A ∈ X ∧ C ∈ X
7 ablogrpo ⊢ G ∈ AbelOp → G ∈ GrpOp
8 1 2 grpomuldivass ⊢ G ∈ GrpOp ∧ B ∈ X ∧ A ∈ X ∧ C ∈ X → B G A D C = B G A D C
9 7 8 sylan ⊢ G ∈ AbelOp ∧ B ∈ X ∧ A ∈ X ∧ C ∈ X → B G A D C = B G A D C
10 6 9 sylan2b ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → B G A D C = B G A D C
11 simpr2 ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → B ∈ X
12 1 2 grpodivcl ⊢ G ∈ GrpOp ∧ A ∈ X ∧ C ∈ X → A D C ∈ X
13 7 12 syl3an1 ⊢ G ∈ AbelOp ∧ A ∈ X ∧ C ∈ X → A D C ∈ X
14 13 3adant3r2 ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D C ∈ X
15 11 14 jca ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → B ∈ X ∧ A D C ∈ X
16 1 ablocom ⊢ G ∈ AbelOp ∧ B ∈ X ∧ A D C ∈ X → B G A D C = A D C G B
17 16 3expb ⊢ G ∈ AbelOp ∧ B ∈ X ∧ A D C ∈ X → B G A D C = A D C G B
18 15 17 syldan ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → B G A D C = A D C G B
19 5 10 18 3eqtrd ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A G B D C = A D C G B