This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem grpodivdiv

Description: Double group division. (Contributed by NM, 24-Feb-2008) (New usage is discouraged.)

Ref Expression
Hypotheses grpdivf.1 ⊢ X = ran ⁡ G
grpdivf.3 ⊢ D = / g ⁡ G
Assertion grpodivdiv ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D B D C = A G C D B

Proof

Step Hyp Ref Expression
1 grpdivf.1 ⊢ X = ran ⁡ G
2 grpdivf.3 ⊢ D = / g ⁡ G
3 simpl ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → G ∈ GrpOp
4 simpr1 ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A ∈ X
5 1 2 grpodivcl ⊢ G ∈ GrpOp ∧ B ∈ X ∧ C ∈ X → B D C ∈ X
6 5 3adant3r1 ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → B D C ∈ X
7 eqid ⊢ inv ⁡ G = inv ⁡ G
8 1 7 2 grpodivval ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B D C ∈ X → A D B D C = A G inv ⁡ G ⁡ B D C
9 3 4 6 8 syl3anc ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D B D C = A G inv ⁡ G ⁡ B D C
10 1 7 2 grpoinvdiv ⊢ G ∈ GrpOp ∧ B ∈ X ∧ C ∈ X → inv ⁡ G ⁡ B D C = C D B
11 10 3adant3r1 ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → inv ⁡ G ⁡ B D C = C D B
12 11 oveq2d ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A G inv ⁡ G ⁡ B D C = A G C D B
13 9 12 eqtrd ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D B D C = A G C D B