Definition df-dvr

Description: Define ring division. (Contributed by Mario Carneiro, 2-Jul-2014)

	Ref	Expression
Assertion	df-dvr	⊢ /r = ( 𝑟 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ 𝑟 ) , 𝑦 ∈ ( Unit ‘ 𝑟 ) ↦ ( 𝑥 ( .r ‘ 𝑟 ) ( ( invr ‘ 𝑟 ) ‘ 𝑦 ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdvr	⊢ /r
1		vr	⊢ 𝑟
2		cvv	⊢ V
3		vx	⊢ 𝑥
4		cbs	⊢ Base
5	1	cv	⊢ 𝑟
6	5 4	cfv	⊢ ( Base ‘ 𝑟 )
7		vy	⊢ 𝑦
8		cui	⊢ Unit
9	5 8	cfv	⊢ ( Unit ‘ 𝑟 )
10	3	cv	⊢ 𝑥
11		cmulr	⊢ .r
12	5 11	cfv	⊢ ( .r ‘ 𝑟 )
13		cinvr	⊢ invr
14	5 13	cfv	⊢ ( invr ‘ 𝑟 )
15	7	cv	⊢ 𝑦
16	15 14	cfv	⊢ ( ( invr ‘ 𝑟 ) ‘ 𝑦 )
17	10 16 12	co	⊢ ( 𝑥 ( .r ‘ 𝑟 ) ( ( invr ‘ 𝑟 ) ‘ 𝑦 ) )
18	3 7 6 9 17	cmpo	⊢ ( 𝑥 ∈ ( Base ‘ 𝑟 ) , 𝑦 ∈ ( Unit ‘ 𝑟 ) ↦ ( 𝑥 ( .r ‘ 𝑟 ) ( ( invr ‘ 𝑟 ) ‘ 𝑦 ) ) )
19	1 2 18	cmpt	⊢ ( 𝑟 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ 𝑟 ) , 𝑦 ∈ ( Unit ‘ 𝑟 ) ↦ ( 𝑥 ( .r ‘ 𝑟 ) ( ( invr ‘ 𝑟 ) ‘ 𝑦 ) ) ) )
20	0 19	wceq	⊢ /r = ( 𝑟 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ 𝑟 ) , 𝑦 ∈ ( Unit ‘ 𝑟 ) ↦ ( 𝑥 ( .r ‘ 𝑟 ) ( ( invr ‘ 𝑟 ) ‘ 𝑦 ) ) ) )