Metamath Proof Explorer


Theorem nrhmzr

Description: There is no ring homomorphism from the zero ring into a nonzero ring. (Contributed by AV, 18-Apr-2020)

Ref Expression
Assertion nrhmzr
|- ( ( Z e. ( Ring \ NzRing ) /\ R e. NzRing ) -> ( Z RingHom R ) = (/) )

Proof

Step Hyp Ref Expression
1 eqid
 |-  ( Base ` Z ) = ( Base ` Z )
2 eqid
 |-  ( 0g ` Z ) = ( 0g ` Z )
3 eqid
 |-  ( 1r ` Z ) = ( 1r ` Z )
4 1 2 3 0ring1eq0
 |-  ( Z e. ( Ring \ NzRing ) -> ( 1r ` Z ) = ( 0g ` Z ) )
5 4 adantr
 |-  ( ( Z e. ( Ring \ NzRing ) /\ R e. NzRing ) -> ( 1r ` Z ) = ( 0g ` Z ) )
6 5 adantr
 |-  ( ( ( Z e. ( Ring \ NzRing ) /\ R e. NzRing ) /\ f e. ( Z RingHom R ) ) -> ( 1r ` Z ) = ( 0g ` Z ) )
7 6 eqcomd
 |-  ( ( ( Z e. ( Ring \ NzRing ) /\ R e. NzRing ) /\ f e. ( Z RingHom R ) ) -> ( 0g ` Z ) = ( 1r ` Z ) )
8 7 fveq2d
 |-  ( ( ( Z e. ( Ring \ NzRing ) /\ R e. NzRing ) /\ f e. ( Z RingHom R ) ) -> ( f ` ( 0g ` Z ) ) = ( f ` ( 1r ` Z ) ) )
9 eqid
 |-  ( 1r ` R ) = ( 1r ` R )
10 3 9 rhm1
 |-  ( f e. ( Z RingHom R ) -> ( f ` ( 1r ` Z ) ) = ( 1r ` R ) )
11 10 adantl
 |-  ( ( ( Z e. ( Ring \ NzRing ) /\ R e. NzRing ) /\ f e. ( Z RingHom R ) ) -> ( f ` ( 1r ` Z ) ) = ( 1r ` R ) )
12 8 11 eqtrd
 |-  ( ( ( Z e. ( Ring \ NzRing ) /\ R e. NzRing ) /\ f e. ( Z RingHom R ) ) -> ( f ` ( 0g ` Z ) ) = ( 1r ` R ) )
13 rhmghm
 |-  ( f e. ( Z RingHom R ) -> f e. ( Z GrpHom R ) )
14 13 adantl
 |-  ( ( ( Z e. ( Ring \ NzRing ) /\ R e. NzRing ) /\ f e. ( Z RingHom R ) ) -> f e. ( Z GrpHom R ) )
15 eqid
 |-  ( 0g ` R ) = ( 0g ` R )
16 2 15 ghmid
 |-  ( f e. ( Z GrpHom R ) -> ( f ` ( 0g ` Z ) ) = ( 0g ` R ) )
17 14 16 syl
 |-  ( ( ( Z e. ( Ring \ NzRing ) /\ R e. NzRing ) /\ f e. ( Z RingHom R ) ) -> ( f ` ( 0g ` Z ) ) = ( 0g ` R ) )
18 12 17 jca
 |-  ( ( ( Z e. ( Ring \ NzRing ) /\ R e. NzRing ) /\ f e. ( Z RingHom R ) ) -> ( ( f ` ( 0g ` Z ) ) = ( 1r ` R ) /\ ( f ` ( 0g ` Z ) ) = ( 0g ` R ) ) )
19 18 ralrimiva
 |-  ( ( Z e. ( Ring \ NzRing ) /\ R e. NzRing ) -> A. f e. ( Z RingHom R ) ( ( f ` ( 0g ` Z ) ) = ( 1r ` R ) /\ ( f ` ( 0g ` Z ) ) = ( 0g ` R ) ) )
20 9 15 nzrnz
 |-  ( R e. NzRing -> ( 1r ` R ) =/= ( 0g ` R ) )
21 20 necomd
 |-  ( R e. NzRing -> ( 0g ` R ) =/= ( 1r ` R ) )
22 21 adantl
 |-  ( ( Z e. ( Ring \ NzRing ) /\ R e. NzRing ) -> ( 0g ` R ) =/= ( 1r ` R ) )
23 22 adantr
 |-  ( ( ( Z e. ( Ring \ NzRing ) /\ R e. NzRing ) /\ ( f ` ( 0g ` Z ) ) = ( 0g ` R ) ) -> ( 0g ` R ) =/= ( 1r ` R ) )
24 neeq1
 |-  ( ( f ` ( 0g ` Z ) ) = ( 0g ` R ) -> ( ( f ` ( 0g ` Z ) ) =/= ( 1r ` R ) <-> ( 0g ` R ) =/= ( 1r ` R ) ) )
25 24 adantl
 |-  ( ( ( Z e. ( Ring \ NzRing ) /\ R e. NzRing ) /\ ( f ` ( 0g ` Z ) ) = ( 0g ` R ) ) -> ( ( f ` ( 0g ` Z ) ) =/= ( 1r ` R ) <-> ( 0g ` R ) =/= ( 1r ` R ) ) )
26 23 25 mpbird
 |-  ( ( ( Z e. ( Ring \ NzRing ) /\ R e. NzRing ) /\ ( f ` ( 0g ` Z ) ) = ( 0g ` R ) ) -> ( f ` ( 0g ` Z ) ) =/= ( 1r ` R ) )
27 26 orcd
 |-  ( ( ( Z e. ( Ring \ NzRing ) /\ R e. NzRing ) /\ ( f ` ( 0g ` Z ) ) = ( 0g ` R ) ) -> ( ( f ` ( 0g ` Z ) ) =/= ( 1r ` R ) \/ ( f ` ( 0g ` Z ) ) =/= ( 0g ` R ) ) )
28 27 expcom
 |-  ( ( f ` ( 0g ` Z ) ) = ( 0g ` R ) -> ( ( Z e. ( Ring \ NzRing ) /\ R e. NzRing ) -> ( ( f ` ( 0g ` Z ) ) =/= ( 1r ` R ) \/ ( f ` ( 0g ` Z ) ) =/= ( 0g ` R ) ) ) )
29 olc
 |-  ( ( f ` ( 0g ` Z ) ) =/= ( 0g ` R ) -> ( ( f ` ( 0g ` Z ) ) =/= ( 1r ` R ) \/ ( f ` ( 0g ` Z ) ) =/= ( 0g ` R ) ) )
30 29 a1d
 |-  ( ( f ` ( 0g ` Z ) ) =/= ( 0g ` R ) -> ( ( Z e. ( Ring \ NzRing ) /\ R e. NzRing ) -> ( ( f ` ( 0g ` Z ) ) =/= ( 1r ` R ) \/ ( f ` ( 0g ` Z ) ) =/= ( 0g ` R ) ) ) )
31 28 30 pm2.61ine
 |-  ( ( Z e. ( Ring \ NzRing ) /\ R e. NzRing ) -> ( ( f ` ( 0g ` Z ) ) =/= ( 1r ` R ) \/ ( f ` ( 0g ` Z ) ) =/= ( 0g ` R ) ) )
32 neorian
 |-  ( ( ( f ` ( 0g ` Z ) ) =/= ( 1r ` R ) \/ ( f ` ( 0g ` Z ) ) =/= ( 0g ` R ) ) <-> -. ( ( f ` ( 0g ` Z ) ) = ( 1r ` R ) /\ ( f ` ( 0g ` Z ) ) = ( 0g ` R ) ) )
33 31 32 sylib
 |-  ( ( Z e. ( Ring \ NzRing ) /\ R e. NzRing ) -> -. ( ( f ` ( 0g ` Z ) ) = ( 1r ` R ) /\ ( f ` ( 0g ` Z ) ) = ( 0g ` R ) ) )
34 con3
 |-  ( ( f e. ( Z RingHom R ) -> ( ( f ` ( 0g ` Z ) ) = ( 1r ` R ) /\ ( f ` ( 0g ` Z ) ) = ( 0g ` R ) ) ) -> ( -. ( ( f ` ( 0g ` Z ) ) = ( 1r ` R ) /\ ( f ` ( 0g ` Z ) ) = ( 0g ` R ) ) -> -. f e. ( Z RingHom R ) ) )
35 33 34 syl5com
 |-  ( ( Z e. ( Ring \ NzRing ) /\ R e. NzRing ) -> ( ( f e. ( Z RingHom R ) -> ( ( f ` ( 0g ` Z ) ) = ( 1r ` R ) /\ ( f ` ( 0g ` Z ) ) = ( 0g ` R ) ) ) -> -. f e. ( Z RingHom R ) ) )
36 35 alimdv
 |-  ( ( Z e. ( Ring \ NzRing ) /\ R e. NzRing ) -> ( A. f ( f e. ( Z RingHom R ) -> ( ( f ` ( 0g ` Z ) ) = ( 1r ` R ) /\ ( f ` ( 0g ` Z ) ) = ( 0g ` R ) ) ) -> A. f -. f e. ( Z RingHom R ) ) )
37 df-ral
 |-  ( A. f e. ( Z RingHom R ) ( ( f ` ( 0g ` Z ) ) = ( 1r ` R ) /\ ( f ` ( 0g ` Z ) ) = ( 0g ` R ) ) <-> A. f ( f e. ( Z RingHom R ) -> ( ( f ` ( 0g ` Z ) ) = ( 1r ` R ) /\ ( f ` ( 0g ` Z ) ) = ( 0g ` R ) ) ) )
38 eq0
 |-  ( ( Z RingHom R ) = (/) <-> A. f -. f e. ( Z RingHom R ) )
39 36 37 38 3imtr4g
 |-  ( ( Z e. ( Ring \ NzRing ) /\ R e. NzRing ) -> ( A. f e. ( Z RingHom R ) ( ( f ` ( 0g ` Z ) ) = ( 1r ` R ) /\ ( f ` ( 0g ` Z ) ) = ( 0g ` R ) ) -> ( Z RingHom R ) = (/) ) )
40 19 39 mpd
 |-  ( ( Z e. ( Ring \ NzRing ) /\ R e. NzRing ) -> ( Z RingHom R ) = (/) )