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

Definition df-gid 26494
Description: Define a function that maps a group operation to the group's identity element. (Contributed by FL, 5-Feb-2010.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.)
Assertion
Ref Expression
df-gid GId = (𝑔 ∈ V ↦ (𝑢 ∈ ran 𝑔𝑥 ∈ ran 𝑔((𝑢𝑔𝑥) = 𝑥 ∧ (𝑥𝑔𝑢) = 𝑥)))
Distinct variable group:   𝑢,𝑔,𝑥

Detailed syntax breakdown of Definition df-gid
StepHypRef Expression
1 cgi 26490 . 2 class GId
2 vg . . 3 setvar 𝑔
3 cvv 3168 . . 3 class V
4 vu . . . . . . . . 9 setvar 𝑢
54cv 1473 . . . . . . . 8 class 𝑢
6 vx . . . . . . . . 9 setvar 𝑥
76cv 1473 . . . . . . . 8 class 𝑥
82cv 1473 . . . . . . . 8 class 𝑔
95, 7, 8co 6523 . . . . . . 7 class (𝑢𝑔𝑥)
109, 7wceq 1474 . . . . . 6 wff (𝑢𝑔𝑥) = 𝑥
117, 5, 8co 6523 . . . . . . 7 class (𝑥𝑔𝑢)
1211, 7wceq 1474 . . . . . 6 wff (𝑥𝑔𝑢) = 𝑥
1310, 12wa 382 . . . . 5 wff ((𝑢𝑔𝑥) = 𝑥 ∧ (𝑥𝑔𝑢) = 𝑥)
148crn 5025 . . . . 5 class ran 𝑔
1513, 6, 14wral 2891 . . . 4 wff 𝑥 ∈ ran 𝑔((𝑢𝑔𝑥) = 𝑥 ∧ (𝑥𝑔𝑢) = 𝑥)
1615, 4, 14crio 6484 . . 3 class (𝑢 ∈ ran 𝑔𝑥 ∈ ran 𝑔((𝑢𝑔𝑥) = 𝑥 ∧ (𝑥𝑔𝑢) = 𝑥))
172, 3, 16cmpt 4633 . 2 class (𝑔 ∈ V ↦ (𝑢 ∈ ran 𝑔𝑥 ∈ ran 𝑔((𝑢𝑔𝑥) = 𝑥 ∧ (𝑥𝑔𝑢) = 𝑥)))
181, 17wceq 1474 1 wff GId = (𝑔 ∈ V ↦ (𝑢 ∈ ran 𝑔𝑥 ∈ ran 𝑔((𝑢𝑔𝑥) = 𝑥 ∧ (𝑥𝑔𝑢) = 𝑥)))
Colors of variables: wff setvar class
This definition is referenced by:  gidval  26512
  Copyright terms: Public domain W3C validator