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 ‘ 𝑔 ) ‘ 𝑦 ) ) ) )