Theorem ring1nzdiv

Description: In a unitary ring, the ring unity is not a zero divisor. (Contributed by AV, 7-Mar-2025)

	Ref	Expression
Hypotheses	ringunitnzdiv.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	ringunitnzdiv.z	⊢ 0 = ( 0g ‘ 𝑅 )
	ringunitnzdiv.t	⊢ · = ( .r ‘ 𝑅 )
	ringunitnzdiv.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	ringunitnzdiv.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	ring1nzdiv.x	⊢ 1 = ( 1r ‘ 𝑅 )
Assertion	ring1nzdiv	⊢ ( 𝜑 → ( ( 1 · 𝑌 ) = 0 ↔ 𝑌 = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		ringunitnzdiv.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		ringunitnzdiv.z	⊢ 0 = ( 0g ‘ 𝑅 )
3		ringunitnzdiv.t	⊢ · = ( .r ‘ 𝑅 )
4		ringunitnzdiv.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
5		ringunitnzdiv.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6		ring1nzdiv.x	⊢ 1 = ( 1r ‘ 𝑅 )
7		eqid	⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
8	7 6	1unit	⊢ ( 𝑅 ∈ Ring → 1 ∈ ( Unit ‘ 𝑅 ) )
9	4 8	syl	⊢ ( 𝜑 → 1 ∈ ( Unit ‘ 𝑅 ) )
10	1 2 3 4 5 9	ringunitnzdiv	⊢ ( 𝜑 → ( ( 1 · 𝑌 ) = 0 ↔ 𝑌 = 0 ) )