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

Metamath Proof Explorer

Definition df-sbg

Description: Define group subtraction (also called division for multiplicative groups). (Contributed by NM, 31-Mar-2014)

Ref Expression
Assertion df-sbg ⊢ - 𝑔 = g ∈ V ⟼ x ∈ Base g , y ∈ Base g ⟼ x + g inv g ⁡ g ⁡ y

Detailed syntax breakdown

Step Hyp Ref Expression
0 csg class - 𝑔
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 vy setvar y
8 3 cv setvar x
9 cplusg class + 𝑔
10 5 9 cfv class + g
11 cminusg class inv g
12 5 11 cfv class inv g ⁡ g
13 7 cv setvar y
14 13 12 cfv class inv g ⁡ g ⁡ y
15 8 14 10 co class x + g inv g ⁡ g ⁡ y
16 3 7 6 6 15 cmpo class x ∈ Base g , y ∈ Base g ⟼ x + g inv g ⁡ g ⁡ y
17 1 2 16 cmpt class g ∈ V ⟼ x ∈ Base g , y ∈ Base g ⟼ x + g inv g ⁡ g ⁡ y
18 0 17 wceq wff - 𝑔 = g ∈ V ⟼ x ∈ Base g , y ∈ Base g ⟼ x + g inv g ⁡ g ⁡ y