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$