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

Definition df-minusg 17473
 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 17470 . 2 class invg
2 vg . . 3 setvar 𝑔
3 cvv 3231 . . 3 class V
4 vx . . . 4 setvar 𝑥
52cv 1522 . . . . 5 class 𝑔
6 cbs 15904 . . . . 5 class Base
75, 6cfv 5926 . . . 4 class (Base‘𝑔)
8 vw . . . . . . . 8 setvar 𝑤
98cv 1522 . . . . . . 7 class 𝑤
104cv 1522 . . . . . . 7 class 𝑥
11 cplusg 15988 . . . . . . . 8 class +g
125, 11cfv 5926 . . . . . . 7 class (+g𝑔)
139, 10, 12co 6690 . . . . . 6 class (𝑤(+g𝑔)𝑥)
14 c0g 16147 . . . . . . 7 class 0g
155, 14cfv 5926 . . . . . 6 class (0g𝑔)
1613, 15wceq 1523 . . . . 5 wff (𝑤(+g𝑔)𝑥) = (0g𝑔)
1716, 8, 7crio 6650 . . . 4 class (𝑤 ∈ (Base‘𝑔)(𝑤(+g𝑔)𝑥) = (0g𝑔))
184, 7, 17cmpt 4762 . . 3 class (𝑥 ∈ (Base‘𝑔) ↦ (𝑤 ∈ (Base‘𝑔)(𝑤(+g𝑔)𝑥) = (0g𝑔)))
192, 3, 18cmpt 4762 . 2 class (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔) ↦ (𝑤 ∈ (Base‘𝑔)(𝑤(+g𝑔)𝑥) = (0g𝑔))))
201, 19wceq 1523 1 wff invg = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔) ↦ (𝑤 ∈ (Base‘𝑔)(𝑤(+g𝑔)𝑥) = (0g𝑔))))
 Colors of variables: wff setvar class This definition is referenced by:  grpinvfval  17507
 Copyright terms: Public domain W3C validator