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