Metamath Proof Explorer

Theorem c0rhm

Description: The constant mapping to zero is a ring homomorphism from any 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 c0rhm 
|- ( ( S e. Ring /\ T e. ( Ring \ NzRing ) ) -> H e. ( S RingHom 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 eldifi 
 |-  ( T e. ( Ring \ NzRing ) -> T e. Ring )
5 4 anim2i 
 |-  ( ( S e. Ring /\ T e. ( Ring \ NzRing ) ) -> ( S e. Ring /\ T e. Ring ) )
6 ringgrp 
 |-  ( S e. Ring -> S e. Grp )
7 ringgrp 
 |-  ( T e. Ring -> T e. Grp )
8 4 7 syl 
 |-  ( T e. ( Ring \ NzRing ) -> T e. Grp )
9 1 2 3 c0ghm 
 |-  ( ( S e. Grp /\ T e. Grp ) -> H e. ( S GrpHom T ) )
10 6 8 9 syl2an 
 |-  ( ( S e. Ring /\ T e. ( Ring \ NzRing ) ) -> H e. ( S GrpHom T ) )
11 eqid 
 |-  ( Base ` T ) = ( Base ` T )
12 eqid 
 |-  ( 1r ` T ) = ( 1r ` T )
13 11 2 12 0ring1eq0 
 |-  ( T e. ( Ring \ NzRing ) -> ( 1r ` T ) = .0. )
14 13 eqcomd 
 |-  ( T e. ( Ring \ NzRing ) -> .0. = ( 1r ` T ) )
15 14 mpteq2dv 
 |-  ( T e. ( Ring \ NzRing ) -> ( x e. B |-> .0. ) = ( x e. B |-> ( 1r ` T ) ) )
16 15 adantl 
 |-  ( ( S e. Ring /\ T e. ( Ring \ NzRing ) ) -> ( x e. B |-> .0. ) = ( x e. B |-> ( 1r ` T ) ) )
17 3 16 syl5eq 
 |-  ( ( S e. Ring /\ T e. ( Ring \ NzRing ) ) -> H = ( x e. B |-> ( 1r ` T ) ) )
18 eqid 
 |-  ( mulGrp ` S ) = ( mulGrp ` S )
19 18 ringmgp 
 |-  ( S e. Ring -> ( mulGrp ` S ) e. Mnd )
20 eqid 
 |-  ( mulGrp ` T ) = ( mulGrp ` T )
21 20 ringmgp 
 |-  ( T e. Ring -> ( mulGrp ` T ) e. Mnd )
22 4 21 syl 
 |-  ( T e. ( Ring \ NzRing ) -> ( mulGrp ` T ) e. Mnd )
23 18 1 mgpbas 
 |-  B = ( Base ` ( mulGrp ` S ) )
24 20 12 ringidval 
 |-  ( 1r ` T ) = ( 0g ` ( mulGrp ` T ) )
25 eqid 
 |-  ( x e. B |-> ( 1r ` T ) ) = ( x e. B |-> ( 1r ` T ) )
26 23 24 25 c0mhm 
 |-  ( ( ( mulGrp ` S ) e. Mnd /\ ( mulGrp ` T ) e. Mnd ) -> ( x e. B |-> ( 1r ` T ) ) e. ( ( mulGrp ` S ) MndHom ( mulGrp ` T ) ) )
27 19 22 26 syl2an 
 |-  ( ( S e. Ring /\ T e. ( Ring \ NzRing ) ) -> ( x e. B |-> ( 1r ` T ) ) e. ( ( mulGrp ` S ) MndHom ( mulGrp ` T ) ) )
28 17 27 eqeltrd 
 |-  ( ( S e. Ring /\ T e. ( Ring \ NzRing ) ) -> H e. ( ( mulGrp ` S ) MndHom ( mulGrp ` T ) ) )
29 10 28 jca 
 |-  ( ( S e. Ring /\ T e. ( Ring \ NzRing ) ) -> ( H e. ( S GrpHom T ) /\ H e. ( ( mulGrp ` S ) MndHom ( mulGrp ` T ) ) ) )
30 18 20 isrhm 
 |-  ( H e. ( S RingHom T ) <-> ( ( S e. Ring /\ T e. Ring ) /\ ( H e. ( S GrpHom T ) /\ H e. ( ( mulGrp ` S ) MndHom ( mulGrp ` T ) ) ) ) )
31 5 29 30 sylanbrc 
 |-  ( ( S e. Ring /\ T e. ( Ring \ NzRing ) ) -> H e. ( S RingHom T ) )