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

Definition df-gdiv 28283
 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 28279 . 2 class /𝑔
2 vg . . 3 setvar 𝑔
3 cgr 28276 . . 3 class GrpOp
4 vx . . . 4 setvar 𝑥
5 vy . . . 4 setvar 𝑦
62cv 1537 . . . . 5 class 𝑔
76crn 5524 . . . 4 class ran 𝑔
84cv 1537 . . . . 5 class 𝑥
95cv 1537 . . . . . 6 class 𝑦
10 cgn 28278 . . . . . . 7 class inv
116, 10cfv 6328 . . . . . 6 class (inv‘𝑔)
129, 11cfv 6328 . . . . 5 class ((inv‘𝑔)‘𝑦)
138, 12, 6co 7139 . . . 4 class (𝑥𝑔((inv‘𝑔)‘𝑦))
144, 5, 7, 7, 13cmpo 7141 . . 3 class (𝑥 ∈ ran 𝑔, 𝑦 ∈ ran 𝑔 ↦ (𝑥𝑔((inv‘𝑔)‘𝑦)))
152, 3, 14cmpt 5113 . 2 class (𝑔 ∈ GrpOp ↦ (𝑥 ∈ ran 𝑔, 𝑦 ∈ ran 𝑔 ↦ (𝑥𝑔((inv‘𝑔)‘𝑦))))
161, 15wceq 1538 1 wff /𝑔 = (𝑔 ∈ GrpOp ↦ (𝑥 ∈ ran 𝑔, 𝑦 ∈ ran 𝑔 ↦ (𝑥𝑔((inv‘𝑔)‘𝑦))))
 Colors of variables: wff setvar class This definition is referenced by:  grpodivfval  28321  vsfval  28420
 Copyright terms: Public domain W3C validator