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 ) )