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 = ( 1st ` S )
keridl.2
|- Z = ( GId ` G )
Assertion keridl
|- ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RngHom S ) ) -> ( `' F " { Z } ) e. ( Idl ` R ) )

Proof

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