This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-minusg

Description: Define inverse of group element. (Contributed by NM, 24-Aug-2011)

Ref Expression
Assertion df-minusg ⊢ inv g = g ∈ V ⟼ x ∈ Base g ⟼ ι w ∈ Base g | w + g x = 0 g

Detailed syntax breakdown

Step Hyp Ref Expression
0 cminusg class inv g
1 vg setvar g
2 cvv class V
3 vx setvar x
4 cbs class Base
5 1 cv setvar g
6 5 4 cfv class Base g
7 vw setvar w
8 7 cv setvar w
9 cplusg class + 𝑔
10 5 9 cfv class + g
11 3 cv setvar x
12 8 11 10 co class w + g x
13 c0g class 0 𝑔
14 5 13 cfv class 0 g
15 12 14 wceq wff w + g x = 0 g
16 15 7 6 crio class ι w ∈ Base g | w + g x = 0 g
17 3 6 16 cmpt class x ∈ Base g ⟼ ι w ∈ Base g | w + g x = 0 g
18 1 2 17 cmpt class g ∈ V ⟼ x ∈ Base g ⟼ ι w ∈ Base g | w + g x = 0 g
19 0 18 wceq wff inv g = g ∈ V ⟼ x ∈ Base g ⟼ ι w ∈ Base g | w + g x = 0 g