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

Metamath Proof Explorer

Theorem rrgnz

Description: In a nonzero ring, the zero is a left zero divisor (that is, not a left-regular element). (Contributed by Thierry Arnoux, 6-May-2025)

Ref Expression
Hypotheses rrgnz.t ⊢ 𝐸 = ( RLReg ‘ 𝑅 )
rrgnz.z ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion rrgnz ( 𝑅 ∈ NzRing → ¬ 0 ∈ 𝐸 )

Proof

Step Hyp Ref Expression
1 rrgnz.t ⊢ 𝐸 = ( RLReg ‘ 𝑅 )
2 rrgnz.z ⊢ 0 = ( 0g ‘ 𝑅 )
3 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
4 3 2 nzrnz ⊢ ( 𝑅 ∈ NzRing → ( 1r ‘ 𝑅 ) ≠ 0 )
5 4 neneqd ⊢ ( 𝑅 ∈ NzRing → ¬ ( 1r ‘ 𝑅 ) = 0 )
6 nzrring ⊢ ( 𝑅 ∈ NzRing → 𝑅 ∈ Ring )
7 6 adantr ⊢ ( ( 𝑅 ∈ NzRing ∧ 0 ∈ 𝐸 ) → 𝑅 ∈ Ring )
8 simpr ⊢ ( ( 𝑅 ∈ NzRing ∧ 0 ∈ 𝐸 ) → 0 ∈ 𝐸 )
9 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
10 9 3 ringidcl ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
11 7 10 syl ⊢ ( ( 𝑅 ∈ NzRing ∧ 0 ∈ 𝐸 ) → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
12 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
13 9 12 2 7 11 ringlzd ⊢ ( ( 𝑅 ∈ NzRing ∧ 0 ∈ 𝐸 ) → ( 0 ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = 0 )
14 1 9 12 2 rrgeq0 ⊢ ( ( 𝑅 ∈ Ring ∧ 0 ∈ 𝐸 ∧ ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 0 ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = 0 ↔ ( 1r ‘ 𝑅 ) = 0 ) )
15 14 biimpa ⊢ ( ( ( 𝑅 ∈ Ring ∧ 0 ∈ 𝐸 ∧ ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ) ∧ ( 0 ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = 0 ) → ( 1r ‘ 𝑅 ) = 0 )
16 7 8 11 13 15 syl31anc ⊢ ( ( 𝑅 ∈ NzRing ∧ 0 ∈ 𝐸 ) → ( 1r ‘ 𝑅 ) = 0 )
17 5 16 mtand ⊢ ( 𝑅 ∈ NzRing → ¬ 0 ∈ 𝐸 )