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	|- B = ( Base ` R )
	ringunitnzdiv.z	|- .0. = ( 0g ` R )
	ringunitnzdiv.t	|- .x. = ( .r ` R )
	ringunitnzdiv.r	|- ( ph -> R e. Ring )
	ringunitnzdiv.y	|- ( ph -> Y e. B )
	ring1nzdiv.x	|- .1. = ( 1r ` R )
Assertion	ring1nzdiv	|- ( ph -> ( ( .1. .x. Y ) = .0. <-> Y = .0. ) )

Proof

Step	Hyp	Ref	Expression
1		ringunitnzdiv.b	|- B = ( Base ` R )
2		ringunitnzdiv.z	|- .0. = ( 0g ` R )
3		ringunitnzdiv.t	|- .x. = ( .r ` R )
4		ringunitnzdiv.r	|- ( ph -> R e. Ring )
5		ringunitnzdiv.y	|- ( ph -> Y e. B )
6		ring1nzdiv.x	|- .1. = ( 1r ` R )
7		eqid	|- ( Unit ` R ) = ( Unit ` R )
8	7 6	1unit	|- ( R e. Ring -> .1. e. ( Unit ` R ) )
9	4 8	syl	|- ( ph -> .1. e. ( Unit ` R ) )
10	1 2 3 4 5 9	ringunitnzdiv	|- ( ph -> ( ( .1. .x. Y ) = .0. <-> Y = .0. ) )