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 18103
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 18100 . 2 class invg
2 vg . . 3 setvar 𝑔
3 cvv 3444 . . 3 class V
4 vx . . . 4 setvar 𝑥
52cv 1537 . . . . 5 class 𝑔
6 cbs 16479 . . . . 5 class Base
75, 6cfv 6328 . . . 4 class (Base‘𝑔)
8 vw . . . . . . . 8 setvar 𝑤
98cv 1537 . . . . . . 7 class 𝑤
104cv 1537 . . . . . . 7 class 𝑥
11 cplusg 16561 . . . . . . . 8 class +g
125, 11cfv 6328 . . . . . . 7 class (+g𝑔)
139, 10, 12co 7139 . . . . . 6 class (𝑤(+g𝑔)𝑥)
14 c0g 16709 . . . . . . 7 class 0g
155, 14cfv 6328 . . . . . 6 class (0g𝑔)
1613, 15wceq 1538 . . . . 5 wff (𝑤(+g𝑔)𝑥) = (0g𝑔)
1716, 8, 7crio 7096 . . . 4 class (𝑤 ∈ (Base‘𝑔)(𝑤(+g𝑔)𝑥) = (0g𝑔))
184, 7, 17cmpt 5113 . . 3 class (𝑥 ∈ (Base‘𝑔) ↦ (𝑤 ∈ (Base‘𝑔)(𝑤(+g𝑔)𝑥) = (0g𝑔)))
192, 3, 18cmpt 5113 . 2 class (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔) ↦ (𝑤 ∈ (Base‘𝑔)(𝑤(+g𝑔)𝑥) = (0g𝑔))))
201, 19wceq 1538 1 wff invg = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔) ↦ (𝑤 ∈ (Base‘𝑔)(𝑤(+g𝑔)𝑥) = (0g𝑔))))
Colors of variables: wff setvar class
This definition is referenced by:  grpinvfval  18138  grpinvfvalALT  18139
  Copyright terms: Public domain W3C validator