This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) = (/) )