Theorem rprmnunit

Description: A ring prime is not a unit. (Contributed by Thierry Arnoux, 18-May-2025)

	Ref	Expression
Hypotheses	rprmdvds.2	|- P = ( RPrime ` R )
	rprmdvds.3	|- U = ( Unit ` R )
	rprmdvds.5	|- ( ph -> R e. V )
	rprmdvds.6	|- ( ph -> Q e. P )
Assertion	rprmnunit	|- ( ph -> -. Q e. U )

Proof

Step	Hyp	Ref	Expression
1		rprmdvds.2	|- P = ( RPrime ` R )
2		rprmdvds.3	|- U = ( Unit ` R )
3		rprmdvds.5	|- ( ph -> R e. V )
4		rprmdvds.6	|- ( ph -> Q e. P )
5		eqidd	|- ( ph -> ( U u. { ( 0g ` R ) } ) = ( U u. { ( 0g ` R ) } ) )
6	4 1	eleqtrdi	|- ( ph -> Q e. ( RPrime ` R ) )
7		eqid	|- ( Base ` R ) = ( Base ` R )
8		eqid	|- ( 0g ` R ) = ( 0g ` R )
9		eqid	|- ( ||r ` R ) = ( ||r ` R )
10		eqid	|- ( .r ` R ) = ( .r ` R )
11	7 2 8 9 10	isrprm	|- ( R e. V -> ( Q e. ( RPrime ` R ) <-> ( Q e. ( ( Base ` R ) \ ( U u. { ( 0g ` R ) } ) ) /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( Q ( ||r ` R ) ( x ( .r ` R ) y ) -> ( Q ( ||r ` R ) x \/ Q ( ||r ` R ) y ) ) ) ) )
12	11	simprbda	|- ( ( R e. V /\ Q e. ( RPrime ` R ) ) -> Q e. ( ( Base ` R ) \ ( U u. { ( 0g ` R ) } ) ) )
13	3 6 12	syl2anc	|- ( ph -> Q e. ( ( Base ` R ) \ ( U u. { ( 0g ` R ) } ) ) )
14	13	eldifbd	|- ( ph -> -. Q e. ( U u. { ( 0g ` R ) } ) )
15		nelun	|- ( ( U u. { ( 0g ` R ) } ) = ( U u. { ( 0g ` R ) } ) -> ( -. Q e. ( U u. { ( 0g ` R ) } ) <-> ( -. Q e. U /\ -. Q e. { ( 0g ` R ) } ) ) )
16	15	simprbda	|- ( ( ( U u. { ( 0g ` R ) } ) = ( U u. { ( 0g ` R ) } ) /\ -. Q e. ( U u. { ( 0g ` R ) } ) ) -> -. Q e. U )
17	5 14 16	syl2anc	|- ( ph -> -. Q e. U )