Definition df-gdiv

Description: Define a function that maps a group operation to the group's division (or subtraction) operation. (Contributed by NM, 15-Feb-2008) (New usage is discouraged.)

	Ref	Expression
Assertion	df-gdiv	⊢ /𝑔 = ( 𝑔 ∈ GrpOp ↦ ( 𝑥 ∈ ran 𝑔 , 𝑦 ∈ ran 𝑔 ↦ ( 𝑥 𝑔 ( ( inv ‘ 𝑔 ) ‘ 𝑦 ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgs	⊢ /𝑔
1		vg	⊢ 𝑔
2		cgr	⊢ GrpOp
3		vx	⊢ 𝑥
4	1	cv	⊢ 𝑔
5	4	crn	⊢ ran 𝑔
6		vy	⊢ 𝑦
7	3	cv	⊢ 𝑥
8		cgn	⊢ inv
9	4 8	cfv	⊢ ( inv ‘ 𝑔 )
10	6	cv	⊢ 𝑦
11	10 9	cfv	⊢ ( ( inv ‘ 𝑔 ) ‘ 𝑦 )
12	7 11 4	co	⊢ ( 𝑥 𝑔 ( ( inv ‘ 𝑔 ) ‘ 𝑦 ) )
13	3 6 5 5 12	cmpo	⊢ ( 𝑥 ∈ ran 𝑔 , 𝑦 ∈ ran 𝑔 ↦ ( 𝑥 𝑔 ( ( inv ‘ 𝑔 ) ‘ 𝑦 ) ) )
14	1 2 13	cmpt	⊢ ( 𝑔 ∈ GrpOp ↦ ( 𝑥 ∈ ran 𝑔 , 𝑦 ∈ ran 𝑔 ↦ ( 𝑥 𝑔 ( ( inv ‘ 𝑔 ) ‘ 𝑦 ) ) ) )
15	0 14	wceq	⊢ /𝑔 = ( 𝑔 ∈ GrpOp ↦ ( 𝑥 ∈ ran 𝑔 , 𝑦 ∈ ran 𝑔 ↦ ( 𝑥 𝑔 ( ( inv ‘ 𝑔 ) ‘ 𝑦 ) ) ) )