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

Metamath Proof Explorer

Definition df-dvdsr

Description: Define the (right) divisibility relation in a ring. Access to the left divisibility relation is available through ( ||r( oppRR ) ) . (Contributed by Mario Carneiro, 1-Dec-2014)

Ref Expression
Assertion df-dvdsr ⊢ ∥ r = w ∈ V ⟼ x y | x ∈ Base w ∧ ∃ z ∈ Base w z ⋅ w x = y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdsr class ∥ r
1 vw setvar w
2 cvv class V
3 vx setvar x
4 vy setvar y
5 3 cv setvar x
6 cbs class Base
7 1 cv setvar w
8 7 6 cfv class Base w
9 5 8 wcel wff x ∈ Base w
10 vz setvar z
11 10 cv setvar z
12 cmulr class ⋅ 𝑟
13 7 12 cfv class ⋅ w
14 11 5 13 co class z ⋅ w x
15 4 cv setvar y
16 14 15 wceq wff z ⋅ w x = y
17 16 10 8 wrex wff ∃ z ∈ Base w z ⋅ w x = y
18 9 17 wa wff x ∈ Base w ∧ ∃ z ∈ Base w z ⋅ w x = y
19 18 3 4 copab class x y | x ∈ Base w ∧ ∃ z ∈ Base w z ⋅ w x = y
20 1 2 19 cmpt class w ∈ V ⟼ x y | x ∈ Base w ∧ ∃ z ∈ Base w z ⋅ w x = y
21 0 20 wceq wff ∥ r = w ∈ V ⟼ x y | x ∈ Base w ∧ ∃ z ∈ Base w z ⋅ w x = y