Metamath Proof Explorer


Theorem rhmimaidl

Description: The image of an ideal I by a surjective ring homomorphism F is an ideal. (Contributed by Thierry Arnoux, 6-Jul-2024)

Ref Expression
Hypotheses rhmimaidl.b B = Base S
rhmimaidl.t T = LIdeal R
rhmimaidl.u U = LIdeal S
Assertion rhmimaidl F R RingHom S ran F = B I T F I U

Proof

Step Hyp Ref Expression
1 rhmimaidl.b B = Base S
2 rhmimaidl.t T = LIdeal R
3 rhmimaidl.u U = LIdeal S
4 eqid Base R = Base R
5 4 1 rhmf F R RingHom S F : Base R B
6 fimass F : Base R B F I B
7 5 6 syl F R RingHom S F I B
8 7 ad2antrr F R RingHom S ran F = B I T F I B
9 5 ffnd F R RingHom S F Fn Base R
10 9 ad2antrr F R RingHom S ran F = B I T F Fn Base R
11 rhmrcl1 F R RingHom S R Ring
12 11 ad2antrr F R RingHom S ran F = B I T R Ring
13 eqid 0 R = 0 R
14 4 13 ring0cl R Ring 0 R Base R
15 12 14 syl F R RingHom S ran F = B I T 0 R Base R
16 simpr F R RingHom S ran F = B I T I T
17 2 13 lidl0cl R Ring I T 0 R I
18 12 16 17 syl2anc F R RingHom S ran F = B I T 0 R I
19 10 15 18 fnfvimad F R RingHom S ran F = B I T F 0 R F I
20 19 ne0d F R RingHom S ran F = B I T F I
21 rhmghm F R RingHom S F R GrpHom S
22 21 ad4antr F R RingHom S I T j I i I z Base R F R GrpHom S
23 11 ad4antr F R RingHom S I T j I i I z Base R R Ring
24 simpr F R RingHom S I T j I i I z Base R z Base R
25 4 2 lidlss I T I Base R
26 25 ad4antlr F R RingHom S I T j I i I z Base R I Base R
27 simplr F R RingHom S I T j I i I z Base R i I
28 26 27 sseldd F R RingHom S I T j I i I z Base R i Base R
29 eqid R = R
30 4 29 ringcl R Ring z Base R i Base R z R i Base R
31 23 24 28 30 syl3anc F R RingHom S I T j I i I z Base R z R i Base R
32 simpllr F R RingHom S I T j I i I z Base R j I
33 26 32 sseldd F R RingHom S I T j I i I z Base R j Base R
34 eqid + R = + R
35 eqid + S = + S
36 4 34 35 ghmlin F R GrpHom S z R i Base R j Base R F z R i + R j = F z R i + S F j
37 22 31 33 36 syl3anc F R RingHom S I T j I i I z Base R F z R i + R j = F z R i + S F j
38 simp-4l F R RingHom S I T j I i I z Base R F R RingHom S
39 eqid S = S
40 4 29 39 rhmmul F R RingHom S z Base R i Base R F z R i = F z S F i
41 38 24 28 40 syl3anc F R RingHom S I T j I i I z Base R F z R i = F z S F i
42 41 oveq1d F R RingHom S I T j I i I z Base R F z R i + S F j = F z S F i + S F j
43 37 42 eqtrd F R RingHom S I T j I i I z Base R F z R i + R j = F z S F i + S F j
44 43 adantl4r F R RingHom S ran F = B I T j I i I z Base R F z R i + R j = F z S F i + S F j
45 44 adantl3r F R RingHom S ran F = B I T x B j I i I z Base R F z R i + R j = F z S F i + S F j
46 45 adantl3r F R RingHom S ran F = B I T x B a F I j I i I z Base R F z R i + R j = F z S F i + S F j
47 46 adantl3r F R RingHom S ran F = B I T x B a F I b F I j I i I z Base R F z R i + R j = F z S F i + S F j
48 47 adantllr F R RingHom S ran F = B I T x B a F I b F I j I F j = b i I z Base R F z R i + R j = F z S F i + S F j
49 48 ad4ant13 F R RingHom S ran F = B I T x B a F I b F I j I F j = b i I F i = a z Base R F z = x F z R i + R j = F z S F i + S F j
50 simpr F R RingHom S ran F = B I T x B a F I b F I j I F j = b i I F i = a z Base R F z = x F z = x
51 simpllr F R RingHom S ran F = B I T x B a F I b F I j I F j = b i I F i = a z Base R F z = x F i = a
52 50 51 oveq12d F R RingHom S ran F = B I T x B a F I b F I j I F j = b i I F i = a z Base R F z = x F z S F i = x S a
53 simp-5r F R RingHom S ran F = B I T x B a F I b F I j I F j = b i I F i = a z Base R F z = x F j = b
54 52 53 oveq12d F R RingHom S ran F = B I T x B a F I b F I j I F j = b i I F i = a z Base R F z = x F z S F i + S F j = x S a + S b
55 49 54 eqtrd F R RingHom S ran F = B I T x B a F I b F I j I F j = b i I F i = a z Base R F z = x F z R i + R j = x S a + S b
56 10 ad9antr F R RingHom S ran F = B I T x B a F I b F I j I F j = b i I F i = a z Base R F z = x F Fn Base R
57 16 25 syl F R RingHom S ran F = B I T I Base R
58 57 ad9antr F R RingHom S ran F = B I T x B a F I b F I j I F j = b i I F i = a z Base R F z = x I Base R
59 16 ad9antr F R RingHom S ran F = B I T x B a F I b F I j I F j = b i I F i = a z Base R F z = x I T
60 simplr F R RingHom S ran F = B I T x B a F I b F I j I F j = b i I F i = a z Base R F z = x z Base R
61 simp-4r F R RingHom S ran F = B I T x B a F I b F I j I F j = b i I F i = a z Base R F z = x i I
62 simp-6r F R RingHom S ran F = B I T x B a F I b F I j I F j = b i I F i = a z Base R F z = x j I
63 2 4 34 29 islidl I T I Base R I z Base R i I j I z R i + R j I
64 63 simp3bi I T z Base R i I j I z R i + R j I
65 64 r19.21bi I T z Base R i I j I z R i + R j I
66 65 r19.21bi I T z Base R i I j I z R i + R j I
67 66 r19.21bi I T z Base R i I j I z R i + R j I
68 59 60 61 62 67 syl1111anc F R RingHom S ran F = B I T x B a F I b F I j I F j = b i I F i = a z Base R F z = x z R i + R j I
69 58 68 sseldd F R RingHom S ran F = B I T x B a F I b F I j I F j = b i I F i = a z Base R F z = x z R i + R j Base R
70 56 69 68 fnfvimad F R RingHom S ran F = B I T x B a F I b F I j I F j = b i I F i = a z Base R F z = x F z R i + R j F I
71 55 70 eqeltrrd F R RingHom S ran F = B I T x B a F I b F I j I F j = b i I F i = a z Base R F z = x x S a + S b F I
72 5 ad2antrr F R RingHom S ran F = B I T F : Base R B
73 72 ffund F R RingHom S ran F = B I T Fun F
74 73 ad7antr F R RingHom S ran F = B I T x B a F I b F I j I F j = b i I F i = a Fun F
75 5 fdmd F R RingHom S dom F = Base R
76 75 imaeq2d F R RingHom S F dom F = F Base R
77 imadmrn F dom F = ran F
78 76 77 eqtr3di F R RingHom S F Base R = ran F
79 78 eqeq1d F R RingHom S F Base R = B ran F = B
80 79 biimpar F R RingHom S ran F = B F Base R = B
81 80 eleq2d F R RingHom S ran F = B x F Base R x B
82 81 biimpar F R RingHom S ran F = B x B x F Base R
83 82 adantlr F R RingHom S ran F = B I T x B x F Base R
84 83 ad6antr F R RingHom S ran F = B I T x B a F I b F I j I F j = b i I F i = a x F Base R
85 fvelima Fun F x F Base R z Base R F z = x
86 74 84 85 syl2anc F R RingHom S ran F = B I T x B a F I b F I j I F j = b i I F i = a z Base R F z = x
87 71 86 r19.29a F R RingHom S ran F = B I T x B a F I b F I j I F j = b i I F i = a x S a + S b F I
88 73 ad5antr F R RingHom S ran F = B I T x B a F I b F I j I F j = b Fun F
89 simp-4r F R RingHom S ran F = B I T x B a F I b F I j I F j = b a F I
90 fvelima Fun F a F I i I F i = a
91 88 89 90 syl2anc F R RingHom S ran F = B I T x B a F I b F I j I F j = b i I F i = a
92 87 91 r19.29a F R RingHom S ran F = B I T x B a F I b F I j I F j = b x S a + S b F I
93 73 ad3antrrr F R RingHom S ran F = B I T x B a F I b F I Fun F
94 simpr F R RingHom S ran F = B I T x B a F I b F I b F I
95 fvelima Fun F b F I j I F j = b
96 93 94 95 syl2anc F R RingHom S ran F = B I T x B a F I b F I j I F j = b
97 92 96 r19.29a F R RingHom S ran F = B I T x B a F I b F I x S a + S b F I
98 97 anasss F R RingHom S ran F = B I T x B a F I b F I x S a + S b F I
99 98 ralrimivva F R RingHom S ran F = B I T x B a F I b F I x S a + S b F I
100 99 ralrimiva F R RingHom S ran F = B I T x B a F I b F I x S a + S b F I
101 3 1 35 39 islidl F I U F I B F I x B a F I b F I x S a + S b F I
102 8 20 100 101 syl3anbrc F R RingHom S ran F = B I T F I U
103 102 3impa F R RingHom S ran F = B I T F I U