Metamath Proof Explorer

Theorem rhmpreimaidl

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

Ref Expression
Hypothesis rhmpreimaidl.i 
|- I = ( LIdeal ` R )
Assertion rhmpreimaidl 
|- ( ( F e. ( R RingHom S ) /\ J e. ( LIdeal ` S ) ) -> ( `' F " J ) e. I )

Proof

Step Hyp Ref Expression
1 rhmpreimaidl.i 
 |-  I = ( LIdeal ` R )
2 cnvimass 
 |-  ( `' F " J ) C_ dom F
3 eqid 
 |-  ( Base ` R ) = ( Base ` R )
4 eqid 
 |-  ( Base ` S ) = ( Base ` S )
5 3 4 rhmf 
 |-  ( F e. ( R RingHom S ) -> F : ( Base ` R ) --> ( Base ` S ) )
6 2 5 fssdm 
 |-  ( F e. ( R RingHom S ) -> ( `' F " J ) C_ ( Base ` R ) )
7 6 adantr 
 |-  ( ( F e. ( R RingHom S ) /\ J e. ( LIdeal ` S ) ) -> ( `' F " J ) C_ ( Base ` R ) )
8 5 adantr 
 |-  ( ( F e. ( R RingHom S ) /\ J e. ( LIdeal ` S ) ) -> F : ( Base ` R ) --> ( Base ` S ) )
9 8 ffund 
 |-  ( ( F e. ( R RingHom S ) /\ J e. ( LIdeal ` S ) ) -> Fun F )
10 rhmrcl1 
 |-  ( F e. ( R RingHom S ) -> R e. Ring )
11 10 adantr 
 |-  ( ( F e. ( R RingHom S ) /\ J e. ( LIdeal ` S ) ) -> R e. Ring )
12 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
13 3 12 ring0cl 
 |-  ( R e. Ring -> ( 0g ` R ) e. ( Base ` R ) )
14 11 13 syl 
 |-  ( ( F e. ( R RingHom S ) /\ J e. ( LIdeal ` S ) ) -> ( 0g ` R ) e. ( Base ` R ) )
15 8 fdmd 
 |-  ( ( F e. ( R RingHom S ) /\ J e. ( LIdeal ` S ) ) -> dom F = ( Base ` R ) )
16 14 15 eleqtrrd 
 |-  ( ( F e. ( R RingHom S ) /\ J e. ( LIdeal ` S ) ) -> ( 0g ` R ) e. dom F )
17 rhmghm 
 |-  ( F e. ( R RingHom S ) -> F e. ( R GrpHom S ) )
18 ghmmhm 
 |-  ( F e. ( R GrpHom S ) -> F e. ( R MndHom S ) )
19 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
20 12 19 mhm0 
 |-  ( F e. ( R MndHom S ) -> ( F ` ( 0g ` R ) ) = ( 0g ` S ) )
21 17 18 20 3syl 
 |-  ( F e. ( R RingHom S ) -> ( F ` ( 0g ` R ) ) = ( 0g ` S ) )
22 21 adantr 
 |-  ( ( F e. ( R RingHom S ) /\ J e. ( LIdeal ` S ) ) -> ( F ` ( 0g ` R ) ) = ( 0g ` S ) )
23 rhmrcl2 
 |-  ( F e. ( R RingHom S ) -> S e. Ring )
24 eqid 
 |-  ( LIdeal ` S ) = ( LIdeal ` S )
25 24 19 lidl0cl 
 |-  ( ( S e. Ring /\ J e. ( LIdeal ` S ) ) -> ( 0g ` S ) e. J )
26 23 25 sylan 
 |-  ( ( F e. ( R RingHom S ) /\ J e. ( LIdeal ` S ) ) -> ( 0g ` S ) e. J )
27 22 26 eqeltrd 
 |-  ( ( F e. ( R RingHom S ) /\ J e. ( LIdeal ` S ) ) -> ( F ` ( 0g ` R ) ) e. J )
28 fvimacnv 
 |-  ( ( Fun F /\ ( 0g ` R ) e. dom F ) -> ( ( F ` ( 0g ` R ) ) e. J <-> ( 0g ` R ) e. ( `' F " J ) ) )
29 28 biimpa 
 |-  ( ( ( Fun F /\ ( 0g ` R ) e. dom F ) /\ ( F ` ( 0g ` R ) ) e. J ) -> ( 0g ` R ) e. ( `' F " J ) )
30 9 16 27 29 syl21anc 
 |-  ( ( F e. ( R RingHom S ) /\ J e. ( LIdeal ` S ) ) -> ( 0g ` R ) e. ( `' F " J ) )
31 30 ne0d 
 |-  ( ( F e. ( R RingHom S ) /\ J e. ( LIdeal ` S ) ) -> ( `' F " J ) =/= (/) )
32 8 ffnd 
 |-  ( ( F e. ( R RingHom S ) /\ J e. ( LIdeal ` S ) ) -> F Fn ( Base ` R ) )
33 32 ad3antrrr 
 |-  ( ( ( ( ( F e. ( R RingHom S ) /\ J e. ( LIdeal ` S ) ) /\ x e. ( Base ` R ) ) /\ a e. ( `' F " J ) ) /\ b e. ( `' F " J ) ) -> F Fn ( Base ` R ) )
34 11 ad3antrrr 
 |-  ( ( ( ( ( F e. ( R RingHom S ) /\ J e. ( LIdeal ` S ) ) /\ x e. ( Base ` R ) ) /\ a e. ( `' F " J ) ) /\ b e. ( `' F " J ) ) -> R e. Ring )
35 simpllr 
 |-  ( ( ( ( ( F e. ( R RingHom S ) /\ J e. ( LIdeal ` S ) ) /\ x e. ( Base ` R ) ) /\ a e. ( `' F " J ) ) /\ b e. ( `' F " J ) ) -> x e. ( Base ` R ) )
36 6 ad2antrr 
 |-  ( ( ( F e. ( R RingHom S ) /\ J e. ( LIdeal ` S ) ) /\ x e. ( Base ` R ) ) -> ( `' F " J ) C_ ( Base ` R ) )
37 36 sselda 
 |-  ( ( ( ( F e. ( R RingHom S ) /\ J e. ( LIdeal ` S ) ) /\ x e. ( Base ` R ) ) /\ a e. ( `' F " J ) ) -> a e. ( Base ` R ) )
38 37 adantr 
 |-  ( ( ( ( ( F e. ( R RingHom S ) /\ J e. ( LIdeal ` S ) ) /\ x e. ( Base ` R ) ) /\ a e. ( `' F " J ) ) /\ b e. ( `' F " J ) ) -> a e. ( Base ` R ) )
39 eqid 
 |-  ( .r ` R ) = ( .r ` R )
40 3 39 ringcl 
 |-  ( ( R e. Ring /\ x e. ( Base ` R ) /\ a e. ( Base ` R ) ) -> ( x ( .r ` R ) a ) e. ( Base ` R ) )
41 34 35 38 40 syl3anc 
 |-  ( ( ( ( ( F e. ( R RingHom S ) /\ J e. ( LIdeal ` S ) ) /\ x e. ( Base ` R ) ) /\ a e. ( `' F " J ) ) /\ b e. ( `' F " J ) ) -> ( x ( .r ` R ) a ) e. ( Base ` R ) )
42 36 adantr 
 |-  ( ( ( ( F e. ( R RingHom S ) /\ J e. ( LIdeal ` S ) ) /\ x e. ( Base ` R ) ) /\ a e. ( `' F " J ) ) -> ( `' F " J ) C_ ( Base ` R ) )
43 42 sselda 
 |-  ( ( ( ( ( F e. ( R RingHom S ) /\ J e. ( LIdeal ` S ) ) /\ x e. ( Base ` R ) ) /\ a e. ( `' F " J ) ) /\ b e. ( `' F " J ) ) -> b e. ( Base ` R ) )
44 eqid 
 |-  ( +g ` R ) = ( +g ` R )
45 3 44 ringacl 
 |-  ( ( R e. Ring /\ ( x ( .r ` R ) a ) e. ( Base ` R ) /\ b e. ( Base ` R ) ) -> ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. ( Base ` R ) )
46 34 41 43 45 syl3anc 
 |-  ( ( ( ( ( F e. ( R RingHom S ) /\ J e. ( LIdeal ` S ) ) /\ x e. ( Base ` R ) ) /\ a e. ( `' F " J ) ) /\ b e. ( `' F " J ) ) -> ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. ( Base ` R ) )
47 17 ad4antr 
 |-  ( ( ( ( ( F e. ( R RingHom S ) /\ J e. ( LIdeal ` S ) ) /\ x e. ( Base ` R ) ) /\ a e. ( `' F " J ) ) /\ b e. ( `' F " J ) ) -> F e. ( R GrpHom S ) )
48 eqid 
 |-  ( +g ` S ) = ( +g ` S )
49 3 44 48 ghmlin 
 |-  ( ( F e. ( R GrpHom S ) /\ ( x ( .r ` R ) a ) e. ( Base ` R ) /\ b e. ( Base ` R ) ) -> ( F ` ( ( x ( .r ` R ) a ) ( +g ` R ) b ) ) = ( ( F ` ( x ( .r ` R ) a ) ) ( +g ` S ) ( F ` b ) ) )
50 47 41 43 49 syl3anc 
 |-  ( ( ( ( ( F e. ( R RingHom S ) /\ J e. ( LIdeal ` S ) ) /\ x e. ( Base ` R ) ) /\ a e. ( `' F " J ) ) /\ b e. ( `' F " J ) ) -> ( F ` ( ( x ( .r ` R ) a ) ( +g ` R ) b ) ) = ( ( F ` ( x ( .r ` R ) a ) ) ( +g ` S ) ( F ` b ) ) )
51 simp-4l 
 |-  ( ( ( ( ( F e. ( R RingHom S ) /\ J e. ( LIdeal ` S ) ) /\ x e. ( Base ` R ) ) /\ a e. ( `' F " J ) ) /\ b e. ( `' F " J ) ) -> F e. ( R RingHom S ) )
52 51 23 syl 
 |-  ( ( ( ( ( F e. ( R RingHom S ) /\ J e. ( LIdeal ` S ) ) /\ x e. ( Base ` R ) ) /\ a e. ( `' F " J ) ) /\ b e. ( `' F " J ) ) -> S e. Ring )
53 simpr 
 |-  ( ( F e. ( R RingHom S ) /\ J e. ( LIdeal ` S ) ) -> J e. ( LIdeal ` S ) )
54 53 ad3antrrr 
 |-  ( ( ( ( ( F e. ( R RingHom S ) /\ J e. ( LIdeal ` S ) ) /\ x e. ( Base ` R ) ) /\ a e. ( `' F " J ) ) /\ b e. ( `' F " J ) ) -> J e. ( LIdeal ` S ) )
55 eqid 
 |-  ( .r ` S ) = ( .r ` S )
56 3 39 55 rhmmul 
 |-  ( ( F e. ( R RingHom S ) /\ x e. ( Base ` R ) /\ a e. ( Base ` R ) ) -> ( F ` ( x ( .r ` R ) a ) ) = ( ( F ` x ) ( .r ` S ) ( F ` a ) ) )
57 51 35 38 56 syl3anc 
 |-  ( ( ( ( ( F e. ( R RingHom S ) /\ J e. ( LIdeal ` S ) ) /\ x e. ( Base ` R ) ) /\ a e. ( `' F " J ) ) /\ b e. ( `' F " J ) ) -> ( F ` ( x ( .r ` R ) a ) ) = ( ( F ` x ) ( .r ` S ) ( F ` a ) ) )
58 8 ffvelrnda 
 |-  ( ( ( F e. ( R RingHom S ) /\ J e. ( LIdeal ` S ) ) /\ x e. ( Base ` R ) ) -> ( F ` x ) e. ( Base ` S ) )
59 58 ad2antrr 
 |-  ( ( ( ( ( F e. ( R RingHom S ) /\ J e. ( LIdeal ` S ) ) /\ x e. ( Base ` R ) ) /\ a e. ( `' F " J ) ) /\ b e. ( `' F " J ) ) -> ( F ` x ) e. ( Base ` S ) )
60 simplr 
 |-  ( ( ( ( ( F e. ( R RingHom S ) /\ J e. ( LIdeal ` S ) ) /\ x e. ( Base ` R ) ) /\ a e. ( `' F " J ) ) /\ b e. ( `' F " J ) ) -> a e. ( `' F " J ) )
61 elpreima 
 |-  ( F Fn ( Base ` R ) -> ( a e. ( `' F " J ) <-> ( a e. ( Base ` R ) /\ ( F ` a ) e. J ) ) )
62 61 simplbda 
 |-  ( ( F Fn ( Base ` R ) /\ a e. ( `' F " J ) ) -> ( F ` a ) e. J )
63 33 60 62 syl2anc 
 |-  ( ( ( ( ( F e. ( R RingHom S ) /\ J e. ( LIdeal ` S ) ) /\ x e. ( Base ` R ) ) /\ a e. ( `' F " J ) ) /\ b e. ( `' F " J ) ) -> ( F ` a ) e. J )
64 24 4 55 lidlmcl 
 |-  ( ( ( S e. Ring /\ J e. ( LIdeal ` S ) ) /\ ( ( F ` x ) e. ( Base ` S ) /\ ( F ` a ) e. J ) ) -> ( ( F ` x ) ( .r ` S ) ( F ` a ) ) e. J )
65 52 54 59 63 64 syl22anc 
 |-  ( ( ( ( ( F e. ( R RingHom S ) /\ J e. ( LIdeal ` S ) ) /\ x e. ( Base ` R ) ) /\ a e. ( `' F " J ) ) /\ b e. ( `' F " J ) ) -> ( ( F ` x ) ( .r ` S ) ( F ` a ) ) e. J )
66 57 65 eqeltrd 
 |-  ( ( ( ( ( F e. ( R RingHom S ) /\ J e. ( LIdeal ` S ) ) /\ x e. ( Base ` R ) ) /\ a e. ( `' F " J ) ) /\ b e. ( `' F " J ) ) -> ( F ` ( x ( .r ` R ) a ) ) e. J )
67 simpr 
 |-  ( ( ( ( ( F e. ( R RingHom S ) /\ J e. ( LIdeal ` S ) ) /\ x e. ( Base ` R ) ) /\ a e. ( `' F " J ) ) /\ b e. ( `' F " J ) ) -> b e. ( `' F " J ) )
68 elpreima 
 |-  ( F Fn ( Base ` R ) -> ( b e. ( `' F " J ) <-> ( b e. ( Base ` R ) /\ ( F ` b ) e. J ) ) )
69 68 simplbda 
 |-  ( ( F Fn ( Base ` R ) /\ b e. ( `' F " J ) ) -> ( F ` b ) e. J )
70 33 67 69 syl2anc 
 |-  ( ( ( ( ( F e. ( R RingHom S ) /\ J e. ( LIdeal ` S ) ) /\ x e. ( Base ` R ) ) /\ a e. ( `' F " J ) ) /\ b e. ( `' F " J ) ) -> ( F ` b ) e. J )
71 24 48 lidlacl 
 |-  ( ( ( S e. Ring /\ J e. ( LIdeal ` S ) ) /\ ( ( F ` ( x ( .r ` R ) a ) ) e. J /\ ( F ` b ) e. J ) ) -> ( ( F ` ( x ( .r ` R ) a ) ) ( +g ` S ) ( F ` b ) ) e. J )
72 52 54 66 70 71 syl22anc 
 |-  ( ( ( ( ( F e. ( R RingHom S ) /\ J e. ( LIdeal ` S ) ) /\ x e. ( Base ` R ) ) /\ a e. ( `' F " J ) ) /\ b e. ( `' F " J ) ) -> ( ( F ` ( x ( .r ` R ) a ) ) ( +g ` S ) ( F ` b ) ) e. J )
73 50 72 eqeltrd 
 |-  ( ( ( ( ( F e. ( R RingHom S ) /\ J e. ( LIdeal ` S ) ) /\ x e. ( Base ` R ) ) /\ a e. ( `' F " J ) ) /\ b e. ( `' F " J ) ) -> ( F ` ( ( x ( .r ` R ) a ) ( +g ` R ) b ) ) e. J )
74 33 46 73 elpreimad 
 |-  ( ( ( ( ( F e. ( R RingHom S ) /\ J e. ( LIdeal ` S ) ) /\ x e. ( Base ` R ) ) /\ a e. ( `' F " J ) ) /\ b e. ( `' F " J ) ) -> ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. ( `' F " J ) )
75 74 anasss 
 |-  ( ( ( ( F e. ( R RingHom S ) /\ J e. ( LIdeal ` S ) ) /\ x e. ( Base ` R ) ) /\ ( a e. ( `' F " J ) /\ b e. ( `' F " J ) ) ) -> ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. ( `' F " J ) )
76 75 ralrimivva 
 |-  ( ( ( F e. ( R RingHom S ) /\ J e. ( LIdeal ` S ) ) /\ x e. ( Base ` R ) ) -> A. a e. ( `' F " J ) A. b e. ( `' F " J ) ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. ( `' F " J ) )
77 76 ralrimiva 
 |-  ( ( F e. ( R RingHom S ) /\ J e. ( LIdeal ` S ) ) -> A. x e. ( Base ` R ) A. a e. ( `' F " J ) A. b e. ( `' F " J ) ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. ( `' F " J ) )
78 1 3 44 39 islidl 
 |-  ( ( `' F " J ) e. I <-> ( ( `' F " J ) C_ ( Base ` R ) /\ ( `' F " J ) =/= (/) /\ A. x e. ( Base ` R ) A. a e. ( `' F " J ) A. b e. ( `' F " J ) ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. ( `' F " J ) ) )
79 7 31 77 78 syl3anbrc 
 |-  ( ( F e. ( R RingHom S ) /\ J e. ( LIdeal ` S ) ) -> ( `' F " J ) e. I )