Metamath Proof Explorer

Definition df-dvr

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

Ref Expression
Assertion df-dvr ⊢ / r = r ∈ V ⟼ x ∈ Base r , y ∈ Unit ⁡ r ⟼ x ⋅ r inv r ⁡ r ⁡ y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdvr class / r
1 vr setvar r
2 cvv class V
3 vx setvar x
4 cbs class Base
5 1 cv setvar r
6 5 4 cfv class Base r
7 vy setvar y
8 cui class Unit
9 5 8 cfv class Unit ⁡ r
10 3 cv setvar x
11 cmulr class ⋅ 𝑟
12 5 11 cfv class ⋅ r
13 cinvr class inv r
14 5 13 cfv class inv r ⁡ r
15 7 cv setvar y
16 15 14 cfv class inv r ⁡ r ⁡ y
17 10 16 12 co class x ⋅ r inv r ⁡ r ⁡ y
18 3 7 6 9 17 cmpo class x ∈ Base r , y ∈ Unit ⁡ r ⟼ x ⋅ r inv r ⁡ r ⁡ y
19 1 2 18 cmpt class r ∈ V ⟼ x ∈ Base r , y ∈ Unit ⁡ r ⟼ x ⋅ r inv r ⁡ r ⁡ y
20 0 19 wceq wff / r = r ∈ V ⟼ x ∈ Base r , y ∈ Unit ⁡ r ⟼ x ⋅ r inv r ⁡ r ⁡ y