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 18047
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 18044 . 2 class invg
2 vg . . 3 setvar 𝑔
3 cvv 3495 . . 3 class V
4 vx . . . 4 setvar 𝑥
52cv 1527 . . . . 5 class 𝑔
6 cbs 16473 . . . . 5 class Base
75, 6cfv 6349 . . . 4 class (Base‘𝑔)
8 vw . . . . . . . 8 setvar 𝑤
98cv 1527 . . . . . . 7 class 𝑤
104cv 1527 . . . . . . 7 class 𝑥
11 cplusg 16555 . . . . . . . 8 class +g
125, 11cfv 6349 . . . . . . 7 class (+g𝑔)
139, 10, 12co 7145 . . . . . 6 class (𝑤(+g𝑔)𝑥)
14 c0g 16703 . . . . . . 7 class 0g
155, 14cfv 6349 . . . . . 6 class (0g𝑔)
1613, 15wceq 1528 . . . . 5 wff (𝑤(+g𝑔)𝑥) = (0g𝑔)
1716, 8, 7crio 7102 . . . 4 class (𝑤 ∈ (Base‘𝑔)(𝑤(+g𝑔)𝑥) = (0g𝑔))
184, 7, 17cmpt 5138 . . 3 class (𝑥 ∈ (Base‘𝑔) ↦ (𝑤 ∈ (Base‘𝑔)(𝑤(+g𝑔)𝑥) = (0g𝑔)))
192, 3, 18cmpt 5138 . 2 class (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔) ↦ (𝑤 ∈ (Base‘𝑔)(𝑤(+g𝑔)𝑥) = (0g𝑔))))
201, 19wceq 1528 1 wff invg = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔) ↦ (𝑤 ∈ (Base‘𝑔)(𝑤(+g𝑔)𝑥) = (0g𝑔))))
Colors of variables: wff setvar class
This definition is referenced by:  grpinvfval  18082  grpinvfvalALT  18083
  Copyright terms: Public domain W3C validator