Metamath Proof Explorer


Theorem rprmval

Description: The prime elements of a ring R . (Contributed by Thierry Arnoux, 1-Jul-2024)

Ref Expression
Hypotheses rprmval.b B = Base R
rprmval.u U = Unit R
rprmval.1 0 ˙ = 0 R
rprmval.m · ˙ = R
rprmval.d ˙ = r R
Assertion rprmval R V RPrime R = p B U 0 ˙ | x B y B p ˙ x · ˙ y p ˙ x p ˙ y

Proof

Step Hyp Ref Expression
1 rprmval.b B = Base R
2 rprmval.u U = Unit R
3 rprmval.1 0 ˙ = 0 R
4 rprmval.m · ˙ = R
5 rprmval.d ˙ = r R
6 df-rprm RPrime = r V Base r / b p b Unit r 0 r | x b y b [˙ r r / d]˙ p d x r y p d x p d y
7 fvexd r = R Base r V
8 simpr r = R b = Base r b = Base r
9 fveq2 r = R Base r = Base R
10 9 adantr r = R b = Base r Base r = Base R
11 8 10 eqtrd r = R b = Base r b = Base R
12 11 1 eqtr4di r = R b = Base r b = B
13 fveq2 r = R Unit r = Unit R
14 13 2 eqtr4di r = R Unit r = U
15 fveq2 r = R 0 r = 0 R
16 15 3 eqtr4di r = R 0 r = 0 ˙
17 16 sneqd r = R 0 r = 0 ˙
18 14 17 uneq12d r = R Unit r 0 r = U 0 ˙
19 18 adantr r = R b = Base r Unit r 0 r = U 0 ˙
20 12 19 difeq12d r = R b = Base r b Unit r 0 r = B U 0 ˙
21 fvexd r = R b = Base r r r V
22 eqidd r = R b = Base r d = r r p = p
23 simpr r = R b = Base r d = r r d = r r
24 fveq2 r = R r r = r R
25 24 ad2antrr r = R b = Base r d = r r r r = r R
26 23 25 eqtrd r = R b = Base r d = r r d = r R
27 26 5 eqtr4di r = R b = Base r d = r r d = ˙
28 fveq2 r = R r = R
29 28 4 eqtr4di r = R r = · ˙
30 29 ad2antrr r = R b = Base r d = r r r = · ˙
31 30 oveqd r = R b = Base r d = r r x r y = x · ˙ y
32 22 27 31 breq123d r = R b = Base r d = r r p d x r y p ˙ x · ˙ y
33 27 breqd r = R b = Base r d = r r p d x p ˙ x
34 27 breqd r = R b = Base r d = r r p d y p ˙ y
35 33 34 orbi12d r = R b = Base r d = r r p d x p d y p ˙ x p ˙ y
36 32 35 imbi12d r = R b = Base r d = r r p d x r y p d x p d y p ˙ x · ˙ y p ˙ x p ˙ y
37 21 36 sbcied r = R b = Base r [˙ r r / d]˙ p d x r y p d x p d y p ˙ x · ˙ y p ˙ x p ˙ y
38 12 37 raleqbidv r = R b = Base r y b [˙ r r / d]˙ p d x r y p d x p d y y B p ˙ x · ˙ y p ˙ x p ˙ y
39 12 38 raleqbidv r = R b = Base r x b y b [˙ r r / d]˙ p d x r y p d x p d y x B y B p ˙ x · ˙ y p ˙ x p ˙ y
40 20 39 rabeqbidv r = R b = Base r p b Unit r 0 r | x b y b [˙ r r / d]˙ p d x r y p d x p d y = p B U 0 ˙ | x B y B p ˙ x · ˙ y p ˙ x p ˙ y
41 7 40 csbied r = R Base r / b p b Unit r 0 r | x b y b [˙ r r / d]˙ p d x r y p d x p d y = p B U 0 ˙ | x B y B p ˙ x · ˙ y p ˙ x p ˙ y
42 elex R V R V
43 1 fvexi B V
44 43 difexi B U 0 ˙ V
45 44 rabex p B U 0 ˙ | x B y B p ˙ x · ˙ y p ˙ x p ˙ y V
46 45 a1i R V p B U 0 ˙ | x B y B p ˙ x · ˙ y p ˙ x p ˙ y V
47 6 41 42 46 fvmptd3 R V RPrime R = p B U 0 ˙ | x B y B p ˙ x · ˙ y p ˙ x p ˙ y