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