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 e. _V |-> { <. x , y >. | ( x e. ( Base ` w ) /\ E. z e. ( Base ` w ) ( z ( .r ` w ) x ) = y ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdsr
 |-  ||r
1 vw
 |-  w
2 cvv
 |-  _V
3 vx
 |-  x
4 vy
 |-  y
5 3 cv
 |-  x
6 cbs
 |-  Base
7 1 cv
 |-  w
8 7 6 cfv
 |-  ( Base ` w )
9 5 8 wcel
 |-  x e. ( Base ` w )
10 vz
 |-  z
11 10 cv
 |-  z
12 cmulr
 |-  .r
13 7 12 cfv
 |-  ( .r ` w )
14 11 5 13 co
 |-  ( z ( .r ` w ) x )
15 4 cv
 |-  y
16 14 15 wceq
 |-  ( z ( .r ` w ) x ) = y
17 16 10 8 wrex
 |-  E. z e. ( Base ` w ) ( z ( .r ` w ) x ) = y
18 9 17 wa
 |-  ( x e. ( Base ` w ) /\ E. z e. ( Base ` w ) ( z ( .r ` w ) x ) = y )
19 18 3 4 copab
 |-  { <. x , y >. | ( x e. ( Base ` w ) /\ E. z e. ( Base ` w ) ( z ( .r ` w ) x ) = y ) }
20 1 2 19 cmpt
 |-  ( w e. _V |-> { <. x , y >. | ( x e. ( Base ` w ) /\ E. z e. ( Base ` w ) ( z ( .r ` w ) x ) = y ) } )
21 0 20 wceq
 |-  ||r = ( w e. _V |-> { <. x , y >. | ( x e. ( Base ` w ) /\ E. z e. ( Base ` w ) ( z ( .r ` w ) x ) = y ) } )