This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )