Theorem isrprm

Description: Property for P to be a prime element in the ring R . (Contributed by Thierry Arnoux, 1-Jul-2024)

	Ref	Expression
Hypotheses	isrprm.1	|- B = ( Base ` R )
	isrprm.2	|- U = ( Unit ` R )
	isrprm.3	|- .0. = ( 0g ` R )
	isrprm.4	|- .|| = ( ||r ` R )
	isrprm.5	|- .x. = ( .r ` R )
Assertion	isrprm	|- ( R e. V -> ( P e. ( RPrime ` R ) <-> ( P e. ( B \ ( U u. { .0. } ) ) /\ A. x e. B A. y e. B ( P .|| ( x .x. y ) -> ( P .|| x \/ P .|| y ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		isrprm.1	|- B = ( Base ` R )
2		isrprm.2	|- U = ( Unit ` R )
3		isrprm.3	|- .0. = ( 0g ` R )
4		isrprm.4	|- .|| = ( ||r ` R )
5		isrprm.5	|- .x. = ( .r ` R )
6	1 2 3 5 4	rprmval	|- ( R e. V -> ( RPrime ` R ) = { p e. ( B \ ( U u. { .0. } ) ) | A. x e. B A. y e. B ( p .|| ( x .x. y ) -> ( p .|| x \/ p .|| y ) ) } )
7	6	eleq2d	|- ( R e. V -> ( P e. ( RPrime ` R ) <-> P e. { p e. ( B \ ( U u. { .0. } ) ) | A. x e. B A. y e. B ( p .|| ( x .x. y ) -> ( p .|| x \/ p .|| y ) ) } ) )
8		breq1	|- ( p = P -> ( p .|| ( x .x. y ) <-> P .|| ( x .x. y ) ) )
9		breq1	|- ( p = P -> ( p .|| x <-> P .|| x ) )
10		breq1	|- ( p = P -> ( p .|| y <-> P .|| y ) )
11	9 10	orbi12d	|- ( p = P -> ( ( p .|| x \/ p .|| y ) <-> ( P .|| x \/ P .|| y ) ) )
12	8 11	imbi12d	|- ( p = P -> ( ( p .|| ( x .x. y ) -> ( p .|| x \/ p .|| y ) ) <-> ( P .|| ( x .x. y ) -> ( P .|| x \/ P .|| y ) ) ) )
13	12	2ralbidv	|- ( p = P -> ( A. x e. B A. y e. B ( p .|| ( x .x. y ) -> ( p .|| x \/ p .|| y ) ) <-> A. x e. B A. y e. B ( P .|| ( x .x. y ) -> ( P .|| x \/ P .|| y ) ) ) )
14	13	elrab	|- ( P e. { p e. ( B \ ( U u. { .0. } ) ) | A. x e. B A. y e. B ( p .|| ( x .x. y ) -> ( p .|| x \/ p .|| y ) ) } <-> ( P e. ( B \ ( U u. { .0. } ) ) /\ A. x e. B A. y e. B ( P .|| ( x .x. y ) -> ( P .|| x \/ P .|| y ) ) ) )
15	7 14	bitrdi	|- ( R e. V -> ( P e. ( RPrime ` R ) <-> ( P e. ( B \ ( U u. { .0. } ) ) /\ A. x e. B A. y e. B ( P .|| ( x .x. y ) -> ( P .|| x \/ P .|| y ) ) ) ) )