Metamath Proof Explorer

Definition df-gdiv

Description: Define a function that maps a group operation to the group's division (or subtraction) operation. (Contributed by NM, 15-Feb-2008) (New usage is discouraged.)

Ref Expression
Assertion df-gdiv ⊢ / g = g ∈ GrpOp ⟼ x ∈ ran ⁡ g , y ∈ ran ⁡ g ⟼ x g inv ⁡ g ⁡ y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cgs class / g
1 vg setvar g
2 cgr class GrpOp
3 vx setvar x
4 1 cv setvar g
5 4 crn class ran ⁡ g
6 vy setvar y
7 3 cv setvar x
8 cgn class inv
9 4 8 cfv class inv ⁡ g
10 6 cv setvar y
11 10 9 cfv class inv ⁡ g ⁡ y
12 7 11 4 co class x g inv ⁡ g ⁡ y
13 3 6 5 5 12 cmpo class x ∈ ran ⁡ g , y ∈ ran ⁡ g ⟼ x g inv ⁡ g ⁡ y
14 1 2 13 cmpt class g ∈ GrpOp ⟼ x ∈ ran ⁡ g , y ∈ ran ⁡ g ⟼ x g inv ⁡ g ⁡ y
15 0 14 wceq wff / g = g ∈ GrpOp ⟼ x ∈ ran ⁡ g , y ∈ ran ⁡ g ⟼ x g inv ⁡ g ⁡ y