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 ) ) |