Metamath Proof Explorer


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 ˙ = 0 R
isrprm.4 ˙ = r R
isrprm.5 · ˙ = R
Assertion isrprm R V P RPrime R P B U 0 ˙ x B y B P ˙ 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 ˙ = 0 R
4 isrprm.4 ˙ = r R
5 isrprm.5 · ˙ = R
6 1 2 3 5 4 rprmval R V RPrime R = p B U 0 ˙ | x B y B p ˙ x · ˙ y p ˙ x p ˙ y
7 6 eleq2d R V P RPrime R P p B U 0 ˙ | x B y B p ˙ x · ˙ y p ˙ x p ˙ y
8 breq1 p = P p ˙ x · ˙ y P ˙ 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 · ˙ y p ˙ x p ˙ y P ˙ x · ˙ y P ˙ x P ˙ y
13 12 2ralbidv p = P x B y B p ˙ x · ˙ y p ˙ x p ˙ y x B y B P ˙ x · ˙ y P ˙ x P ˙ y
14 13 elrab P p B U 0 ˙ | x B y B p ˙ x · ˙ y p ˙ x p ˙ y P B U 0 ˙ x B y B P ˙ x · ˙ y P ˙ x P ˙ y
15 7 14 bitrdi R V P RPrime R P B U 0 ˙ x B y B P ˙ x · ˙ y P ˙ x P ˙ y