Metamath Proof Explorer

Theorem rhmpreimaprmidl

Description: The preimage of a prime ideal by a ring homomorphism is a prime ideal. (Contributed by Thierry Arnoux, 29-Jun-2024)

Ref Expression
Hypothesis rhmpreimaprmidl.p 
|- P = ( PrmIdeal ` R )
Assertion rhmpreimaprmidl 
|- ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) -> ( `' F " J ) e. P )

Proof

Step Hyp Ref Expression
1 rhmpreimaprmidl.p 
 |-  P = ( PrmIdeal ` R )
2 rhmrcl1 
 |-  ( F e. ( R RingHom S ) -> R e. Ring )
3 2 ad2antlr 
 |-  ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) -> R e. Ring )
4 rhmrcl2 
 |-  ( F e. ( R RingHom S ) -> S e. Ring )
5 prmidlidl 
 |-  ( ( S e. Ring /\ J e. ( PrmIdeal ` S ) ) -> J e. ( LIdeal ` S ) )
6 4 5 sylan 
 |-  ( ( F e. ( R RingHom S ) /\ J e. ( PrmIdeal ` S ) ) -> J e. ( LIdeal ` S ) )
7 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
8 7 rhmpreimaidl 
 |-  ( ( F e. ( R RingHom S ) /\ J e. ( LIdeal ` S ) ) -> ( `' F " J ) e. ( LIdeal ` R ) )
9 6 8 syldan 
 |-  ( ( F e. ( R RingHom S ) /\ J e. ( PrmIdeal ` S ) ) -> ( `' F " J ) e. ( LIdeal ` R ) )
10 9 adantll 
 |-  ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) -> ( `' F " J ) e. ( LIdeal ` R ) )
11 4 adantr 
 |-  ( ( F e. ( R RingHom S ) /\ J e. ( PrmIdeal ` S ) ) -> S e. Ring )
12 eqid 
 |-  ( Base ` S ) = ( Base ` S )
13 eqid 
 |-  ( .r ` S ) = ( .r ` S )
14 12 13 prmidlnr 
 |-  ( ( S e. Ring /\ J e. ( PrmIdeal ` S ) ) -> J =/= ( Base ` S ) )
15 4 14 sylan 
 |-  ( ( F e. ( R RingHom S ) /\ J e. ( PrmIdeal ` S ) ) -> J =/= ( Base ` S ) )
16 eqid 
 |-  ( 1r ` S ) = ( 1r ` S )
17 12 16 pridln1 
 |-  ( ( S e. Ring /\ J e. ( LIdeal ` S ) /\ J =/= ( Base ` S ) ) -> -. ( 1r ` S ) e. J )
18 11 6 15 17 syl3anc 
 |-  ( ( F e. ( R RingHom S ) /\ J e. ( PrmIdeal ` S ) ) -> -. ( 1r ` S ) e. J )
19 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
20 19 16 rhm1 
 |-  ( F e. ( R RingHom S ) -> ( F ` ( 1r ` R ) ) = ( 1r ` S ) )
21 20 ad2antrr 
 |-  ( ( ( F e. ( R RingHom S ) /\ J e. ( PrmIdeal ` S ) ) /\ ( `' F " J ) = ( Base ` R ) ) -> ( F ` ( 1r ` R ) ) = ( 1r ` S ) )
22 eqid 
 |-  ( Base ` R ) = ( Base ` R )
23 22 12 rhmf 
 |-  ( F e. ( R RingHom S ) -> F : ( Base ` R ) --> ( Base ` S ) )
24 23 ffnd 
 |-  ( F e. ( R RingHom S ) -> F Fn ( Base ` R ) )
25 24 ad2antrr 
 |-  ( ( ( F e. ( R RingHom S ) /\ J e. ( PrmIdeal ` S ) ) /\ ( `' F " J ) = ( Base ` R ) ) -> F Fn ( Base ` R ) )
26 22 19 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. ( Base ` R ) )
27 2 26 syl 
 |-  ( F e. ( R RingHom S ) -> ( 1r ` R ) e. ( Base ` R ) )
28 27 ad2antrr 
 |-  ( ( ( F e. ( R RingHom S ) /\ J e. ( PrmIdeal ` S ) ) /\ ( `' F " J ) = ( Base ` R ) ) -> ( 1r ` R ) e. ( Base ` R ) )
29 simpr 
 |-  ( ( ( F e. ( R RingHom S ) /\ J e. ( PrmIdeal ` S ) ) /\ ( `' F " J ) = ( Base ` R ) ) -> ( `' F " J ) = ( Base ` R ) )
30 28 29 eleqtrrd 
 |-  ( ( ( F e. ( R RingHom S ) /\ J e. ( PrmIdeal ` S ) ) /\ ( `' F " J ) = ( Base ` R ) ) -> ( 1r ` R ) e. ( `' F " J ) )
31 elpreima 
 |-  ( F Fn ( Base ` R ) -> ( ( 1r ` R ) e. ( `' F " J ) <-> ( ( 1r ` R ) e. ( Base ` R ) /\ ( F ` ( 1r ` R ) ) e. J ) ) )
32 31 biimpa 
 |-  ( ( F Fn ( Base ` R ) /\ ( 1r ` R ) e. ( `' F " J ) ) -> ( ( 1r ` R ) e. ( Base ` R ) /\ ( F ` ( 1r ` R ) ) e. J ) )
33 25 30 32 syl2anc 
 |-  ( ( ( F e. ( R RingHom S ) /\ J e. ( PrmIdeal ` S ) ) /\ ( `' F " J ) = ( Base ` R ) ) -> ( ( 1r ` R ) e. ( Base ` R ) /\ ( F ` ( 1r ` R ) ) e. J ) )
34 33 simprd 
 |-  ( ( ( F e. ( R RingHom S ) /\ J e. ( PrmIdeal ` S ) ) /\ ( `' F " J ) = ( Base ` R ) ) -> ( F ` ( 1r ` R ) ) e. J )
35 21 34 eqeltrrd 
 |-  ( ( ( F e. ( R RingHom S ) /\ J e. ( PrmIdeal ` S ) ) /\ ( `' F " J ) = ( Base ` R ) ) -> ( 1r ` S ) e. J )
36 18 35 mtand 
 |-  ( ( F e. ( R RingHom S ) /\ J e. ( PrmIdeal ` S ) ) -> -. ( `' F " J ) = ( Base ` R ) )
37 36 neqned 
 |-  ( ( F e. ( R RingHom S ) /\ J e. ( PrmIdeal ` S ) ) -> ( `' F " J ) =/= ( Base ` R ) )
38 37 adantll 
 |-  ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) -> ( `' F " J ) =/= ( Base ` R ) )
39 simp-5l 
 |-  ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) -> S e. CRing )
40 simp-4r 
 |-  ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) -> J e. ( PrmIdeal ` S ) )
41 simp-5r 
 |-  ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) -> F e. ( R RingHom S ) )
42 41 23 syl 
 |-  ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) -> F : ( Base ` R ) --> ( Base ` S ) )
43 simpllr 
 |-  ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) -> a e. ( Base ` R ) )
44 42 43 ffvelrnd 
 |-  ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) -> ( F ` a ) e. ( Base ` S ) )
45 simplr 
 |-  ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) -> b e. ( Base ` R ) )
46 42 45 ffvelrnd 
 |-  ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) -> ( F ` b ) e. ( Base ` S ) )
47 eqid 
 |-  ( .r ` R ) = ( .r ` R )
48 22 47 13 rhmmul 
 |-  ( ( F e. ( R RingHom S ) /\ a e. ( Base ` R ) /\ b e. ( Base ` R ) ) -> ( F ` ( a ( .r ` R ) b ) ) = ( ( F ` a ) ( .r ` S ) ( F ` b ) ) )
49 41 43 45 48 syl3anc 
 |-  ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) -> ( F ` ( a ( .r ` R ) b ) ) = ( ( F ` a ) ( .r ` S ) ( F ` b ) ) )
50 24 ad5antlr 
 |-  ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) -> F Fn ( Base ` R ) )
51 simpr 
 |-  ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) -> ( a ( .r ` R ) b ) e. ( `' F " J ) )
52 elpreima 
 |-  ( F Fn ( Base ` R ) -> ( ( a ( .r ` R ) b ) e. ( `' F " J ) <-> ( ( a ( .r ` R ) b ) e. ( Base ` R ) /\ ( F ` ( a ( .r ` R ) b ) ) e. J ) ) )
53 52 simplbda 
 |-  ( ( F Fn ( Base ` R ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) -> ( F ` ( a ( .r ` R ) b ) ) e. J )
54 50 51 53 syl2anc 
 |-  ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) -> ( F ` ( a ( .r ` R ) b ) ) e. J )
55 49 54 eqeltrrd 
 |-  ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) -> ( ( F ` a ) ( .r ` S ) ( F ` b ) ) e. J )
56 12 13 prmidlc 
 |-  ( ( ( S e. CRing /\ J e. ( PrmIdeal ` S ) ) /\ ( ( F ` a ) e. ( Base ` S ) /\ ( F ` b ) e. ( Base ` S ) /\ ( ( F ` a ) ( .r ` S ) ( F ` b ) ) e. J ) ) -> ( ( F ` a ) e. J \/ ( F ` b ) e. J ) )
57 39 40 44 46 55 56 syl23anc 
 |-  ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) -> ( ( F ` a ) e. J \/ ( F ` b ) e. J ) )
58 50 adantr 
 |-  ( ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) /\ ( F ` a ) e. J ) -> F Fn ( Base ` R ) )
59 43 adantr 
 |-  ( ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) /\ ( F ` a ) e. J ) -> a e. ( Base ` R ) )
60 simpr 
 |-  ( ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) /\ ( F ` a ) e. J ) -> ( F ` a ) e. J )
61 58 59 60 elpreimad 
 |-  ( ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) /\ ( F ` a ) e. J ) -> a e. ( `' F " J ) )
62 61 ex 
 |-  ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) -> ( ( F ` a ) e. J -> a e. ( `' F " J ) ) )
63 50 adantr 
 |-  ( ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) /\ ( F ` b ) e. J ) -> F Fn ( Base ` R ) )
64 simpllr 
 |-  ( ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) /\ ( F ` b ) e. J ) -> b e. ( Base ` R ) )
65 simpr 
 |-  ( ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) /\ ( F ` b ) e. J ) -> ( F ` b ) e. J )
66 63 64 65 elpreimad 
 |-  ( ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) /\ ( F ` b ) e. J ) -> b e. ( `' F " J ) )
67 66 ex 
 |-  ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) -> ( ( F ` b ) e. J -> b e. ( `' F " J ) ) )
68 62 67 orim12d 
 |-  ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) -> ( ( ( F ` a ) e. J \/ ( F ` b ) e. J ) -> ( a e. ( `' F " J ) \/ b e. ( `' F " J ) ) ) )
69 57 68 mpd 
 |-  ( ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) /\ ( a ( .r ` R ) b ) e. ( `' F " J ) ) -> ( a e. ( `' F " J ) \/ b e. ( `' F " J ) ) )
70 69 ex 
 |-  ( ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ a e. ( Base ` R ) ) /\ b e. ( Base ` R ) ) -> ( ( a ( .r ` R ) b ) e. ( `' F " J ) -> ( a e. ( `' F " J ) \/ b e. ( `' F " J ) ) ) )
71 70 anasss 
 |-  ( ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) /\ ( a e. ( Base ` R ) /\ b e. ( Base ` R ) ) ) -> ( ( a ( .r ` R ) b ) e. ( `' F " J ) -> ( a e. ( `' F " J ) \/ b e. ( `' F " J ) ) ) )
72 71 ralrimivva 
 |-  ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) -> A. a e. ( Base ` R ) A. b e. ( Base ` R ) ( ( a ( .r ` R ) b ) e. ( `' F " J ) -> ( a e. ( `' F " J ) \/ b e. ( `' F " J ) ) ) )
73 22 47 prmidl2 
 |-  ( ( ( R e. Ring /\ ( `' F " J ) e. ( LIdeal ` R ) ) /\ ( ( `' F " J ) =/= ( Base ` R ) /\ A. a e. ( Base ` R ) A. b e. ( Base ` R ) ( ( a ( .r ` R ) b ) e. ( `' F " J ) -> ( a e. ( `' F " J ) \/ b e. ( `' F " J ) ) ) ) ) -> ( `' F " J ) e. ( PrmIdeal ` R ) )
74 3 10 38 72 73 syl22anc 
 |-  ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) -> ( `' F " J ) e. ( PrmIdeal ` R ) )
75 74 1 eleqtrrdi 
 |-  ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ J e. ( PrmIdeal ` S ) ) -> ( `' F " J ) e. P )