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 ⊢ 𝐵 = ( Base ‘ 𝑆 )
c0mhm.0 ⊢ 0 = ( 0g ‘ 𝑇 )
c0mhm.h ⊢ 𝐻 = ( 𝑥 ∈ 𝐵 ↦ 0 )
Assertion c0rnghm ( ( 𝑆 ∈ Rng ∧ 𝑇 ∈ ( Ring ∖ NzRing ) ) → 𝐻 ∈ ( 𝑆 RngHomo 𝑇 ) )

Proof

Step Hyp Ref Expression
1 c0mhm.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
2 c0mhm.0 ⊢ 0 = ( 0g ‘ 𝑇 )
3 c0mhm.h ⊢ 𝐻 = ( 𝑥 ∈ 𝐵 ↦ 0 )
4 ringssrng ⊢ Ring ⊆ Rng
5 4 a1i ⊢ ( 𝑆 ∈ Rng → Ring ⊆ Rng )
6 5 ssdifssd ⊢ ( 𝑆 ∈ Rng → ( Ring ∖ NzRing ) ⊆ Rng )
7 6 sseld ⊢ ( 𝑆 ∈ Rng → ( 𝑇 ∈ ( Ring ∖ NzRing ) → 𝑇 ∈ Rng ) )
8 7 imdistani ⊢ ( ( 𝑆 ∈ Rng ∧ 𝑇 ∈ ( Ring ∖ NzRing ) ) → ( 𝑆 ∈ Rng ∧ 𝑇 ∈ Rng ) )
9 rngabl ⊢ ( 𝑆 ∈ Rng → 𝑆 ∈ Abel )
10 ablgrp ⊢ ( 𝑆 ∈ Abel → 𝑆 ∈ Grp )
11 9 10 syl ⊢ ( 𝑆 ∈ Rng → 𝑆 ∈ Grp )
12 eldifi ⊢ ( 𝑇 ∈ ( Ring ∖ NzRing ) → 𝑇 ∈ Ring )
13 ringgrp ⊢ ( 𝑇 ∈ Ring → 𝑇 ∈ Grp )
14 12 13 syl ⊢ ( 𝑇 ∈ ( Ring ∖ NzRing ) → 𝑇 ∈ Grp )
15 1 2 3 c0ghm ⊢ ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ) → 𝐻 ∈ ( 𝑆 GrpHom 𝑇 ) )
16 11 14 15 syl2an ⊢ ( ( 𝑆 ∈ Rng ∧ 𝑇 ∈ ( Ring ∖ NzRing ) ) → 𝐻 ∈ ( 𝑆 GrpHom 𝑇 ) )
17 eqid ⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
18 eqid ⊢ ( 1r ‘ 𝑇 ) = ( 1r ‘ 𝑇 )
19 17 2 18 0ring1eq0 ⊢ ( 𝑇 ∈ ( Ring ∖ NzRing ) → ( 1r ‘ 𝑇 ) = 0 )
20 19 eqcomd ⊢ ( 𝑇 ∈ ( Ring ∖ NzRing ) → 0 = ( 1r ‘ 𝑇 ) )
21 20 mpteq2dv ⊢ ( 𝑇 ∈ ( Ring ∖ NzRing ) → ( 𝑥 ∈ 𝐵 ↦ 0 ) = ( 𝑥 ∈ 𝐵 ↦ ( 1r ‘ 𝑇 ) ) )
22 21 adantl ⊢ ( ( 𝑆 ∈ Rng ∧ 𝑇 ∈ ( Ring ∖ NzRing ) ) → ( 𝑥 ∈ 𝐵 ↦ 0 ) = ( 𝑥 ∈ 𝐵 ↦ ( 1r ‘ 𝑇 ) ) )
23 3 22 syl5eq ⊢ ( ( 𝑆 ∈ Rng ∧ 𝑇 ∈ ( Ring ∖ NzRing ) ) → 𝐻 = ( 𝑥 ∈ 𝐵 ↦ ( 1r ‘ 𝑇 ) ) )
24 eqid ⊢ ( mulGrp ‘ 𝑆 ) = ( mulGrp ‘ 𝑆 )
25 24 rngmgp ⊢ ( 𝑆 ∈ Rng → ( mulGrp ‘ 𝑆 ) ∈ Smgrp )
26 sgrpmgm ⊢ ( ( mulGrp ‘ 𝑆 ) ∈ Smgrp → ( mulGrp ‘ 𝑆 ) ∈ Mgm )
27 25 26 syl ⊢ ( 𝑆 ∈ Rng → ( mulGrp ‘ 𝑆 ) ∈ Mgm )
28 eqid ⊢ ( mulGrp ‘ 𝑇 ) = ( mulGrp ‘ 𝑇 )
29 28 ringmgp ⊢ ( 𝑇 ∈ Ring → ( mulGrp ‘ 𝑇 ) ∈ Mnd )
30 12 29 syl ⊢ ( 𝑇 ∈ ( Ring ∖ NzRing ) → ( mulGrp ‘ 𝑇 ) ∈ Mnd )
31 24 1 mgpbas ⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑆 ) )
32 28 18 ringidval ⊢ ( 1r ‘ 𝑇 ) = ( 0g ‘ ( mulGrp ‘ 𝑇 ) )
33 eqid ⊢ ( 𝑥 ∈ 𝐵 ↦ ( 1r ‘ 𝑇 ) ) = ( 𝑥 ∈ 𝐵 ↦ ( 1r ‘ 𝑇 ) )
34 31 32 33 c0mgm ⊢ ( ( ( mulGrp ‘ 𝑆 ) ∈ Mgm ∧ ( mulGrp ‘ 𝑇 ) ∈ Mnd ) → ( 𝑥 ∈ 𝐵 ↦ ( 1r ‘ 𝑇 ) ) ∈ ( ( mulGrp ‘ 𝑆 ) MgmHom ( mulGrp ‘ 𝑇 ) ) )
35 27 30 34 syl2an ⊢ ( ( 𝑆 ∈ Rng ∧ 𝑇 ∈ ( Ring ∖ NzRing ) ) → ( 𝑥 ∈ 𝐵 ↦ ( 1r ‘ 𝑇 ) ) ∈ ( ( mulGrp ‘ 𝑆 ) MgmHom ( mulGrp ‘ 𝑇 ) ) )
36 23 35 eqeltrd ⊢ ( ( 𝑆 ∈ Rng ∧ 𝑇 ∈ ( Ring ∖ NzRing ) ) → 𝐻 ∈ ( ( mulGrp ‘ 𝑆 ) MgmHom ( mulGrp ‘ 𝑇 ) ) )
37 16 36 jca ⊢ ( ( 𝑆 ∈ Rng ∧ 𝑇 ∈ ( Ring ∖ NzRing ) ) → ( 𝐻 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐻 ∈ ( ( mulGrp ‘ 𝑆 ) MgmHom ( mulGrp ‘ 𝑇 ) ) ) )
38 24 28 isrnghmmul ⊢ ( 𝐻 ∈ ( 𝑆 RngHomo 𝑇 ) ↔ ( ( 𝑆 ∈ Rng ∧ 𝑇 ∈ Rng ) ∧ ( 𝐻 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐻 ∈ ( ( mulGrp ‘ 𝑆 ) MgmHom ( mulGrp ‘ 𝑇 ) ) ) ) )
39 8 37 38 sylanbrc ⊢ ( ( 𝑆 ∈ Rng ∧ 𝑇 ∈ ( Ring ∖ NzRing ) ) → 𝐻 ∈ ( 𝑆 RngHomo 𝑇 ) )