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

Metamath Proof Explorer

Theorem rrgeq0

Description: Left-multiplication by a left regular element does not change zeroness. (Contributed by Stefan O'Rear, 28-Mar-2015)

Ref Expression
Hypotheses rrgval.e ⊢ 𝐸 = ( RLReg ‘ 𝑅 )
rrgval.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
rrgval.t ⊢ · = ( .r ‘ 𝑅 )
rrgval.z ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion rrgeq0 ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 · 𝑌 ) = 0 ↔ 𝑌 = 0 ) )

Proof

Step Hyp Ref Expression
1 rrgval.e ⊢ 𝐸 = ( RLReg ‘ 𝑅 )
2 rrgval.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 rrgval.t ⊢ · = ( .r ‘ 𝑅 )
4 rrgval.z ⊢ 0 = ( 0g ‘ 𝑅 )
5 1 2 3 4 rrgeq0i ⊢ ( ( 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 · 𝑌 ) = 0 → 𝑌 = 0 ) )
6 5 3adant1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 · 𝑌 ) = 0 → 𝑌 = 0 ) )
7 simp1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ 𝐵 ) → 𝑅 ∈ Ring )
8 1 2 3 4 rrgval ⊢ 𝐸 = { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 0 → 𝑦 = 0 ) }
9 8 ssrab3 ⊢ 𝐸 ⊆ 𝐵
10 simp2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ∈ 𝐸 )
11 9 10 sselid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
12 2 3 4 ringrz ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 · 0 ) = 0 )
13 7 11 12 syl2anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 · 0 ) = 0 )
14 oveq2 ⊢ ( 𝑌 = 0 → ( 𝑋 · 𝑌 ) = ( 𝑋 · 0 ) )
15 14 eqeq1d ⊢ ( 𝑌 = 0 → ( ( 𝑋 · 𝑌 ) = 0 ↔ ( 𝑋 · 0 ) = 0 ) )
16 13 15 syl5ibrcom ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑌 = 0 → ( 𝑋 · 𝑌 ) = 0 ) )
17 6 16 impbid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐸 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 · 𝑌 ) = 0 ↔ 𝑌 = 0 ) )