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