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 = ( 𝑤 ∈ 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 ‘ 𝑤 ) 𝑥 ) = 𝑦 ) } )