Step |
Hyp |
Ref |
Expression |
1 |
|
kerunit.1 |
|- U = ( Unit ` R ) |
2 |
|
kerunit.2 |
|- .0. = ( 0g ` S ) |
3 |
|
kerunit.3 |
|- .1. = ( 1r ` S ) |
4 |
|
elin |
|- ( x e. ( U i^i ( `' F " { .0. } ) ) <-> ( x e. U /\ x e. ( `' F " { .0. } ) ) ) |
5 |
4
|
biimpi |
|- ( x e. ( U i^i ( `' F " { .0. } ) ) -> ( x e. U /\ x e. ( `' F " { .0. } ) ) ) |
6 |
5
|
adantl |
|- ( ( F e. ( R RingHom S ) /\ x e. ( U i^i ( `' F " { .0. } ) ) ) -> ( x e. U /\ x e. ( `' F " { .0. } ) ) ) |
7 |
6
|
simpld |
|- ( ( F e. ( R RingHom S ) /\ x e. ( U i^i ( `' F " { .0. } ) ) ) -> x e. U ) |
8 |
|
rhmrcl1 |
|- ( F e. ( R RingHom S ) -> R e. Ring ) |
9 |
|
eqid |
|- ( invr ` R ) = ( invr ` R ) |
10 |
|
eqid |
|- ( .r ` R ) = ( .r ` R ) |
11 |
|
eqid |
|- ( 1r ` R ) = ( 1r ` R ) |
12 |
1 9 10 11
|
unitlinv |
|- ( ( R e. Ring /\ x e. U ) -> ( ( ( invr ` R ) ` x ) ( .r ` R ) x ) = ( 1r ` R ) ) |
13 |
12
|
fveq2d |
|- ( ( R e. Ring /\ x e. U ) -> ( F ` ( ( ( invr ` R ) ` x ) ( .r ` R ) x ) ) = ( F ` ( 1r ` R ) ) ) |
14 |
8 13
|
sylan |
|- ( ( F e. ( R RingHom S ) /\ x e. U ) -> ( F ` ( ( ( invr ` R ) ` x ) ( .r ` R ) x ) ) = ( F ` ( 1r ` R ) ) ) |
15 |
7 14
|
syldan |
|- ( ( F e. ( R RingHom S ) /\ x e. ( U i^i ( `' F " { .0. } ) ) ) -> ( F ` ( ( ( invr ` R ) ` x ) ( .r ` R ) x ) ) = ( F ` ( 1r ` R ) ) ) |
16 |
|
simpl |
|- ( ( F e. ( R RingHom S ) /\ x e. ( U i^i ( `' F " { .0. } ) ) ) -> F e. ( R RingHom S ) ) |
17 |
8
|
adantr |
|- ( ( F e. ( R RingHom S ) /\ x e. ( U i^i ( `' F " { .0. } ) ) ) -> R e. Ring ) |
18 |
|
eqid |
|- ( Base ` R ) = ( Base ` R ) |
19 |
1 9 18
|
ringinvcl |
|- ( ( R e. Ring /\ x e. U ) -> ( ( invr ` R ) ` x ) e. ( Base ` R ) ) |
20 |
17 7 19
|
syl2anc |
|- ( ( F e. ( R RingHom S ) /\ x e. ( U i^i ( `' F " { .0. } ) ) ) -> ( ( invr ` R ) ` x ) e. ( Base ` R ) ) |
21 |
18 1
|
unitcl |
|- ( x e. U -> x e. ( Base ` R ) ) |
22 |
7 21
|
syl |
|- ( ( F e. ( R RingHom S ) /\ x e. ( U i^i ( `' F " { .0. } ) ) ) -> x e. ( Base ` R ) ) |
23 |
|
eqid |
|- ( .r ` S ) = ( .r ` S ) |
24 |
18 10 23
|
rhmmul |
|- ( ( F e. ( R RingHom S ) /\ ( ( invr ` R ) ` x ) e. ( Base ` R ) /\ x e. ( Base ` R ) ) -> ( F ` ( ( ( invr ` R ) ` x ) ( .r ` R ) x ) ) = ( ( F ` ( ( invr ` R ) ` x ) ) ( .r ` S ) ( F ` x ) ) ) |
25 |
16 20 22 24
|
syl3anc |
|- ( ( F e. ( R RingHom S ) /\ x e. ( U i^i ( `' F " { .0. } ) ) ) -> ( F ` ( ( ( invr ` R ) ` x ) ( .r ` R ) x ) ) = ( ( F ` ( ( invr ` R ) ` x ) ) ( .r ` S ) ( F ` x ) ) ) |
26 |
6
|
simprd |
|- ( ( F e. ( R RingHom S ) /\ x e. ( U i^i ( `' F " { .0. } ) ) ) -> x e. ( `' F " { .0. } ) ) |
27 |
|
eqid |
|- ( Base ` S ) = ( Base ` S ) |
28 |
18 27
|
rhmf |
|- ( F e. ( R RingHom S ) -> F : ( Base ` R ) --> ( Base ` S ) ) |
29 |
|
ffn |
|- ( F : ( Base ` R ) --> ( Base ` S ) -> F Fn ( Base ` R ) ) |
30 |
|
elpreima |
|- ( F Fn ( Base ` R ) -> ( x e. ( `' F " { .0. } ) <-> ( x e. ( Base ` R ) /\ ( F ` x ) e. { .0. } ) ) ) |
31 |
28 29 30
|
3syl |
|- ( F e. ( R RingHom S ) -> ( x e. ( `' F " { .0. } ) <-> ( x e. ( Base ` R ) /\ ( F ` x ) e. { .0. } ) ) ) |
32 |
31
|
simplbda |
|- ( ( F e. ( R RingHom S ) /\ x e. ( `' F " { .0. } ) ) -> ( F ` x ) e. { .0. } ) |
33 |
26 32
|
syldan |
|- ( ( F e. ( R RingHom S ) /\ x e. ( U i^i ( `' F " { .0. } ) ) ) -> ( F ` x ) e. { .0. } ) |
34 |
|
fvex |
|- ( F ` x ) e. _V |
35 |
34
|
elsn |
|- ( ( F ` x ) e. { .0. } <-> ( F ` x ) = .0. ) |
36 |
33 35
|
sylib |
|- ( ( F e. ( R RingHom S ) /\ x e. ( U i^i ( `' F " { .0. } ) ) ) -> ( F ` x ) = .0. ) |
37 |
36
|
oveq2d |
|- ( ( F e. ( R RingHom S ) /\ x e. ( U i^i ( `' F " { .0. } ) ) ) -> ( ( F ` ( ( invr ` R ) ` x ) ) ( .r ` S ) ( F ` x ) ) = ( ( F ` ( ( invr ` R ) ` x ) ) ( .r ` S ) .0. ) ) |
38 |
|
rhmrcl2 |
|- ( F e. ( R RingHom S ) -> S e. Ring ) |
39 |
38
|
adantr |
|- ( ( F e. ( R RingHom S ) /\ x e. ( U i^i ( `' F " { .0. } ) ) ) -> S e. Ring ) |
40 |
28
|
adantr |
|- ( ( F e. ( R RingHom S ) /\ x e. ( U i^i ( `' F " { .0. } ) ) ) -> F : ( Base ` R ) --> ( Base ` S ) ) |
41 |
40 20
|
ffvelrnd |
|- ( ( F e. ( R RingHom S ) /\ x e. ( U i^i ( `' F " { .0. } ) ) ) -> ( F ` ( ( invr ` R ) ` x ) ) e. ( Base ` S ) ) |
42 |
27 23 2
|
ringrz |
|- ( ( S e. Ring /\ ( F ` ( ( invr ` R ) ` x ) ) e. ( Base ` S ) ) -> ( ( F ` ( ( invr ` R ) ` x ) ) ( .r ` S ) .0. ) = .0. ) |
43 |
39 41 42
|
syl2anc |
|- ( ( F e. ( R RingHom S ) /\ x e. ( U i^i ( `' F " { .0. } ) ) ) -> ( ( F ` ( ( invr ` R ) ` x ) ) ( .r ` S ) .0. ) = .0. ) |
44 |
25 37 43
|
3eqtrd |
|- ( ( F e. ( R RingHom S ) /\ x e. ( U i^i ( `' F " { .0. } ) ) ) -> ( F ` ( ( ( invr ` R ) ` x ) ( .r ` R ) x ) ) = .0. ) |
45 |
11 3
|
rhm1 |
|- ( F e. ( R RingHom S ) -> ( F ` ( 1r ` R ) ) = .1. ) |
46 |
45
|
adantr |
|- ( ( F e. ( R RingHom S ) /\ x e. ( U i^i ( `' F " { .0. } ) ) ) -> ( F ` ( 1r ` R ) ) = .1. ) |
47 |
15 44 46
|
3eqtr3rd |
|- ( ( F e. ( R RingHom S ) /\ x e. ( U i^i ( `' F " { .0. } ) ) ) -> .1. = .0. ) |
48 |
47
|
reximdva0 |
|- ( ( F e. ( R RingHom S ) /\ ( U i^i ( `' F " { .0. } ) ) =/= (/) ) -> E. x e. ( U i^i ( `' F " { .0. } ) ) .1. = .0. ) |
49 |
|
id |
|- ( .1. = .0. -> .1. = .0. ) |
50 |
49
|
rexlimivw |
|- ( E. x e. ( U i^i ( `' F " { .0. } ) ) .1. = .0. -> .1. = .0. ) |
51 |
48 50
|
syl |
|- ( ( F e. ( R RingHom S ) /\ ( U i^i ( `' F " { .0. } ) ) =/= (/) ) -> .1. = .0. ) |