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 RingOpsHom 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 RingOpsHom S ) ) -> F : ran ( 1st ` R ) --> ran G )
8 3 7 fssdm 
 |-  ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom 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 RingOpsHom S ) ) -> ( GId ` ( 1st ` R ) ) e. ran ( 1st ` R ) )
12 4 9 1 2 rngohom0 
 |-  ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom 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 RingOpsHom 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 RingOpsHom 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 RingOpsHom 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 RingOpsHom 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 RingOpsHom 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 RingOpsHom 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 RingOpsHom S ) ) -> ( Z G Z ) = Z )
30 29 ad2antrr 
 |-  ( ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom 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 RingOpsHom 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 RingOpsHom 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 RingOpsHom 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 RingOpsHom 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 RingOpsHom 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 RingOpsHom 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 RingOpsHom 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 biimtrid 
 |-  ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom 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 RingOpsHom 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 RingOpsHom 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 RingOpsHom 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 RingOpsHom 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 RingOpsHom 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 RingOpsHom 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 RingOpsHom 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 RingOpsHom 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 RingOpsHom 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 RingOpsHom 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 RingOpsHom 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 RingOpsHom 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 RingOpsHom 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 RingOpsHom 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 RingOpsHom 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 RingOpsHom 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 RingOpsHom S ) ) /\ z e. ran ( 1st ` R ) ) -> ( ( F ` z ) ( 2nd ` S ) Z ) = Z )
76 75 adantlr 
 |-  ( ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom 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 RingOpsHom 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 RingOpsHom 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 RingOpsHom 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 RingOpsHom 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 RingOpsHom 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 RingOpsHom 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 RingOpsHom 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 RingOpsHom 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 RingOpsHom 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 RingOpsHom 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 RingOpsHom 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 RingOpsHom 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 RingOpsHom 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 RingOpsHom S ) ) /\ z e. ran ( 1st ` R ) ) -> ( Z ( 2nd ` S ) ( F ` z ) ) = Z )
99 98 adantlr 
 |-  ( ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom 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 RingOpsHom 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 RingOpsHom 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 RingOpsHom 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 RingOpsHom 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 RingOpsHom 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 RingOpsHom 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 RingOpsHom 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 RingOpsHom 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 biimtrid 
 |-  ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom 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 RingOpsHom 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 RingOpsHom 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 RingOpsHom 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 RingOpsHom 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 RingOpsHom 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 RingOpsHom S ) ) -> ( `' F " { Z } ) e. ( Idl ` R ) )