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 ↦ ( 𝑥 ∈ ( Base ‘ 𝑔 ) , 𝑦 ∈ ( Base ‘ 𝑔 ) ↦ ( 𝑥 ( +g𝑔 ) ( ( invg𝑔 ) ‘ 𝑦 ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 csg -g
1 vg 𝑔
2 cvv V
3 vx 𝑥
4 cbs Base
5 1 cv 𝑔
6 5 4 cfv ( Base ‘ 𝑔 )
7 vy 𝑦
8 3 cv 𝑥
9 cplusg +g
10 5 9 cfv ( +g𝑔 )
11 cminusg invg
12 5 11 cfv ( invg𝑔 )
13 7 cv 𝑦
14 13 12 cfv ( ( invg𝑔 ) ‘ 𝑦 )
15 8 14 10 co ( 𝑥 ( +g𝑔 ) ( ( invg𝑔 ) ‘ 𝑦 ) )
16 3 7 6 6 15 cmpo ( 𝑥 ∈ ( Base ‘ 𝑔 ) , 𝑦 ∈ ( Base ‘ 𝑔 ) ↦ ( 𝑥 ( +g𝑔 ) ( ( invg𝑔 ) ‘ 𝑦 ) ) )
17 1 2 16 cmpt ( 𝑔 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ 𝑔 ) , 𝑦 ∈ ( Base ‘ 𝑔 ) ↦ ( 𝑥 ( +g𝑔 ) ( ( invg𝑔 ) ‘ 𝑦 ) ) ) )
18 0 17 wceq -g = ( 𝑔 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ 𝑔 ) , 𝑦 ∈ ( Base ‘ 𝑔 ) ↦ ( 𝑥 ( +g𝑔 ) ( ( invg𝑔 ) ‘ 𝑦 ) ) ) )