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 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 ) } )