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

Proof

Step Hyp Ref Expression
1 c0mhm.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
2 c0mhm.0 ⊢ 0 = ( 0g ‘ 𝑇 )
3 c0mhm.h ⊢ 𝐻 = ( 𝑥 ∈ 𝐵 ↦ 0 )
4 eldifi ⊢ ( 𝑇 ∈ ( Ring ∖ NzRing ) → 𝑇 ∈ Ring )
5 4 anim2i ⊢ ( ( 𝑆 ∈ Ring ∧ 𝑇 ∈ ( Ring ∖ NzRing ) ) → ( 𝑆 ∈ Ring ∧ 𝑇 ∈ Ring ) )
6 ringgrp ⊢ ( 𝑆 ∈ Ring → 𝑆 ∈ Grp )
7 ringgrp ⊢ ( 𝑇 ∈ Ring → 𝑇 ∈ Grp )
8 4 7 syl ⊢ ( 𝑇 ∈ ( Ring ∖ NzRing ) → 𝑇 ∈ Grp )
9 1 2 3 c0ghm ⊢ ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ) → 𝐻 ∈ ( 𝑆 GrpHom 𝑇 ) )
10 6 8 9 syl2an ⊢ ( ( 𝑆 ∈ Ring ∧ 𝑇 ∈ ( Ring ∖ NzRing ) ) → 𝐻 ∈ ( 𝑆 GrpHom 𝑇 ) )
11 eqid ⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
12 eqid ⊢ ( 1r ‘ 𝑇 ) = ( 1r ‘ 𝑇 )
13 11 2 12 0ring1eq0 ⊢ ( 𝑇 ∈ ( Ring ∖ NzRing ) → ( 1r ‘ 𝑇 ) = 0 )
14 13 eqcomd ⊢ ( 𝑇 ∈ ( Ring ∖ NzRing ) → 0 = ( 1r ‘ 𝑇 ) )
15 14 mpteq2dv ⊢ ( 𝑇 ∈ ( Ring ∖ NzRing ) → ( 𝑥 ∈ 𝐵 ↦ 0 ) = ( 𝑥 ∈ 𝐵 ↦ ( 1r ‘ 𝑇 ) ) )
16 15 adantl ⊢ ( ( 𝑆 ∈ Ring ∧ 𝑇 ∈ ( Ring ∖ NzRing ) ) → ( 𝑥 ∈ 𝐵 ↦ 0 ) = ( 𝑥 ∈ 𝐵 ↦ ( 1r ‘ 𝑇 ) ) )
17 3 16 syl5eq ⊢ ( ( 𝑆 ∈ Ring ∧ 𝑇 ∈ ( Ring ∖ NzRing ) ) → 𝐻 = ( 𝑥 ∈ 𝐵 ↦ ( 1r ‘ 𝑇 ) ) )
18 eqid ⊢ ( mulGrp ‘ 𝑆 ) = ( mulGrp ‘ 𝑆 )
19 18 ringmgp ⊢ ( 𝑆 ∈ Ring → ( mulGrp ‘ 𝑆 ) ∈ Mnd )
20 eqid ⊢ ( mulGrp ‘ 𝑇 ) = ( mulGrp ‘ 𝑇 )
21 20 ringmgp ⊢ ( 𝑇 ∈ Ring → ( mulGrp ‘ 𝑇 ) ∈ Mnd )
22 4 21 syl ⊢ ( 𝑇 ∈ ( Ring ∖ NzRing ) → ( mulGrp ‘ 𝑇 ) ∈ Mnd )
23 18 1 mgpbas ⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑆 ) )
24 20 12 ringidval ⊢ ( 1r ‘ 𝑇 ) = ( 0g ‘ ( mulGrp ‘ 𝑇 ) )
25 eqid ⊢ ( 𝑥 ∈ 𝐵 ↦ ( 1r ‘ 𝑇 ) ) = ( 𝑥 ∈ 𝐵 ↦ ( 1r ‘ 𝑇 ) )
26 23 24 25 c0mhm ⊢ ( ( ( mulGrp ‘ 𝑆 ) ∈ Mnd ∧ ( mulGrp ‘ 𝑇 ) ∈ Mnd ) → ( 𝑥 ∈ 𝐵 ↦ ( 1r ‘ 𝑇 ) ) ∈ ( ( mulGrp ‘ 𝑆 ) MndHom ( mulGrp ‘ 𝑇 ) ) )
27 19 22 26 syl2an ⊢ ( ( 𝑆 ∈ Ring ∧ 𝑇 ∈ ( Ring ∖ NzRing ) ) → ( 𝑥 ∈ 𝐵 ↦ ( 1r ‘ 𝑇 ) ) ∈ ( ( mulGrp ‘ 𝑆 ) MndHom ( mulGrp ‘ 𝑇 ) ) )
28 17 27 eqeltrd ⊢ ( ( 𝑆 ∈ Ring ∧ 𝑇 ∈ ( Ring ∖ NzRing ) ) → 𝐻 ∈ ( ( mulGrp ‘ 𝑆 ) MndHom ( mulGrp ‘ 𝑇 ) ) )
29 10 28 jca ⊢ ( ( 𝑆 ∈ Ring ∧ 𝑇 ∈ ( Ring ∖ NzRing ) ) → ( 𝐻 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐻 ∈ ( ( mulGrp ‘ 𝑆 ) MndHom ( mulGrp ‘ 𝑇 ) ) ) )
30 18 20 isrhm ⊢ ( 𝐻 ∈ ( 𝑆 RingHom 𝑇 ) ↔ ( ( 𝑆 ∈ Ring ∧ 𝑇 ∈ Ring ) ∧ ( 𝐻 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐻 ∈ ( ( mulGrp ‘ 𝑆 ) MndHom ( mulGrp ‘ 𝑇 ) ) ) ) )
31 5 29 30 sylanbrc ⊢ ( ( 𝑆 ∈ Ring ∧ 𝑇 ∈ ( Ring ∖ NzRing ) ) → 𝐻 ∈ ( 𝑆 RingHom 𝑇 ) )