Metamath Proof Explorer

Theorem grponpcan

Description: Cancellation law for group division. ( npcan analog.) (Contributed by NM, 15-Feb-2008) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 grpdivf.1 ⊢ X = ran ⁡ G
2 grpdivf.3 ⊢ D = / g ⁡ G
3 eqid ⊢ inv ⁡ G = inv ⁡ G
4 1 3 2 grpodivval ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X → A D B = A G inv ⁡ G ⁡ B
5 4 oveq1d ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X → A D B G B = A G inv ⁡ G ⁡ B G B
6 simp1 ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X → G ∈ GrpOp
7 simp2 ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X → A ∈ X
8 1 3 grpoinvcl ⊢ G ∈ GrpOp ∧ B ∈ X → inv ⁡ G ⁡ B ∈ X
9 8 3adant2 ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X → inv ⁡ G ⁡ B ∈ X
10 simp3 ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X → B ∈ X
11 1 grpoass ⊢ G ∈ GrpOp ∧ A ∈ X ∧ inv ⁡ G ⁡ B ∈ X ∧ B ∈ X → A G inv ⁡ G ⁡ B G B = A G inv ⁡ G ⁡ B G B
12 6 7 9 10 11 syl13anc ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X → A G inv ⁡ G ⁡ B G B = A G inv ⁡ G ⁡ B G B
13 eqid ⊢ GId ⁡ G = GId ⁡ G
14 1 13 3 grpolinv ⊢ G ∈ GrpOp ∧ B ∈ X → inv ⁡ G ⁡ B G B = GId ⁡ G
15 14 oveq2d ⊢ G ∈ GrpOp ∧ B ∈ X → A G inv ⁡ G ⁡ B G B = A G GId ⁡ G
16 15 3adant2 ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X → A G inv ⁡ G ⁡ B G B = A G GId ⁡ G
17 1 13 grporid ⊢ G ∈ GrpOp ∧ A ∈ X → A G GId ⁡ G = A
18 17 3adant3 ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X → A G GId ⁡ G = A
19 16 18 eqtrd ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X → A G inv ⁡ G ⁡ B G B = A
20 12 19 eqtrd ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X → A G inv ⁡ G ⁡ B G B = A
21 5 20 eqtrd ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X → A D B G B = A