Metamath Proof Explorer

Theorem c0rnghm

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

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

Proof

Step Hyp Ref Expression
1 c0mhm.b 
 |-  B = ( Base ` S )
2 c0mhm.0 
 |-  .0. = ( 0g ` T )
3 c0mhm.h 
 |-  H = ( x e. B |-> .0. )
4 ringssrng 
 |-  Ring C_ Rng
5 4 a1i 
 |-  ( S e. Rng -> Ring C_ Rng )
6 5 ssdifssd 
 |-  ( S e. Rng -> ( Ring \ NzRing ) C_ Rng )
7 6 sseld 
 |-  ( S e. Rng -> ( T e. ( Ring \ NzRing ) -> T e. Rng ) )
8 7 imdistani 
 |-  ( ( S e. Rng /\ T e. ( Ring \ NzRing ) ) -> ( S e. Rng /\ T 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 eldifi 
 |-  ( T e. ( Ring \ NzRing ) -> T e. Ring )
13 ringgrp 
 |-  ( T e. Ring -> T e. Grp )
14 12 13 syl 
 |-  ( T e. ( Ring \ NzRing ) -> T e. Grp )
15 1 2 3 c0ghm 
 |-  ( ( S e. Grp /\ T e. Grp ) -> H e. ( S GrpHom T ) )
16 11 14 15 syl2an 
 |-  ( ( S e. Rng /\ T e. ( Ring \ NzRing ) ) -> H e. ( S GrpHom T ) )
17 eqid 
 |-  ( Base ` T ) = ( Base ` T )
18 eqid 
 |-  ( 1r ` T ) = ( 1r ` T )
19 17 2 18 0ring1eq0 
 |-  ( T e. ( Ring \ NzRing ) -> ( 1r ` T ) = .0. )
20 19 eqcomd 
 |-  ( T e. ( Ring \ NzRing ) -> .0. = ( 1r ` T ) )
21 20 mpteq2dv 
 |-  ( T e. ( Ring \ NzRing ) -> ( x e. B |-> .0. ) = ( x e. B |-> ( 1r ` T ) ) )
22 21 adantl 
 |-  ( ( S e. Rng /\ T e. ( Ring \ NzRing ) ) -> ( x e. B |-> .0. ) = ( x e. B |-> ( 1r ` T ) ) )
23 3 22 syl5eq 
 |-  ( ( S e. Rng /\ T e. ( Ring \ NzRing ) ) -> H = ( x e. B |-> ( 1r ` T ) ) )
24 eqid 
 |-  ( mulGrp ` S ) = ( mulGrp ` S )
25 24 rngmgp 
 |-  ( S e. Rng -> ( mulGrp ` S ) e. Smgrp )
26 sgrpmgm 
 |-  ( ( mulGrp ` S ) e. Smgrp -> ( mulGrp ` S ) e. Mgm )
27 25 26 syl 
 |-  ( S e. Rng -> ( mulGrp ` S ) e. Mgm )
28 eqid 
 |-  ( mulGrp ` T ) = ( mulGrp ` T )
29 28 ringmgp 
 |-  ( T e. Ring -> ( mulGrp ` T ) e. Mnd )
30 12 29 syl 
 |-  ( T e. ( Ring \ NzRing ) -> ( mulGrp ` T ) e. Mnd )
31 24 1 mgpbas 
 |-  B = ( Base ` ( mulGrp ` S ) )
32 28 18 ringidval 
 |-  ( 1r ` T ) = ( 0g ` ( mulGrp ` T ) )
33 eqid 
 |-  ( x e. B |-> ( 1r ` T ) ) = ( x e. B |-> ( 1r ` T ) )
34 31 32 33 c0mgm 
 |-  ( ( ( mulGrp ` S ) e. Mgm /\ ( mulGrp ` T ) e. Mnd ) -> ( x e. B |-> ( 1r ` T ) ) e. ( ( mulGrp ` S ) MgmHom ( mulGrp ` T ) ) )
35 27 30 34 syl2an 
 |-  ( ( S e. Rng /\ T e. ( Ring \ NzRing ) ) -> ( x e. B |-> ( 1r ` T ) ) e. ( ( mulGrp ` S ) MgmHom ( mulGrp ` T ) ) )
36 23 35 eqeltrd 
 |-  ( ( S e. Rng /\ T e. ( Ring \ NzRing ) ) -> H e. ( ( mulGrp ` S ) MgmHom ( mulGrp ` T ) ) )
37 16 36 jca 
 |-  ( ( S e. Rng /\ T e. ( Ring \ NzRing ) ) -> ( H e. ( S GrpHom T ) /\ H e. ( ( mulGrp ` S ) MgmHom ( mulGrp ` T ) ) ) )
38 24 28 isrnghmmul 
 |-  ( H e. ( S RngHomo T ) <-> ( ( S e. Rng /\ T e. Rng ) /\ ( H e. ( S GrpHom T ) /\ H e. ( ( mulGrp ` S ) MgmHom ( mulGrp ` T ) ) ) ) )
39 8 37 38 sylanbrc 
 |-  ( ( S e. Rng /\ T e. ( Ring \ NzRing ) ) -> H e. ( S RngHomo T ) )