Metamath Proof Explorer

Theorem zrrnghm

Description: The constant mapping to zero is a nonunital ring homomorphism from the zero ring to any nonunital ring. (Contributed by AV, 17-Apr-2020)

Ref Expression
Hypotheses zrrhm.b 
|- B = ( Base ` T )
zrrhm.0 
|- .0. = ( 0g ` S )
zrrhm.h 
|- H = ( x e. B |-> .0. )
Assertion zrrnghm 
|- ( ( S e. Rng /\ T e. ( Ring \ NzRing ) ) -> H e. ( T RngHomo S ) )

Proof

Step Hyp Ref Expression
1 zrrhm.b 
 |-  B = ( Base ` T )
2 zrrhm.0 
 |-  .0. = ( 0g ` S )
3 zrrhm.h 
 |-  H = ( x e. B |-> .0. )
4 eldifi 
 |-  ( T e. ( Ring \ NzRing ) -> T e. Ring )
5 ringrng 
 |-  ( T e. Ring -> T e. Rng )
6 4 5 syl 
 |-  ( T e. ( Ring \ NzRing ) -> T e. Rng )
7 6 anim1i 
 |-  ( ( T e. ( Ring \ NzRing ) /\ S e. Rng ) -> ( T e. Rng /\ S e. Rng ) )
8 7 ancoms 
 |-  ( ( S e. Rng /\ T e. ( Ring \ NzRing ) ) -> ( T e. Rng /\ S e. Rng ) )
9 rngabl 
 |-  ( S e. Rng -> S e. Abel )
10 ablgrp 
 |-  ( S e. Abel -> S e. Grp )
11 9 10 syl 
 |-  ( S e. Rng -> S e. Grp )
12 11 adantr 
 |-  ( ( S e. Rng /\ T e. ( Ring \ NzRing ) ) -> S e. Grp )
13 ringgrp 
 |-  ( T e. Ring -> T e. Grp )
14 4 13 syl 
 |-  ( T e. ( Ring \ NzRing ) -> T e. Grp )
15 14 adantl 
 |-  ( ( S e. Rng /\ T e. ( Ring \ NzRing ) ) -> T e. Grp )
16 eqid 
 |-  ( 0g ` T ) = ( 0g ` T )
17 1 16 0ringbas 
 |-  ( T e. ( Ring \ NzRing ) -> B = { ( 0g ` T ) } )
18 17 adantl 
 |-  ( ( S e. Rng /\ T e. ( Ring \ NzRing ) ) -> B = { ( 0g ` T ) } )
19 1 2 3 16 c0snghm 
 |-  ( ( S e. Grp /\ T e. Grp /\ B = { ( 0g ` T ) } ) -> H e. ( T GrpHom S ) )
20 12 15 18 19 syl3anc 
 |-  ( ( S e. Rng /\ T e. ( Ring \ NzRing ) ) -> H e. ( T GrpHom S ) )
21 3 a1i 
 |-  ( ( ( S e. Rng /\ T e. ( Ring \ NzRing ) ) /\ B = { ( 0g ` T ) } ) -> H = ( x e. B |-> .0. ) )
22 eqidd 
 |-  ( ( ( ( S e. Rng /\ T e. ( Ring \ NzRing ) ) /\ B = { ( 0g ` T ) } ) /\ x = ( 0g ` T ) ) -> .0. = .0. )
23 1 16 ring0cl 
 |-  ( T e. Ring -> ( 0g ` T ) e. B )
24 4 23 syl 
 |-  ( T e. ( Ring \ NzRing ) -> ( 0g ` T ) e. B )
25 24 ad2antlr 
 |-  ( ( ( S e. Rng /\ T e. ( Ring \ NzRing ) ) /\ B = { ( 0g ` T ) } ) -> ( 0g ` T ) e. B )
26 2 fvexi 
 |-  .0. e. _V
27 26 a1i 
 |-  ( ( ( S e. Rng /\ T e. ( Ring \ NzRing ) ) /\ B = { ( 0g ` T ) } ) -> .0. e. _V )
28 21 22 25 27 fvmptd 
 |-  ( ( ( S e. Rng /\ T e. ( Ring \ NzRing ) ) /\ B = { ( 0g ` T ) } ) -> ( H ` ( 0g ` T ) ) = .0. )
29 eqid 
 |-  ( Base ` S ) = ( Base ` S )
30 29 2 grpidcl 
 |-  ( S e. Grp -> .0. e. ( Base ` S ) )
31 11 30 syl 
 |-  ( S e. Rng -> .0. e. ( Base ` S ) )
32 eqid 
 |-  ( .r ` S ) = ( .r ` S )
33 29 32 2 rnglz 
 |-  ( ( S e. Rng /\ .0. e. ( Base ` S ) ) -> ( .0. ( .r ` S ) .0. ) = .0. )
34 31 33 mpdan 
 |-  ( S e. Rng -> ( .0. ( .r ` S ) .0. ) = .0. )
35 34 adantr 
 |-  ( ( S e. Rng /\ T e. ( Ring \ NzRing ) ) -> ( .0. ( .r ` S ) .0. ) = .0. )
36 35 adantr 
 |-  ( ( ( S e. Rng /\ T e. ( Ring \ NzRing ) ) /\ B = { ( 0g ` T ) } ) -> ( .0. ( .r ` S ) .0. ) = .0. )
37 36 adantr 
 |-  ( ( ( ( S e. Rng /\ T e. ( Ring \ NzRing ) ) /\ B = { ( 0g ` T ) } ) /\ ( H ` ( 0g ` T ) ) = .0. ) -> ( .0. ( .r ` S ) .0. ) = .0. )
38 simpr 
 |-  ( ( ( ( S e. Rng /\ T e. ( Ring \ NzRing ) ) /\ B = { ( 0g ` T ) } ) /\ ( H ` ( 0g ` T ) ) = .0. ) -> ( H ` ( 0g ` T ) ) = .0. )
39 38 38 oveq12d 
 |-  ( ( ( ( S e. Rng /\ T e. ( Ring \ NzRing ) ) /\ B = { ( 0g ` T ) } ) /\ ( H ` ( 0g ` T ) ) = .0. ) -> ( ( H ` ( 0g ` T ) ) ( .r ` S ) ( H ` ( 0g ` T ) ) ) = ( .0. ( .r ` S ) .0. ) )
40 eqid 
 |-  ( .r ` T ) = ( .r ` T )
41 1 40 16 ringlz 
 |-  ( ( T e. Ring /\ ( 0g ` T ) e. B ) -> ( ( 0g ` T ) ( .r ` T ) ( 0g ` T ) ) = ( 0g ` T ) )
42 4 23 41 syl2anc2 
 |-  ( T e. ( Ring \ NzRing ) -> ( ( 0g ` T ) ( .r ` T ) ( 0g ` T ) ) = ( 0g ` T ) )
43 42 ad2antlr 
 |-  ( ( ( S e. Rng /\ T e. ( Ring \ NzRing ) ) /\ B = { ( 0g ` T ) } ) -> ( ( 0g ` T ) ( .r ` T ) ( 0g ` T ) ) = ( 0g ` T ) )
44 43 adantr 
 |-  ( ( ( ( S e. Rng /\ T e. ( Ring \ NzRing ) ) /\ B = { ( 0g ` T ) } ) /\ ( H ` ( 0g ` T ) ) = .0. ) -> ( ( 0g ` T ) ( .r ` T ) ( 0g ` T ) ) = ( 0g ` T ) )
45 44 fveq2d 
 |-  ( ( ( ( S e. Rng /\ T e. ( Ring \ NzRing ) ) /\ B = { ( 0g ` T ) } ) /\ ( H ` ( 0g ` T ) ) = .0. ) -> ( H ` ( ( 0g ` T ) ( .r ` T ) ( 0g ` T ) ) ) = ( H ` ( 0g ` T ) ) )
46 45 38 eqtrd 
 |-  ( ( ( ( S e. Rng /\ T e. ( Ring \ NzRing ) ) /\ B = { ( 0g ` T ) } ) /\ ( H ` ( 0g ` T ) ) = .0. ) -> ( H ` ( ( 0g ` T ) ( .r ` T ) ( 0g ` T ) ) ) = .0. )
47 37 39 46 3eqtr4rd 
 |-  ( ( ( ( S e. Rng /\ T e. ( Ring \ NzRing ) ) /\ B = { ( 0g ` T ) } ) /\ ( H ` ( 0g ` T ) ) = .0. ) -> ( H ` ( ( 0g ` T ) ( .r ` T ) ( 0g ` T ) ) ) = ( ( H ` ( 0g ` T ) ) ( .r ` S ) ( H ` ( 0g ` T ) ) ) )
48 28 47 mpdan 
 |-  ( ( ( S e. Rng /\ T e. ( Ring \ NzRing ) ) /\ B = { ( 0g ` T ) } ) -> ( H ` ( ( 0g ` T ) ( .r ` T ) ( 0g ` T ) ) ) = ( ( H ` ( 0g ` T ) ) ( .r ` S ) ( H ` ( 0g ` T ) ) ) )
49 23 23 jca 
 |-  ( T e. Ring -> ( ( 0g ` T ) e. B /\ ( 0g ` T ) e. B ) )
50 4 49 syl 
 |-  ( T e. ( Ring \ NzRing ) -> ( ( 0g ` T ) e. B /\ ( 0g ` T ) e. B ) )
51 50 ad2antlr 
 |-  ( ( ( S e. Rng /\ T e. ( Ring \ NzRing ) ) /\ B = { ( 0g ` T ) } ) -> ( ( 0g ` T ) e. B /\ ( 0g ` T ) e. B ) )
52 fvoveq1 
 |-  ( a = ( 0g ` T ) -> ( H ` ( a ( .r ` T ) c ) ) = ( H ` ( ( 0g ` T ) ( .r ` T ) c ) ) )
53 fveq2 
 |-  ( a = ( 0g ` T ) -> ( H ` a ) = ( H ` ( 0g ` T ) ) )
54 53 oveq1d 
 |-  ( a = ( 0g ` T ) -> ( ( H ` a ) ( .r ` S ) ( H ` c ) ) = ( ( H ` ( 0g ` T ) ) ( .r ` S ) ( H ` c ) ) )
55 52 54 eqeq12d 
 |-  ( a = ( 0g ` T ) -> ( ( H ` ( a ( .r ` T ) c ) ) = ( ( H ` a ) ( .r ` S ) ( H ` c ) ) <-> ( H ` ( ( 0g ` T ) ( .r ` T ) c ) ) = ( ( H ` ( 0g ` T ) ) ( .r ` S ) ( H ` c ) ) ) )
56 oveq2 
 |-  ( c = ( 0g ` T ) -> ( ( 0g ` T ) ( .r ` T ) c ) = ( ( 0g ` T ) ( .r ` T ) ( 0g ` T ) ) )
57 56 fveq2d 
 |-  ( c = ( 0g ` T ) -> ( H ` ( ( 0g ` T ) ( .r ` T ) c ) ) = ( H ` ( ( 0g ` T ) ( .r ` T ) ( 0g ` T ) ) ) )
58 fveq2 
 |-  ( c = ( 0g ` T ) -> ( H ` c ) = ( H ` ( 0g ` T ) ) )
59 58 oveq2d 
 |-  ( c = ( 0g ` T ) -> ( ( H ` ( 0g ` T ) ) ( .r ` S ) ( H ` c ) ) = ( ( H ` ( 0g ` T ) ) ( .r ` S ) ( H ` ( 0g ` T ) ) ) )
60 57 59 eqeq12d 
 |-  ( c = ( 0g ` T ) -> ( ( H ` ( ( 0g ` T ) ( .r ` T ) c ) ) = ( ( H ` ( 0g ` T ) ) ( .r ` S ) ( H ` c ) ) <-> ( H ` ( ( 0g ` T ) ( .r ` T ) ( 0g ` T ) ) ) = ( ( H ` ( 0g ` T ) ) ( .r ` S ) ( H ` ( 0g ` T ) ) ) ) )
61 55 60 2ralsng 
 |-  ( ( ( 0g ` T ) e. B /\ ( 0g ` T ) e. B ) -> ( A. a e. { ( 0g ` T ) } A. c e. { ( 0g ` T ) } ( H ` ( a ( .r ` T ) c ) ) = ( ( H ` a ) ( .r ` S ) ( H ` c ) ) <-> ( H ` ( ( 0g ` T ) ( .r ` T ) ( 0g ` T ) ) ) = ( ( H ` ( 0g ` T ) ) ( .r ` S ) ( H ` ( 0g ` T ) ) ) ) )
62 51 61 syl 
 |-  ( ( ( S e. Rng /\ T e. ( Ring \ NzRing ) ) /\ B = { ( 0g ` T ) } ) -> ( A. a e. { ( 0g ` T ) } A. c e. { ( 0g ` T ) } ( H ` ( a ( .r ` T ) c ) ) = ( ( H ` a ) ( .r ` S ) ( H ` c ) ) <-> ( H ` ( ( 0g ` T ) ( .r ` T ) ( 0g ` T ) ) ) = ( ( H ` ( 0g ` T ) ) ( .r ` S ) ( H ` ( 0g ` T ) ) ) ) )
63 48 62 mpbird 
 |-  ( ( ( S e. Rng /\ T e. ( Ring \ NzRing ) ) /\ B = { ( 0g ` T ) } ) -> A. a e. { ( 0g ` T ) } A. c e. { ( 0g ` T ) } ( H ` ( a ( .r ` T ) c ) ) = ( ( H ` a ) ( .r ` S ) ( H ` c ) ) )
64 raleq 
 |-  ( B = { ( 0g ` T ) } -> ( A. c e. B ( H ` ( a ( .r ` T ) c ) ) = ( ( H ` a ) ( .r ` S ) ( H ` c ) ) <-> A. c e. { ( 0g ` T ) } ( H ` ( a ( .r ` T ) c ) ) = ( ( H ` a ) ( .r ` S ) ( H ` c ) ) ) )
65 64 raleqbi1dv 
 |-  ( B = { ( 0g ` T ) } -> ( A. a e. B A. c e. B ( H ` ( a ( .r ` T ) c ) ) = ( ( H ` a ) ( .r ` S ) ( H ` c ) ) <-> A. a e. { ( 0g ` T ) } A. c e. { ( 0g ` T ) } ( H ` ( a ( .r ` T ) c ) ) = ( ( H ` a ) ( .r ` S ) ( H ` c ) ) ) )
66 65 adantl 
 |-  ( ( ( S e. Rng /\ T e. ( Ring \ NzRing ) ) /\ B = { ( 0g ` T ) } ) -> ( A. a e. B A. c e. B ( H ` ( a ( .r ` T ) c ) ) = ( ( H ` a ) ( .r ` S ) ( H ` c ) ) <-> A. a e. { ( 0g ` T ) } A. c e. { ( 0g ` T ) } ( H ` ( a ( .r ` T ) c ) ) = ( ( H ` a ) ( .r ` S ) ( H ` c ) ) ) )
67 63 66 mpbird 
 |-  ( ( ( S e. Rng /\ T e. ( Ring \ NzRing ) ) /\ B = { ( 0g ` T ) } ) -> A. a e. B A. c e. B ( H ` ( a ( .r ` T ) c ) ) = ( ( H ` a ) ( .r ` S ) ( H ` c ) ) )
68 18 67 mpdan 
 |-  ( ( S e. Rng /\ T e. ( Ring \ NzRing ) ) -> A. a e. B A. c e. B ( H ` ( a ( .r ` T ) c ) ) = ( ( H ` a ) ( .r ` S ) ( H ` c ) ) )
69 20 68 jca 
 |-  ( ( S e. Rng /\ T e. ( Ring \ NzRing ) ) -> ( H e. ( T GrpHom S ) /\ A. a e. B A. c e. B ( H ` ( a ( .r ` T ) c ) ) = ( ( H ` a ) ( .r ` S ) ( H ` c ) ) ) )
70 1 40 32 isrnghm 
 |-  ( H e. ( T RngHomo S ) <-> ( ( T e. Rng /\ S e. Rng ) /\ ( H e. ( T GrpHom S ) /\ A. a e. B A. c e. B ( H ` ( a ( .r ` T ) c ) ) = ( ( H ` a ) ( .r ` S ) ( H ` c ) ) ) ) )
71 8 69 70 sylanbrc 
 |-  ( ( S e. Rng /\ T e. ( Ring \ NzRing ) ) -> H e. ( T RngHomo S ) )