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 = ( 𝑤 ∈ V ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( Base ‘ 𝑤 ) ∧ ∃ 𝑧 ∈ ( Base ‘ 𝑤 ) ( 𝑧 ( .r𝑤 ) 𝑥 ) = 𝑦 ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdsr r
1 vw 𝑤
2 cvv V
3 vx 𝑥
4 vy 𝑦
5 3 cv 𝑥
6 cbs Base
7 1 cv 𝑤
8 7 6 cfv ( Base ‘ 𝑤 )
9 5 8 wcel 𝑥 ∈ ( Base ‘ 𝑤 )
10 vz 𝑧
11 10 cv 𝑧
12 cmulr .r
13 7 12 cfv ( .r𝑤 )
14 11 5 13 co ( 𝑧 ( .r𝑤 ) 𝑥 )
15 4 cv 𝑦
16 14 15 wceq ( 𝑧 ( .r𝑤 ) 𝑥 ) = 𝑦
17 16 10 8 wrex 𝑧 ∈ ( Base ‘ 𝑤 ) ( 𝑧 ( .r𝑤 ) 𝑥 ) = 𝑦
18 9 17 wa ( 𝑥 ∈ ( Base ‘ 𝑤 ) ∧ ∃ 𝑧 ∈ ( Base ‘ 𝑤 ) ( 𝑧 ( .r𝑤 ) 𝑥 ) = 𝑦 )
19 18 3 4 copab { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( Base ‘ 𝑤 ) ∧ ∃ 𝑧 ∈ ( Base ‘ 𝑤 ) ( 𝑧 ( .r𝑤 ) 𝑥 ) = 𝑦 ) }
20 1 2 19 cmpt ( 𝑤 ∈ V ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( Base ‘ 𝑤 ) ∧ ∃ 𝑧 ∈ ( Base ‘ 𝑤 ) ( 𝑧 ( .r𝑤 ) 𝑥 ) = 𝑦 ) } )
21 0 20 wceq r = ( 𝑤 ∈ V ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( Base ‘ 𝑤 ) ∧ ∃ 𝑧 ∈ ( Base ‘ 𝑤 ) ( 𝑧 ( .r𝑤 ) 𝑥 ) = 𝑦 ) } )