Metamath Proof Explorer


Theorem keridl

Description: The kernel of a ring homomorphism is an ideal. (Contributed by Jeff Madsen, 3-Jan-2011)

Ref Expression
Hypotheses keridl.1 G = 1 st S
keridl.2 Z = GId G
Assertion keridl R RingOps S RingOps F R RngHom S F -1 Z Idl R

Proof

Step Hyp Ref Expression
1 keridl.1 G = 1 st S
2 keridl.2 Z = GId G
3 cnvimass F -1 Z dom F
4 eqid 1 st R = 1 st R
5 eqid ran 1 st R = ran 1 st R
6 eqid ran G = ran G
7 4 5 1 6 rngohomf R RingOps S RingOps F R RngHom S F : ran 1 st R ran G
8 3 7 fssdm R RingOps S RingOps F R RngHom S F -1 Z ran 1 st R
9 eqid GId 1 st R = GId 1 st R
10 4 5 9 rngo0cl R RingOps GId 1 st R ran 1 st R
11 10 3ad2ant1 R RingOps S RingOps F R RngHom S GId 1 st R ran 1 st R
12 4 9 1 2 rngohom0 R RingOps S RingOps F R RngHom S F GId 1 st R = Z
13 fvex F GId 1 st R V
14 13 elsn F GId 1 st R Z F GId 1 st R = Z
15 12 14 sylibr R RingOps S RingOps F R RngHom S F GId 1 st R Z
16 ffn F : ran 1 st R ran G F Fn ran 1 st R
17 elpreima F Fn ran 1 st R GId 1 st R F -1 Z GId 1 st R ran 1 st R F GId 1 st R Z
18 7 16 17 3syl R RingOps S RingOps F R RngHom S GId 1 st R F -1 Z GId 1 st R ran 1 st R F GId 1 st R Z
19 11 15 18 mpbir2and R RingOps S RingOps F R RngHom S GId 1 st R F -1 Z
20 an4 x ran 1 st R F x Z y ran 1 st R F y Z x ran 1 st R y ran 1 st R F x Z F y Z
21 4 5 1 rngohomadd R RingOps S RingOps F R RngHom S x ran 1 st R y ran 1 st R F x 1 st R y = F x G F y
22 21 adantr R RingOps S RingOps F R RngHom S x ran 1 st R y ran 1 st R F x = Z F y = Z F x 1 st R y = F x G F y
23 oveq12 F x = Z F y = Z F x G F y = Z G Z
24 23 adantl R RingOps S RingOps F R RngHom S x ran 1 st R y ran 1 st R F x = Z F y = Z F x G F y = Z G Z
25 1 rngogrpo S RingOps G GrpOp
26 6 2 grpoidcl G GrpOp Z ran G
27 6 2 grpolid G GrpOp Z ran G Z G Z = Z
28 25 26 27 syl2anc2 S RingOps Z G Z = Z
29 28 3ad2ant2 R RingOps S RingOps F R RngHom S Z G Z = Z
30 29 ad2antrr R RingOps S RingOps F R RngHom S x ran 1 st R y ran 1 st R F x = Z F y = Z Z G Z = Z
31 22 24 30 3eqtrd R RingOps S RingOps F R RngHom S x ran 1 st R y ran 1 st R F x = Z F y = Z F x 1 st R y = Z
32 31 ex R RingOps S RingOps F R RngHom S x ran 1 st R y ran 1 st R F x = Z F y = Z F x 1 st R y = Z
33 fvex F x V
34 33 elsn F x Z F x = Z
35 fvex F y V
36 35 elsn F y Z F y = Z
37 34 36 anbi12i F x Z F y Z F x = Z F y = Z
38 fvex F x 1 st R y V
39 38 elsn F x 1 st R y Z F x 1 st R y = Z
40 32 37 39 3imtr4g R RingOps S RingOps F R RngHom S x ran 1 st R y ran 1 st R F x Z F y Z F x 1 st R y Z
41 40 imdistanda R RingOps S RingOps F R RngHom S x ran 1 st R y ran 1 st R F x Z F y Z x ran 1 st R y ran 1 st R F x 1 st R y Z
42 4 5 rngogcl R RingOps x ran 1 st R y ran 1 st R x 1 st R y ran 1 st R
43 42 3expib R RingOps x ran 1 st R y ran 1 st R x 1 st R y ran 1 st R
44 43 3ad2ant1 R RingOps S RingOps F R RngHom S x ran 1 st R y ran 1 st R x 1 st R y ran 1 st R
45 44 anim1d R RingOps S RingOps F R RngHom S x ran 1 st R y ran 1 st R F x 1 st R y Z x 1 st R y ran 1 st R F x 1 st R y Z
46 41 45 syld R RingOps S RingOps F R RngHom S x ran 1 st R y ran 1 st R F x Z F y Z x 1 st R y ran 1 st R F x 1 st R y Z
47 20 46 syl5bi R RingOps S RingOps F R RngHom S x ran 1 st R F x Z y ran 1 st R F y Z x 1 st R y ran 1 st R F x 1 st R y Z
48 elpreima F Fn ran 1 st R x F -1 Z x ran 1 st R F x Z
49 7 16 48 3syl R RingOps S RingOps F R RngHom S x F -1 Z x ran 1 st R F x Z
50 elpreima F Fn ran 1 st R y F -1 Z y ran 1 st R F y Z
51 7 16 50 3syl R RingOps S RingOps F R RngHom S y F -1 Z y ran 1 st R F y Z
52 49 51 anbi12d R RingOps S RingOps F R RngHom S x F -1 Z y F -1 Z x ran 1 st R F x Z y ran 1 st R F y Z
53 elpreima F Fn ran 1 st R x 1 st R y F -1 Z x 1 st R y ran 1 st R F x 1 st R y Z
54 7 16 53 3syl R RingOps S RingOps F R RngHom S x 1 st R y F -1 Z x 1 st R y ran 1 st R F x 1 st R y Z
55 47 52 54 3imtr4d R RingOps S RingOps F R RngHom S x F -1 Z y F -1 Z x 1 st R y F -1 Z
56 55 impl R RingOps S RingOps F R RngHom S x F -1 Z y F -1 Z x 1 st R y F -1 Z
57 56 ralrimiva R RingOps S RingOps F R RngHom S x F -1 Z y F -1 Z x 1 st R y F -1 Z
58 34 anbi2i x ran 1 st R F x Z x ran 1 st R F x = Z
59 eqid 2 nd R = 2 nd R
60 4 59 5 rngocl R RingOps z ran 1 st R x ran 1 st R z 2 nd R x ran 1 st R
61 60 3expb R RingOps z ran 1 st R x ran 1 st R z 2 nd R x ran 1 st R
62 61 3ad2antl1 R RingOps S RingOps F R RngHom S z ran 1 st R x ran 1 st R z 2 nd R x ran 1 st R
63 62 anass1rs R RingOps S RingOps F R RngHom S x ran 1 st R z ran 1 st R z 2 nd R x ran 1 st R
64 63 adantlrr R RingOps S RingOps F R RngHom S x ran 1 st R F x = Z z ran 1 st R z 2 nd R x ran 1 st R
65 eqid 2 nd S = 2 nd S
66 4 5 59 65 rngohommul R RingOps S RingOps F R RngHom S z ran 1 st R x ran 1 st R F z 2 nd R x = F z 2 nd S F x
67 66 anass1rs R RingOps S RingOps F R RngHom S x ran 1 st R z ran 1 st R F z 2 nd R x = F z 2 nd S F x
68 67 adantlrr R RingOps S RingOps F R RngHom S x ran 1 st R F x = Z z ran 1 st R F z 2 nd R x = F z 2 nd S F x
69 oveq2 F x = Z F z 2 nd S F x = F z 2 nd S Z
70 69 adantl x ran 1 st R F x = Z F z 2 nd S F x = F z 2 nd S Z
71 70 ad2antlr R RingOps S RingOps F R RngHom S x ran 1 st R F x = Z z ran 1 st R F z 2 nd S F x = F z 2 nd S Z
72 4 5 1 6 rngohomcl R RingOps S RingOps F R RngHom S z ran 1 st R F z ran G
73 2 6 1 65 rngorz S RingOps F z ran G F z 2 nd S Z = Z
74 73 3ad2antl2 R RingOps S RingOps F R RngHom S F z ran G F z 2 nd S Z = Z
75 72 74 syldan R RingOps S RingOps F R RngHom S z ran 1 st R F z 2 nd S Z = Z
76 75 adantlr R RingOps S RingOps F R RngHom S x ran 1 st R F x = Z z ran 1 st R F z 2 nd S Z = Z
77 68 71 76 3eqtrd R RingOps S RingOps F R RngHom S x ran 1 st R F x = Z z ran 1 st R F z 2 nd R x = Z
78 fvex F z 2 nd R x V
79 78 elsn F z 2 nd R x Z F z 2 nd R x = Z
80 77 79 sylibr R RingOps S RingOps F R RngHom S x ran 1 st R F x = Z z ran 1 st R F z 2 nd R x Z
81 elpreima F Fn ran 1 st R z 2 nd R x F -1 Z z 2 nd R x ran 1 st R F z 2 nd R x Z
82 7 16 81 3syl R RingOps S RingOps F R RngHom S z 2 nd R x F -1 Z z 2 nd R x ran 1 st R F z 2 nd R x Z
83 82 ad2antrr R RingOps S RingOps F R RngHom S x ran 1 st R F x = Z z ran 1 st R z 2 nd R x F -1 Z z 2 nd R x ran 1 st R F z 2 nd R x Z
84 64 80 83 mpbir2and R RingOps S RingOps F R RngHom S x ran 1 st R F x = Z z ran 1 st R z 2 nd R x F -1 Z
85 4 59 5 rngocl R RingOps x ran 1 st R z ran 1 st R x 2 nd R z ran 1 st R
86 85 3expb R RingOps x ran 1 st R z ran 1 st R x 2 nd R z ran 1 st R
87 86 3ad2antl1 R RingOps S RingOps F R RngHom S x ran 1 st R z ran 1 st R x 2 nd R z ran 1 st R
88 87 anassrs R RingOps S RingOps F R RngHom S x ran 1 st R z ran 1 st R x 2 nd R z ran 1 st R
89 88 adantlrr R RingOps S RingOps F R RngHom S x ran 1 st R F x = Z z ran 1 st R x 2 nd R z ran 1 st R
90 4 5 59 65 rngohommul R RingOps S RingOps F R RngHom S x ran 1 st R z ran 1 st R F x 2 nd R z = F x 2 nd S F z
91 90 anassrs R RingOps S RingOps F R RngHom S x ran 1 st R z ran 1 st R F x 2 nd R z = F x 2 nd S F z
92 91 adantlrr R RingOps S RingOps F R RngHom S x ran 1 st R F x = Z z ran 1 st R F x 2 nd R z = F x 2 nd S F z
93 oveq1 F x = Z F x 2 nd S F z = Z 2 nd S F z
94 93 adantl x ran 1 st R F x = Z F x 2 nd S F z = Z 2 nd S F z
95 94 ad2antlr R RingOps S RingOps F R RngHom S x ran 1 st R F x = Z z ran 1 st R F x 2 nd S F z = Z 2 nd S F z
96 2 6 1 65 rngolz S RingOps F z ran G Z 2 nd S F z = Z
97 96 3ad2antl2 R RingOps S RingOps F R RngHom S F z ran G Z 2 nd S F z = Z
98 72 97 syldan R RingOps S RingOps F R RngHom S z ran 1 st R Z 2 nd S F z = Z
99 98 adantlr R RingOps S RingOps F R RngHom S x ran 1 st R F x = Z z ran 1 st R Z 2 nd S F z = Z
100 92 95 99 3eqtrd R RingOps S RingOps F R RngHom S x ran 1 st R F x = Z z ran 1 st R F x 2 nd R z = Z
101 fvex F x 2 nd R z V
102 101 elsn F x 2 nd R z Z F x 2 nd R z = Z
103 100 102 sylibr R RingOps S RingOps F R RngHom S x ran 1 st R F x = Z z ran 1 st R F x 2 nd R z Z
104 elpreima F Fn ran 1 st R x 2 nd R z F -1 Z x 2 nd R z ran 1 st R F x 2 nd R z Z
105 7 16 104 3syl R RingOps S RingOps F R RngHom S x 2 nd R z F -1 Z x 2 nd R z ran 1 st R F x 2 nd R z Z
106 105 ad2antrr R RingOps S RingOps F R RngHom S x ran 1 st R F x = Z z ran 1 st R x 2 nd R z F -1 Z x 2 nd R z ran 1 st R F x 2 nd R z Z
107 89 103 106 mpbir2and R RingOps S RingOps F R RngHom S x ran 1 st R F x = Z z ran 1 st R x 2 nd R z F -1 Z
108 84 107 jca R RingOps S RingOps F R RngHom S x ran 1 st R F x = Z z ran 1 st R z 2 nd R x F -1 Z x 2 nd R z F -1 Z
109 108 ralrimiva R RingOps S RingOps F R RngHom S x ran 1 st R F x = Z z ran 1 st R z 2 nd R x F -1 Z x 2 nd R z F -1 Z
110 109 ex R RingOps S RingOps F R RngHom S x ran 1 st R F x = Z z ran 1 st R z 2 nd R x F -1 Z x 2 nd R z F -1 Z
111 58 110 syl5bi R RingOps S RingOps F R RngHom S x ran 1 st R F x Z z ran 1 st R z 2 nd R x F -1 Z x 2 nd R z F -1 Z
112 49 111 sylbid R RingOps S RingOps F R RngHom S x F -1 Z z ran 1 st R z 2 nd R x F -1 Z x 2 nd R z F -1 Z
113 112 imp R RingOps S RingOps F R RngHom S x F -1 Z z ran 1 st R z 2 nd R x F -1 Z x 2 nd R z F -1 Z
114 57 113 jca R RingOps S RingOps F R RngHom S x F -1 Z y F -1 Z x 1 st R y F -1 Z z ran 1 st R z 2 nd R x F -1 Z x 2 nd R z F -1 Z
115 114 ralrimiva R RingOps S RingOps F R RngHom S x F -1 Z y F -1 Z x 1 st R y F -1 Z z ran 1 st R z 2 nd R x F -1 Z x 2 nd R z F -1 Z
116 4 59 5 9 isidl R RingOps F -1 Z Idl R F -1 Z ran 1 st R GId 1 st R F -1 Z x F -1 Z y F -1 Z x 1 st R y F -1 Z z ran 1 st R z 2 nd R x F -1 Z x 2 nd R z F -1 Z
117 116 3ad2ant1 R RingOps S RingOps F R RngHom S F -1 Z Idl R F -1 Z ran 1 st R GId 1 st R F -1 Z x F -1 Z y F -1 Z x 1 st R y F -1 Z z ran 1 st R z 2 nd R x F -1 Z x 2 nd R z F -1 Z
118 8 19 115 117 mpbir3and R RingOps S RingOps F R RngHom S F -1 Z Idl R