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

Definition df-ginv 26733
Description: Define a function that maps a group operation to the group's inverse function. (Contributed by NM, 26-Oct-2006.) (New usage is discouraged.)
Assertion
Ref Expression
df-ginv inv = (𝑔 ∈ GrpOp ↦ (𝑥 ∈ ran 𝑔 ↦ (𝑧 ∈ ran 𝑔(𝑧𝑔𝑥) = (GId‘𝑔))))
Distinct variable group:   𝑥,𝑔,𝑧

Detailed syntax breakdown of Definition df-ginv
StepHypRef Expression
1 cgn 26729 . 2 class inv
2 vg . . 3 setvar 𝑔
3 cgr 26727 . . 3 class GrpOp
4 vx . . . 4 setvar 𝑥
52cv 1474 . . . . 5 class 𝑔
65crn 5039 . . . 4 class ran 𝑔
7 vz . . . . . . . 8 setvar 𝑧
87cv 1474 . . . . . . 7 class 𝑧
94cv 1474 . . . . . . 7 class 𝑥
108, 9, 5co 6549 . . . . . 6 class (𝑧𝑔𝑥)
11 cgi 26728 . . . . . . 7 class GId
125, 11cfv 5804 . . . . . 6 class (GId‘𝑔)
1310, 12wceq 1475 . . . . 5 wff (𝑧𝑔𝑥) = (GId‘𝑔)
1413, 7, 6crio 6510 . . . 4 class (𝑧 ∈ ran 𝑔(𝑧𝑔𝑥) = (GId‘𝑔))
154, 6, 14cmpt 4643 . . 3 class (𝑥 ∈ ran 𝑔 ↦ (𝑧 ∈ ran 𝑔(𝑧𝑔𝑥) = (GId‘𝑔)))
162, 3, 15cmpt 4643 . 2 class (𝑔 ∈ GrpOp ↦ (𝑥 ∈ ran 𝑔 ↦ (𝑧 ∈ ran 𝑔(𝑧𝑔𝑥) = (GId‘𝑔))))
171, 16wceq 1475 1 wff inv = (𝑔 ∈ GrpOp ↦ (𝑥 ∈ ran 𝑔 ↦ (𝑧 ∈ ran 𝑔(𝑧𝑔𝑥) = (GId‘𝑔))))
Colors of variables: wff setvar class
This definition is referenced by:  grpoinvfval  26760
  Copyright terms: Public domain W3C validator