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. = ( 0g ` R )
rprmval.m 
|- .x. = ( .r ` R )
rprmval.d 
|- .|| = ( ||r ` R )
Assertion 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 ) ) } )

Proof

Step Hyp Ref Expression
1 rprmval.b 
 |-  B = ( Base ` R )
2 rprmval.u 
 |-  U = ( Unit ` R )
3 rprmval.1 
 |-  .0. = ( 0g ` R )
4 rprmval.m 
 |-  .x. = ( .r ` R )
5 rprmval.d 
 |-  .|| = ( ||r ` R )
6 df-rprm 
 |-  RPrime = ( r e. _V |-> [_ ( Base ` r ) / b ]_ { p e. ( b \ ( ( Unit ` r ) u. { ( 0g ` r ) } ) ) | A. x e. b A. y e. b [. ( ||r ` r ) / d ]. ( p d ( x ( .r ` r ) y ) -> ( p d x \/ p d y ) ) } )
7 fvexd 
 |-  ( r = R -> ( Base ` r ) e. _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 -> ( 0g ` r ) = ( 0g ` R ) )
16 15 3 eqtr4di 
 |-  ( r = R -> ( 0g ` r ) = .0. )
17 16 sneqd 
 |-  ( r = R -> { ( 0g ` r ) } = { .0. } )
18 14 17 uneq12d 
 |-  ( r = R -> ( ( Unit ` r ) u. { ( 0g ` r ) } ) = ( U u. { .0. } ) )
19 18 adantr 
 |-  ( ( r = R /\ b = ( Base ` r ) ) -> ( ( Unit ` r ) u. { ( 0g ` r ) } ) = ( U u. { .0. } ) )
20 12 19 difeq12d 
 |-  ( ( r = R /\ b = ( Base ` r ) ) -> ( b \ ( ( Unit ` r ) u. { ( 0g ` r ) } ) ) = ( B \ ( U u. { .0. } ) ) )
21 fvexd 
 |-  ( ( r = R /\ b = ( Base ` r ) ) -> ( ||r ` r ) e. _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 ) = ( .r ` R ) )
29 28 4 eqtr4di 
 |-  ( r = R -> ( .r ` r ) = .x. )
30 29 ad2antrr 
 |-  ( ( ( r = R /\ b = ( Base ` r ) ) /\ d = ( ||r ` r ) ) -> ( .r ` r ) = .x. )
31 30 oveqd 
 |-  ( ( ( r = R /\ b = ( Base ` r ) ) /\ d = ( ||r ` r ) ) -> ( x ( .r ` r ) y ) = ( x .x. y ) )
32 22 27 31 breq123d 
 |-  ( ( ( r = R /\ b = ( Base ` r ) ) /\ d = ( ||r ` r ) ) -> ( p d ( x ( .r ` r ) y ) <-> p .|| ( x .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 ` r ) y ) -> ( p d x \/ p d y ) ) <-> ( p .|| ( x .x. y ) -> ( p .|| x \/ p .|| y ) ) ) )
37 21 36 sbcied 
 |-  ( ( r = R /\ b = ( Base ` r ) ) -> ( [. ( ||r ` r ) / d ]. ( p d ( x ( .r ` r ) y ) -> ( p d x \/ p d y ) ) <-> ( p .|| ( x .x. y ) -> ( p .|| x \/ p .|| y ) ) ) )
38 12 37 raleqbidv 
 |-  ( ( r = R /\ b = ( Base ` r ) ) -> ( A. y e. b [. ( ||r ` r ) / d ]. ( p d ( x ( .r ` r ) y ) -> ( p d x \/ p d y ) ) <-> A. y e. B ( p .|| ( x .x. y ) -> ( p .|| x \/ p .|| y ) ) ) )
39 12 38 raleqbidv 
 |-  ( ( r = R /\ b = ( Base ` r ) ) -> ( A. x e. b A. y e. b [. ( ||r ` r ) / d ]. ( p d ( x ( .r ` r ) y ) -> ( p d x \/ p d y ) ) <-> A. x e. B A. y e. B ( p .|| ( x .x. y ) -> ( p .|| x \/ p .|| y ) ) ) )
40 20 39 rabeqbidv 
 |-  ( ( r = R /\ b = ( Base ` r ) ) -> { p e. ( b \ ( ( Unit ` r ) u. { ( 0g ` r ) } ) ) | A. x e. b A. y e. b [. ( ||r ` r ) / d ]. ( p d ( x ( .r ` r ) y ) -> ( p d x \/ p d y ) ) } = { p e. ( B \ ( U u. { .0. } ) ) | A. x e. B A. y e. B ( p .|| ( x .x. y ) -> ( p .|| x \/ p .|| y ) ) } )
41 7 40 csbied 
 |-  ( r = R -> [_ ( Base ` r ) / b ]_ { p e. ( b \ ( ( Unit ` r ) u. { ( 0g ` r ) } ) ) | A. x e. b A. y e. b [. ( ||r ` r ) / d ]. ( p d ( x ( .r ` r ) y ) -> ( p d x \/ p d y ) ) } = { p e. ( B \ ( U u. { .0. } ) ) | A. x e. B A. y e. B ( p .|| ( x .x. y ) -> ( p .|| x \/ p .|| y ) ) } )
42 elex 
 |-  ( R e. V -> R e. _V )
43 1 fvexi 
 |-  B e. _V
44 43 difexi 
 |-  ( B \ ( U u. { .0. } ) ) e. _V
45 44 rabex 
 |-  { p e. ( B \ ( U u. { .0. } ) ) | A. x e. B A. y e. B ( p .|| ( x .x. y ) -> ( p .|| x \/ p .|| y ) ) } e. _V
46 45 a1i 
 |-  ( R e. V -> { p e. ( B \ ( U u. { .0. } ) ) | A. x e. B A. y e. B ( p .|| ( x .x. y ) -> ( p .|| x \/ p .|| y ) ) } e. _V )
47 6 41 42 46 fvmptd3 
 |-  ( 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 ) ) } )