Metamath Proof Explorer

Theorem kerunit

Description: If a unit element lies in the kernel of a ring homomorphism, then 0 = 1 , i.e. the target ring is the zero ring. (Contributed by Thierry Arnoux, 24-Oct-2017)

Ref Expression
Hypotheses kerunit.1 
|- U = ( Unit ` R )
kerunit.2 
|- .0. = ( 0g ` S )
kerunit.3 
|- .1. = ( 1r ` S )
Assertion kerunit 
|- ( ( F e. ( R RingHom S ) /\ ( U i^i ( `' F " { .0. } ) ) =/= (/) ) -> .1. = .0. )

Proof

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 ffvelcdmd 
 |-  ( ( 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. )