Theorem ringunitnzdiv

Description: In a unitary ring, a unit 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	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	ringunitnzdiv.x	⊢ ( 𝜑 → 𝑋 ∈ ( Unit ‘ 𝑅 ) )
Assertion	ringunitnzdiv	⊢ ( 𝜑 → ( ( 𝑋 · 𝑌 ) = 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		ringunitnzdiv.x	⊢ ( 𝜑 → 𝑋 ∈ ( Unit ‘ 𝑅 ) )
7		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
8		eqid	⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
9	1 8	unitcl	⊢ ( 𝑋 ∈ ( Unit ‘ 𝑅 ) → 𝑋 ∈ 𝐵 )
10	6 9	syl	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
11		eqid	⊢ ( invr ‘ 𝑅 ) = ( invr ‘ 𝑅 )
12	8 11 1	ringinvcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ ( Unit ‘ 𝑅 ) ) → ( ( invr ‘ 𝑅 ) ‘ 𝑋 ) ∈ 𝐵 )
13	4 6 12	syl2anc	⊢ ( 𝜑 → ( ( invr ‘ 𝑅 ) ‘ 𝑋 ) ∈ 𝐵 )
14		oveq1	⊢ ( 𝑒 = ( ( invr ‘ 𝑅 ) ‘ 𝑋 ) → ( 𝑒 · 𝑋 ) = ( ( ( invr ‘ 𝑅 ) ‘ 𝑋 ) · 𝑋 ) )
15	14	eqeq1d	⊢ ( 𝑒 = ( ( invr ‘ 𝑅 ) ‘ 𝑋 ) → ( ( 𝑒 · 𝑋 ) = ( 1r ‘ 𝑅 ) ↔ ( ( ( invr ‘ 𝑅 ) ‘ 𝑋 ) · 𝑋 ) = ( 1r ‘ 𝑅 ) ) )
16	15	adantl	⊢ ( ( 𝜑 ∧ 𝑒 = ( ( invr ‘ 𝑅 ) ‘ 𝑋 ) ) → ( ( 𝑒 · 𝑋 ) = ( 1r ‘ 𝑅 ) ↔ ( ( ( invr ‘ 𝑅 ) ‘ 𝑋 ) · 𝑋 ) = ( 1r ‘ 𝑅 ) ) )
17	8 11 3 7	unitlinv	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ ( Unit ‘ 𝑅 ) ) → ( ( ( invr ‘ 𝑅 ) ‘ 𝑋 ) · 𝑋 ) = ( 1r ‘ 𝑅 ) )
18	4 6 17	syl2anc	⊢ ( 𝜑 → ( ( ( invr ‘ 𝑅 ) ‘ 𝑋 ) · 𝑋 ) = ( 1r ‘ 𝑅 ) )
19	13 16 18	rspcedvd	⊢ ( 𝜑 → ∃ 𝑒 ∈ 𝐵 ( 𝑒 · 𝑋 ) = ( 1r ‘ 𝑅 ) )
20	1 3 7 2 4 10 19 5	ringinvnzdiv	⊢ ( 𝜑 → ( ( 𝑋 · 𝑌 ) = 0 ↔ 𝑌 = 0 ) )