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

Metamath Proof Explorer

Theorem grpodivid

Description: Division of a group member by itself. (Contributed by NM, 15-Feb-2008) (New usage is discouraged.)

Ref Expression
Hypotheses grpdivf.1 ⊢ X = ran ⁡ G
grpdivf.3 ⊢ D = / g ⁡ G
grpdivid.3 ⊢ U = GId ⁡ G
Assertion grpodivid ⊢ G ∈ GrpOp ∧ A ∈ X → A D A = U

Proof

Step Hyp Ref Expression
1 grpdivf.1 ⊢ X = ran ⁡ G
2 grpdivf.3 ⊢ D = / g ⁡ G
3 grpdivid.3 ⊢ U = GId ⁡ G
4 eqid ⊢ inv ⁡ G = inv ⁡ G
5 1 4 2 grpodivval ⊢ G ∈ GrpOp ∧ A ∈ X ∧ A ∈ X → A D A = A G inv ⁡ G ⁡ A
6 5 3anidm23 ⊢ G ∈ GrpOp ∧ A ∈ X → A D A = A G inv ⁡ G ⁡ A
7 1 3 4 grporinv ⊢ G ∈ GrpOp ∧ A ∈ X → A G inv ⁡ G ⁡ A = U
8 6 7 eqtrd ⊢ G ∈ GrpOp ∧ A ∈ X → A D A = U