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