MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-gdiv Structured version   Visualization version   GIF version

Definition df-gdiv 26500
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.)
Assertion
Ref Expression
df-gdiv /𝑔 = (𝑔 ∈ GrpOp ↦ (𝑥 ∈ ran 𝑔, 𝑦 ∈ ran 𝑔 ↦ (𝑥𝑔((inv‘𝑔)‘𝑦))))
Distinct variable group:   𝑥,𝑔,𝑦

Detailed syntax breakdown of Definition df-gdiv
StepHypRef Expression
1 cgs 26496 . 2 class /𝑔
2 vg . . 3 setvar 𝑔
3 cgr 26493 . . 3 class GrpOp
4 vx . . . 4 setvar 𝑥
5 vy . . . 4 setvar 𝑦
62cv 1473 . . . . 5 class 𝑔
76crn 5029 . . . 4 class ran 𝑔
84cv 1473 . . . . 5 class 𝑥
95cv 1473 . . . . . 6 class 𝑦
10 cgn 26495 . . . . . . 7 class inv
116, 10cfv 5790 . . . . . 6 class (inv‘𝑔)
129, 11cfv 5790 . . . . 5 class ((inv‘𝑔)‘𝑦)
138, 12, 6co 6527 . . . 4 class (𝑥𝑔((inv‘𝑔)‘𝑦))
144, 5, 7, 7, 13cmpt2 6529 . . 3 class (𝑥 ∈ ran 𝑔, 𝑦 ∈ ran 𝑔 ↦ (𝑥𝑔((inv‘𝑔)‘𝑦)))
152, 3, 14cmpt 4637 . 2 class (𝑔 ∈ GrpOp ↦ (𝑥 ∈ ran 𝑔, 𝑦 ∈ ran 𝑔 ↦ (𝑥𝑔((inv‘𝑔)‘𝑦))))
161, 15wceq 1474 1 wff /𝑔 = (𝑔 ∈ GrpOp ↦ (𝑥 ∈ ran 𝑔, 𝑦 ∈ ran 𝑔 ↦ (𝑥𝑔((inv‘𝑔)‘𝑦))))
Colors of variables: wff setvar class
This definition is referenced by:  grpodivfval  26538  vsfval  26658
  Copyright terms: Public domain W3C validator