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

Metamath Proof Explorer

Theorem grpodivf

Description: Mapping for group division. (Contributed by NM, 10-Apr-2008) (Revised by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses grpdivf.1 ⊢ X = ran ⁡ G
grpdivf.3 ⊢ D = / g ⁡ G
Assertion grpodivf ⊢ G ∈ GrpOp → D : X × X ⟶ X

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 grpoinvcl ⊢ G ∈ GrpOp ∧ y ∈ X → inv ⁡ G ⁡ y ∈ X
5 4 3adant2 ⊢ G ∈ GrpOp ∧ x ∈ X ∧ y ∈ X → inv ⁡ G ⁡ y ∈ X
6 1 grpocl ⊢ G ∈ GrpOp ∧ x ∈ X ∧ inv ⁡ G ⁡ y ∈ X → x G inv ⁡ G ⁡ y ∈ X
7 5 6 syld3an3 ⊢ G ∈ GrpOp ∧ x ∈ X ∧ y ∈ X → x G inv ⁡ G ⁡ y ∈ X
8 7 3expib ⊢ G ∈ GrpOp → x ∈ X ∧ y ∈ X → x G inv ⁡ G ⁡ y ∈ X
9 8 ralrimivv ⊢ G ∈ GrpOp → ∀ x ∈ X ∀ y ∈ X x G inv ⁡ G ⁡ y ∈ X
10 eqid ⊢ x ∈ X , y ∈ X ⟼ x G inv ⁡ G ⁡ y = x ∈ X , y ∈ X ⟼ x G inv ⁡ G ⁡ y
11 10 fmpo ⊢ ∀ x ∈ X ∀ y ∈ X x G inv ⁡ G ⁡ y ∈ X ↔ x ∈ X , y ∈ X ⟼ x G inv ⁡ G ⁡ y : X × X ⟶ X
12 9 11 sylib ⊢ G ∈ GrpOp → x ∈ X , y ∈ X ⟼ x G inv ⁡ G ⁡ y : X × X ⟶ X
13 1 3 2 grpodivfval ⊢ G ∈ GrpOp → D = x ∈ X , y ∈ X ⟼ x G inv ⁡ G ⁡ y
14 13 feq1d ⊢ G ∈ GrpOp → D : X × X ⟶ X ↔ x ∈ X , y ∈ X ⟼ x G inv ⁡ G ⁡ y : X × X ⟶ X
15 12 14 mpbird ⊢ G ∈ GrpOp → D : X × X ⟶ X