Metamath Proof Explorer

Theorem rprmirred

Description: In an integral domain, ring primes are irreducible. (Contributed by Thierry Arnoux, 18-May-2025)

Ref Expression
Hypotheses rprmirred.p 
|- P = ( RPrime ` R )
rprmirred.i 
|- I = ( Irred ` R )
rprmirred.q 
|- ( ph -> Q e. P )
rprmirred.r 
|- ( ph -> R e. IDomn )
Assertion rprmirred 
|- ( ph -> Q e. I )

Proof

Step Hyp Ref Expression
1 rprmirred.p 
 |-  P = ( RPrime ` R )
2 rprmirred.i 
 |-  I = ( Irred ` R )
3 rprmirred.q 
 |-  ( ph -> Q e. P )
4 rprmirred.r 
 |-  ( ph -> R e. IDomn )
5 eqid 
 |-  ( Base ` R ) = ( Base ` R )
6 5 1 4 3 rprmcl 
 |-  ( ph -> Q e. ( Base ` R ) )
7 eqid 
 |-  ( Unit ` R ) = ( Unit ` R )
8 1 7 4 3 rprmnunit 
 |-  ( ph -> -. Q e. ( Unit ` R ) )
9 6 8 eldifd 
 |-  ( ph -> Q e. ( ( Base ` R ) \ ( Unit ` R ) ) )
10 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
11 eqid 
 |-  ( .r ` R ) = ( .r ` R )
12 eqid 
 |-  ( ||r ` R ) = ( ||r ` R )
13 4 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ y e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ ( x ( .r ` R ) y ) = Q ) -> R e. IDomn )
14 13 adantr 
 |-  ( ( ( ( ( ph /\ x e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ y e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ ( x ( .r ` R ) y ) = Q ) /\ Q ( ||r ` R ) x ) -> R e. IDomn )
15 1 10 4 3 rprmnz 
 |-  ( ph -> Q =/= ( 0g ` R ) )
16 15 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ y e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ ( x ( .r ` R ) y ) = Q ) /\ Q ( ||r ` R ) x ) -> Q =/= ( 0g ` R ) )
17 simpllr 
 |-  ( ( ( ( ph /\ x e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ y e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ ( x ( .r ` R ) y ) = Q ) -> x e. ( ( Base ` R ) \ ( Unit ` R ) ) )
18 17 adantr 
 |-  ( ( ( ( ( ph /\ x e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ y e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ ( x ( .r ` R ) y ) = Q ) /\ Q ( ||r ` R ) x ) -> x e. ( ( Base ` R ) \ ( Unit ` R ) ) )
19 simplr 
 |-  ( ( ( ( ph /\ x e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ y e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ ( x ( .r ` R ) y ) = Q ) -> y e. ( ( Base ` R ) \ ( Unit ` R ) ) )
20 19 eldifad 
 |-  ( ( ( ( ph /\ x e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ y e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ ( x ( .r ` R ) y ) = Q ) -> y e. ( Base ` R ) )
21 20 adantr 
 |-  ( ( ( ( ( ph /\ x e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ y e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ ( x ( .r ` R ) y ) = Q ) /\ Q ( ||r ` R ) x ) -> y e. ( Base ` R ) )
22 simplr 
 |-  ( ( ( ( ( ph /\ x e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ y e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ ( x ( .r ` R ) y ) = Q ) /\ Q ( ||r ` R ) x ) -> ( x ( .r ` R ) y ) = Q )
23 22 eqcomd 
 |-  ( ( ( ( ( ph /\ x e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ y e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ ( x ( .r ` R ) y ) = Q ) /\ Q ( ||r ` R ) x ) -> Q = ( x ( .r ` R ) y ) )
24 simpr 
 |-  ( ( ( ( ( ph /\ x e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ y e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ ( x ( .r ` R ) y ) = Q ) /\ Q ( ||r ` R ) x ) -> Q ( ||r ` R ) x )
25 5 7 10 11 12 14 16 18 21 23 24 rprmirredlem 
 |-  ( ( ( ( ( ph /\ x e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ y e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ ( x ( .r ` R ) y ) = Q ) /\ Q ( ||r ` R ) x ) -> y e. ( Unit ` R ) )
26 19 adantr 
 |-  ( ( ( ( ( ph /\ x e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ y e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ ( x ( .r ` R ) y ) = Q ) /\ Q ( ||r ` R ) x ) -> y e. ( ( Base ` R ) \ ( Unit ` R ) ) )
27 26 eldifbd 
 |-  ( ( ( ( ( ph /\ x e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ y e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ ( x ( .r ` R ) y ) = Q ) /\ Q ( ||r ` R ) x ) -> -. y e. ( Unit ` R ) )
28 25 27 pm2.21fal 
 |-  ( ( ( ( ( ph /\ x e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ y e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ ( x ( .r ` R ) y ) = Q ) /\ Q ( ||r ` R ) x ) -> F. )
29 13 adantr 
 |-  ( ( ( ( ( ph /\ x e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ y e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ ( x ( .r ` R ) y ) = Q ) /\ Q ( ||r ` R ) y ) -> R e. IDomn )
30 15 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ y e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ ( x ( .r ` R ) y ) = Q ) /\ Q ( ||r ` R ) y ) -> Q =/= ( 0g ` R ) )
31 19 adantr 
 |-  ( ( ( ( ( ph /\ x e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ y e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ ( x ( .r ` R ) y ) = Q ) /\ Q ( ||r ` R ) y ) -> y e. ( ( Base ` R ) \ ( Unit ` R ) ) )
32 17 eldifad 
 |-  ( ( ( ( ph /\ x e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ y e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ ( x ( .r ` R ) y ) = Q ) -> x e. ( Base ` R ) )
33 32 adantr 
 |-  ( ( ( ( ( ph /\ x e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ y e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ ( x ( .r ` R ) y ) = Q ) /\ Q ( ||r ` R ) y ) -> x e. ( Base ` R ) )
34 simplr 
 |-  ( ( ( ( ( ph /\ x e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ y e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ ( x ( .r ` R ) y ) = Q ) /\ Q ( ||r ` R ) y ) -> ( x ( .r ` R ) y ) = Q )
35 29 idomcringd 
 |-  ( ( ( ( ( ph /\ x e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ y e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ ( x ( .r ` R ) y ) = Q ) /\ Q ( ||r ` R ) y ) -> R e. CRing )
36 20 adantr 
 |-  ( ( ( ( ( ph /\ x e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ y e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ ( x ( .r ` R ) y ) = Q ) /\ Q ( ||r ` R ) y ) -> y e. ( Base ` R ) )
37 5 11 35 33 36 crngcomd 
 |-  ( ( ( ( ( ph /\ x e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ y e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ ( x ( .r ` R ) y ) = Q ) /\ Q ( ||r ` R ) y ) -> ( x ( .r ` R ) y ) = ( y ( .r ` R ) x ) )
38 34 37 eqtr3d 
 |-  ( ( ( ( ( ph /\ x e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ y e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ ( x ( .r ` R ) y ) = Q ) /\ Q ( ||r ` R ) y ) -> Q = ( y ( .r ` R ) x ) )
39 simpr 
 |-  ( ( ( ( ( ph /\ x e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ y e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ ( x ( .r ` R ) y ) = Q ) /\ Q ( ||r ` R ) y ) -> Q ( ||r ` R ) y )
40 5 7 10 11 12 29 30 31 33 38 39 rprmirredlem 
 |-  ( ( ( ( ( ph /\ x e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ y e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ ( x ( .r ` R ) y ) = Q ) /\ Q ( ||r ` R ) y ) -> x e. ( Unit ` R ) )
41 17 adantr 
 |-  ( ( ( ( ( ph /\ x e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ y e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ ( x ( .r ` R ) y ) = Q ) /\ Q ( ||r ` R ) y ) -> x e. ( ( Base ` R ) \ ( Unit ` R ) ) )
42 41 eldifbd 
 |-  ( ( ( ( ( ph /\ x e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ y e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ ( x ( .r ` R ) y ) = Q ) /\ Q ( ||r ` R ) y ) -> -. x e. ( Unit ` R ) )
43 40 42 pm2.21fal 
 |-  ( ( ( ( ( ph /\ x e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ y e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ ( x ( .r ` R ) y ) = Q ) /\ Q ( ||r ` R ) y ) -> F. )
44 3 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ y e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ ( x ( .r ` R ) y ) = Q ) -> Q e. P )
45 4 idomringd 
 |-  ( ph -> R e. Ring )
46 5 12 dvdsrid 
 |-  ( ( R e. Ring /\ Q e. ( Base ` R ) ) -> Q ( ||r ` R ) Q )
47 45 6 46 syl2anc 
 |-  ( ph -> Q ( ||r ` R ) Q )
48 47 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ y e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ ( x ( .r ` R ) y ) = Q ) -> Q ( ||r ` R ) Q )
49 simpr 
 |-  ( ( ( ( ph /\ x e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ y e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ ( x ( .r ` R ) y ) = Q ) -> ( x ( .r ` R ) y ) = Q )
50 48 49 breqtrrd 
 |-  ( ( ( ( ph /\ x e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ y e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ ( x ( .r ` R ) y ) = Q ) -> Q ( ||r ` R ) ( x ( .r ` R ) y ) )
51 5 1 12 11 13 44 32 20 50 rprmdvds 
 |-  ( ( ( ( ph /\ x e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ y e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ ( x ( .r ` R ) y ) = Q ) -> ( Q ( ||r ` R ) x \/ Q ( ||r ` R ) y ) )
52 28 43 51 mpjaodan 
 |-  ( ( ( ( ph /\ x e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ y e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ ( x ( .r ` R ) y ) = Q ) -> F. )
53 52 inegd 
 |-  ( ( ( ph /\ x e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ y e. ( ( Base ` R ) \ ( Unit ` R ) ) ) -> -. ( x ( .r ` R ) y ) = Q )
54 53 neqned 
 |-  ( ( ( ph /\ x e. ( ( Base ` R ) \ ( Unit ` R ) ) ) /\ y e. ( ( Base ` R ) \ ( Unit ` R ) ) ) -> ( x ( .r ` R ) y ) =/= Q )
55 54 anasss 
 |-  ( ( ph /\ ( x e. ( ( Base ` R ) \ ( Unit ` R ) ) /\ y e. ( ( Base ` R ) \ ( Unit ` R ) ) ) ) -> ( x ( .r ` R ) y ) =/= Q )
56 55 ralrimivva 
 |-  ( ph -> A. x e. ( ( Base ` R ) \ ( Unit ` R ) ) A. y e. ( ( Base ` R ) \ ( Unit ` R ) ) ( x ( .r ` R ) y ) =/= Q )
57 eqid 
 |-  ( ( Base ` R ) \ ( Unit ` R ) ) = ( ( Base ` R ) \ ( Unit ` R ) )
58 5 7 2 57 11 isirred 
 |-  ( Q e. I <-> ( Q e. ( ( Base ` R ) \ ( Unit ` R ) ) /\ A. x e. ( ( Base ` R ) \ ( Unit ` R ) ) A. y e. ( ( Base ` R ) \ ( Unit ` R ) ) ( x ( .r ` R ) y ) =/= Q ) )
59 9 56 58 sylanbrc 
 |-  ( ph -> Q e. I )