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

Definition df-minusg 17627
Description: Define inverse of group element. (Contributed by NM, 24-Aug-2011.)
Assertion
Ref Expression
df-minusg invg = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔) ↦ (𝑤 ∈ (Base‘𝑔)(𝑤(+g𝑔)𝑥) = (0g𝑔))))
Distinct variable group:   𝑤,𝑔,𝑥

Detailed syntax breakdown of Definition df-minusg
StepHypRef Expression
1 cminusg 17624 . 2 class invg
2 vg . . 3 setvar 𝑔
3 cvv 3391 . . 3 class V
4 vx . . . 4 setvar 𝑥
52cv 1636 . . . . 5 class 𝑔
6 cbs 16064 . . . . 5 class Base
75, 6cfv 6097 . . . 4 class (Base‘𝑔)
8 vw . . . . . . . 8 setvar 𝑤
98cv 1636 . . . . . . 7 class 𝑤
104cv 1636 . . . . . . 7 class 𝑥
11 cplusg 16149 . . . . . . . 8 class +g
125, 11cfv 6097 . . . . . . 7 class (+g𝑔)
139, 10, 12co 6870 . . . . . 6 class (𝑤(+g𝑔)𝑥)
14 c0g 16301 . . . . . . 7 class 0g
155, 14cfv 6097 . . . . . 6 class (0g𝑔)
1613, 15wceq 1637 . . . . 5 wff (𝑤(+g𝑔)𝑥) = (0g𝑔)
1716, 8, 7crio 6830 . . . 4 class (𝑤 ∈ (Base‘𝑔)(𝑤(+g𝑔)𝑥) = (0g𝑔))
184, 7, 17cmpt 4923 . . 3 class (𝑥 ∈ (Base‘𝑔) ↦ (𝑤 ∈ (Base‘𝑔)(𝑤(+g𝑔)𝑥) = (0g𝑔)))
192, 3, 18cmpt 4923 . 2 class (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔) ↦ (𝑤 ∈ (Base‘𝑔)(𝑤(+g𝑔)𝑥) = (0g𝑔))))
201, 19wceq 1637 1 wff invg = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔) ↦ (𝑤 ∈ (Base‘𝑔)(𝑤(+g𝑔)𝑥) = (0g𝑔))))
Colors of variables: wff setvar class
This definition is referenced by:  grpinvfval  17661
  Copyright terms: Public domain W3C validator