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 c0rhm.b ⊢B=BaseS
c0rhm.0 ⊢0˙=0T
c0rhm.h ⊢H=x∈B⟼0˙
Assertion c0rhm ⊢S∈Ring∧T∈Ring∖NzRing→H∈SRingHomT

Proof

Step Hyp Ref Expression
1 c0rhm.b ⊢B=BaseS
2 c0rhm.0 ⊢0˙=0T
3 c0rhm.h ⊢H=x∈B⟼0˙
4 eldifi ⊢T∈Ring∖NzRing→T∈Ring
5 4 anim2i ⊢S∈Ring∧T∈Ring∖NzRing→S∈Ring∧T∈Ring
6 ringgrp ⊢S∈Ring→S∈Grp
7 ringgrp ⊢T∈Ring→T∈Grp
8 4 7 syl ⊢T∈Ring∖NzRing→T∈Grp
9 1 2 3 c0ghm ⊢S∈Grp∧T∈Grp→H∈SGrpHomT
10 6 8 9 syl2an ⊢S∈Ring∧T∈Ring∖NzRing→H∈SGrpHomT
11 eqid ⊢BaseT=BaseT
12 eqid ⊢1T=1T
13 11 2 12 0ring1eq0 ⊢T∈Ring∖NzRing→1T=0˙
14 13 eqcomd ⊢T∈Ring∖NzRing→0˙=1T
15 14 mpteq2dv ⊢T∈Ring∖NzRing→x∈B⟼0˙=x∈B⟼1T
16 15 adantl ⊢S∈Ring∧T∈Ring∖NzRing→x∈B⟼0˙=x∈B⟼1T
17 3 16 eqtrid ⊢S∈Ring∧T∈Ring∖NzRing→H=x∈B⟼1T
18 eqid ⊢mulGrpS=mulGrpS
19 18 ringmgp ⊢S∈Ring→mulGrpS∈Mnd
20 eqid ⊢mulGrpT=mulGrpT
21 20 ringmgp ⊢T∈Ring→mulGrpT∈Mnd
22 4 21 syl ⊢T∈Ring∖NzRing→mulGrpT∈Mnd
23 18 1 mgpbas ⊢B=BasemulGrpS
24 20 12 ringidval ⊢1T=0mulGrpT
25 eqid ⊢x∈B⟼1T=x∈B⟼1T
26 23 24 25 c0mhm ⊢mulGrpS∈Mnd∧mulGrpT∈Mnd→x∈B⟼1T∈mulGrpSMndHommulGrpT
27 19 22 26 syl2an ⊢S∈Ring∧T∈Ring∖NzRing→x∈B⟼1T∈mulGrpSMndHommulGrpT
28 17 27 eqeltrd ⊢S∈Ring∧T∈Ring∖NzRing→H∈mulGrpSMndHommulGrpT
29 10 28 jca ⊢S∈Ring∧T∈Ring∖NzRing→H∈SGrpHomT∧H∈mulGrpSMndHommulGrpT
30 18 20 isrhm ⊢H∈SRingHomT↔S∈Ring∧T∈Ring∧H∈SGrpHomT∧H∈mulGrpSMndHommulGrpT
31 5 29 30 sylanbrc ⊢S∈Ring∧T∈Ring∖NzRing→H∈SRingHomT