# Metamath Proof Explorer

## Theorem ablodivdiv4

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

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

### Proof

Step Hyp Ref Expression
1 abldiv.1 $⊢ X = ran ⁡ G$
2 abldiv.3 $⊢ D = / g ⁡ G$
3 ablogrpo $⊢ G ∈ AbelOp → G ∈ GrpOp$
4 simpl $⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → G ∈ GrpOp$
5 1 2 grpodivcl $⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X → A D B ∈ X$
6 5 3adant3r3 $⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D B ∈ X$
7 simpr3 $⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → C ∈ X$
8 eqid $⊢ inv ⁡ G = inv ⁡ G$
9 1 8 2 grpodivval $⊢ G ∈ GrpOp ∧ A D B ∈ X ∧ C ∈ X → A D B D C = A D B G inv ⁡ G ⁡ C$
10 4 6 7 9 syl3anc $⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D B D C = A D B G inv ⁡ G ⁡ C$
11 3 10 sylan $⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D B D C = A D B G inv ⁡ G ⁡ C$
12 simpr1 $⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A ∈ X$
13 simpr2 $⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → B ∈ X$
14 simp3 $⊢ A ∈ X ∧ B ∈ X ∧ C ∈ X → C ∈ X$
15 1 8 grpoinvcl $⊢ G ∈ GrpOp ∧ C ∈ X → inv ⁡ G ⁡ C ∈ X$
16 3 14 15 syl2an $⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → inv ⁡ G ⁡ C ∈ X$
17 12 13 16 3jca $⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A ∈ X ∧ B ∈ X ∧ inv ⁡ G ⁡ C ∈ X$
18 1 2 ablodivdiv $⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ inv ⁡ G ⁡ C ∈ X → A D B D inv ⁡ G ⁡ C = A D B G inv ⁡ G ⁡ C$
19 17 18 syldan $⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D B D inv ⁡ G ⁡ C = A D B G inv ⁡ G ⁡ C$
20 1 8 2 grpodivinv $⊢ G ∈ GrpOp ∧ B ∈ X ∧ C ∈ X → B D inv ⁡ G ⁡ C = B G C$
21 3 20 syl3an1 $⊢ G ∈ AbelOp ∧ B ∈ X ∧ C ∈ X → B D inv ⁡ G ⁡ C = B G C$
22 21 3adant3r1 $⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → B D inv ⁡ G ⁡ C = B G C$
23 22 oveq2d $⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D B D inv ⁡ G ⁡ C = A D B G C$
24 11 19 23 3eqtr2d $⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D B D C = A D B G C$