Theorem unitnz

Description: In a nonzero ring, a unit cannot be zero. (Contributed by Thierry Arnoux, 25-Apr-2025)

	Ref	Expression
Hypotheses	unitnz.1	⊢ 𝑈 = ( Unit ‘ 𝑅 )
	unitnz.2	⊢ 0 = ( 0g ‘ 𝑅 )
	unitnz.3	⊢ ( 𝜑 → 𝑅 ∈ NzRing )
	unitnz.4	⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
Assertion	unitnz	⊢ ( 𝜑 → 𝑋 ≠ 0 )

Proof

Step	Hyp	Ref	Expression
1		unitnz.1	⊢ 𝑈 = ( Unit ‘ 𝑅 )
2		unitnz.2	⊢ 0 = ( 0g ‘ 𝑅 )
3		unitnz.3	⊢ ( 𝜑 → 𝑅 ∈ NzRing )
4		unitnz.4	⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
5		nzrring	⊢ ( 𝑅 ∈ NzRing → 𝑅 ∈ Ring )
6	3 5	syl	⊢ ( 𝜑 → 𝑅 ∈ Ring )
7		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
8	7 2	nzrnz	⊢ ( 𝑅 ∈ NzRing → ( 1r ‘ 𝑅 ) ≠ 0 )
9	3 8	syl	⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ≠ 0 )
10	1 2 7	0unit	⊢ ( 𝑅 ∈ Ring → ( 0 ∈ 𝑈 ↔ ( 1r ‘ 𝑅 ) = 0 ) )
11	10	necon3bbid	⊢ ( 𝑅 ∈ Ring → ( ¬ 0 ∈ 𝑈 ↔ ( 1r ‘ 𝑅 ) ≠ 0 ) )
12	11	biimpar	⊢ ( ( 𝑅 ∈ Ring ∧ ( 1r ‘ 𝑅 ) ≠ 0 ) → ¬ 0 ∈ 𝑈 )
13	6 9 12	syl2anc	⊢ ( 𝜑 → ¬ 0 ∈ 𝑈 )
14		nelne2	⊢ ( ( 𝑋 ∈ 𝑈 ∧ ¬ 0 ∈ 𝑈 ) → 𝑋 ≠ 0 )
15	4 13 14	syl2anc	⊢ ( 𝜑 → 𝑋 ≠ 0 )