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

Metamath Proof Explorer

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