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

Proof

Step Hyp Ref Expression
1 c0mhm.b ⊢ B = Base S
2 c0mhm.0 ⊢ 0 ˙ = 0 T
3 c0mhm.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 ∈ S GrpHom T
10 6 8 9 syl2an ⊢ S ∈ Ring ∧ T ∈ Ring ∖ NzRing → H ∈ S GrpHom T
11 eqid ⊢ Base T = Base T
12 eqid ⊢ 1 T = 1 T
13 11 2 12 0ring1eq0 ⊢ T ∈ Ring ∖ NzRing → 1 T = 0 ˙
14 13 eqcomd ⊢ T ∈ Ring ∖ NzRing → 0 ˙ = 1 T
15 14 mpteq2dv ⊢ T ∈ Ring ∖ NzRing → x ∈ B ⟼ 0 ˙ = x ∈ B ⟼ 1 T
16 15 adantl ⊢ S ∈ Ring ∧ T ∈ Ring ∖ NzRing → x ∈ B ⟼ 0 ˙ = x ∈ B ⟼ 1 T
17 3 16 syl5eq ⊢ S ∈ Ring ∧ T ∈ Ring ∖ NzRing → H = x ∈ B ⟼ 1 T
18 eqid ⊢ mulGrp S = mulGrp S
19 18 ringmgp ⊢ S ∈ Ring → mulGrp S ∈ Mnd
20 eqid ⊢ mulGrp T = mulGrp T
21 20 ringmgp ⊢ T ∈ Ring → mulGrp T ∈ Mnd
22 4 21 syl ⊢ T ∈ Ring ∖ NzRing → mulGrp T ∈ Mnd
23 18 1 mgpbas ⊢ B = Base mulGrp S
24 20 12 ringidval ⊢ 1 T = 0 mulGrp T
25 eqid ⊢ x ∈ B ⟼ 1 T = x ∈ B ⟼ 1 T
26 23 24 25 c0mhm ⊢ mulGrp S ∈ Mnd ∧ mulGrp T ∈ Mnd → x ∈ B ⟼ 1 T ∈ mulGrp S MndHom mulGrp T
27 19 22 26 syl2an ⊢ S ∈ Ring ∧ T ∈ Ring ∖ NzRing → x ∈ B ⟼ 1 T ∈ mulGrp S MndHom mulGrp T
28 17 27 eqeltrd ⊢ S ∈ Ring ∧ T ∈ Ring ∖ NzRing → H ∈ mulGrp S MndHom mulGrp T
29 10 28 jca ⊢ S ∈ Ring ∧ T ∈ Ring ∖ NzRing → H ∈ S GrpHom T ∧ H ∈ mulGrp S MndHom mulGrp T
30 18 20 isrhm ⊢ H ∈ S RingHom T ↔ S ∈ Ring ∧ T ∈ Ring ∧ H ∈ S GrpHom T ∧ H ∈ mulGrp S MndHom mulGrp T
31 5 29 30 sylanbrc ⊢ S ∈ Ring ∧ T ∈ Ring ∖ NzRing → H ∈ S RingHom T