Theorem dvdsr01

Description: In a ring, zero is divisible by all elements. ("Zero divisor" as a term has a somewhat different meaning, see df-rlreg .) (Contributed by Stefan O'Rear, 29-Mar-2015)

	Ref	Expression
Hypotheses	dvdsr0.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	dvdsr0.d	⊢ ∥ = ( ∥r ‘ 𝑅 )
	dvdsr0.z	⊢ 0 = ( 0g ‘ 𝑅 )
Assertion	dvdsr01	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∥ 0 )

Proof

Step	Hyp	Ref	Expression
1		dvdsr0.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		dvdsr0.d	⊢ ∥ = ( ∥r ‘ 𝑅 )
3		dvdsr0.z	⊢ 0 = ( 0g ‘ 𝑅 )
4	1 3	ring0cl	⊢ ( 𝑅 ∈ Ring → 0 ∈ 𝐵 )
5		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
6	1 5 3	ringlz	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 0 ( .r ‘ 𝑅 ) 𝑋 ) = 0 )
7		oveq1	⊢ ( 𝑥 = 0 → ( 𝑥 ( .r ‘ 𝑅 ) 𝑋 ) = ( 0 ( .r ‘ 𝑅 ) 𝑋 ) )
8	7	eqeq1d	⊢ ( 𝑥 = 0 → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑋 ) = 0 ↔ ( 0 ( .r ‘ 𝑅 ) 𝑋 ) = 0 ) )
9	8	rspcev	⊢ ( ( 0 ∈ 𝐵 ∧ ( 0 ( .r ‘ 𝑅 ) 𝑋 ) = 0 ) → ∃ 𝑥 ∈ 𝐵 ( 𝑥 ( .r ‘ 𝑅 ) 𝑋 ) = 0 )
10	4 6 9	syl2an2r	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ∃ 𝑥 ∈ 𝐵 ( 𝑥 ( .r ‘ 𝑅 ) 𝑋 ) = 0 )
11	1 2 5	dvdsr2	⊢ ( 𝑋 ∈ 𝐵 → ( 𝑋 ∥ 0 ↔ ∃ 𝑥 ∈ 𝐵 ( 𝑥 ( .r ‘ 𝑅 ) 𝑋 ) = 0 ) )
12	11	adantl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ∥ 0 ↔ ∃ 𝑥 ∈ 𝐵 ( 𝑥 ( .r ‘ 𝑅 ) 𝑋 ) = 0 ) )
13	10 12	mpbird	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∥ 0 )