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 ⊢ B = Base S
c0mhm.0 ⊢ 0 ˙ = 0 T
c0mhm.h ⊢ H = x ∈ B ⟼ 0 ˙
Assertion c0rnghm ⊢ S ∈ Rng ∧ T ∈ Ring ∖ NzRing → H ∈ S RngHomo 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 ringssrng ⊢ Ring ⊆ Rng
5 4 a1i ⊢ S ∈ Rng → Ring ⊆ Rng
6 5 ssdifssd ⊢ S ∈ Rng → Ring ∖ NzRing ⊆ Rng
7 6 sseld ⊢ S ∈ Rng → T ∈ Ring ∖ NzRing → T ∈ Rng
8 7 imdistani ⊢ S ∈ Rng ∧ T ∈ Ring ∖ NzRing → S ∈ Rng ∧ T ∈ Rng
9 rngabl ⊢ S ∈ Rng → S ∈ Abel
10 ablgrp ⊢ S ∈ Abel → S ∈ Grp
11 9 10 syl ⊢ S ∈ Rng → S ∈ Grp
12 eldifi ⊢ T ∈ Ring ∖ NzRing → T ∈ Ring
13 ringgrp ⊢ T ∈ Ring → T ∈ Grp
14 12 13 syl ⊢ T ∈ Ring ∖ NzRing → T ∈ Grp
15 1 2 3 c0ghm ⊢ S ∈ Grp ∧ T ∈ Grp → H ∈ S GrpHom T
16 11 14 15 syl2an ⊢ S ∈ Rng ∧ T ∈ Ring ∖ NzRing → H ∈ S GrpHom T
17 eqid ⊢ Base T = Base T
18 eqid ⊢ 1 T = 1 T
19 17 2 18 0ring1eq0 ⊢ T ∈ Ring ∖ NzRing → 1 T = 0 ˙
20 19 eqcomd ⊢ T ∈ Ring ∖ NzRing → 0 ˙ = 1 T
21 20 mpteq2dv ⊢ T ∈ Ring ∖ NzRing → x ∈ B ⟼ 0 ˙ = x ∈ B ⟼ 1 T
22 21 adantl ⊢ S ∈ Rng ∧ T ∈ Ring ∖ NzRing → x ∈ B ⟼ 0 ˙ = x ∈ B ⟼ 1 T
23 3 22 eqtrid ⊢ S ∈ Rng ∧ T ∈ Ring ∖ NzRing → H = x ∈ B ⟼ 1 T
24 eqid ⊢ mulGrp S = mulGrp S
25 24 rngmgp Could not format ( S e. Rng -> ( mulGrp ` S ) e. Smgrp ) : No typesetting found for |- ( S e. Rng -> ( mulGrp ` S ) e. Smgrp ) with typecode |-
26 sgrpmgm Could not format ( ( mulGrp ` S ) e. Smgrp -> ( mulGrp ` S ) e. Mgm ) : No typesetting found for |- ( ( mulGrp ` S ) e. Smgrp -> ( mulGrp ` S ) e. Mgm ) with typecode |-
27 25 26 syl ⊢ S ∈ Rng → mulGrp S ∈ Mgm
28 eqid ⊢ mulGrp T = mulGrp T
29 28 ringmgp ⊢ T ∈ Ring → mulGrp T ∈ Mnd
30 12 29 syl ⊢ T ∈ Ring ∖ NzRing → mulGrp T ∈ Mnd
31 24 1 mgpbas ⊢ B = Base mulGrp S
32 28 18 ringidval ⊢ 1 T = 0 mulGrp T
33 eqid ⊢ x ∈ B ⟼ 1 T = x ∈ B ⟼ 1 T
34 31 32 33 c0mgm ⊢ mulGrp S ∈ Mgm ∧ mulGrp T ∈ Mnd → x ∈ B ⟼ 1 T ∈ mulGrp S MgmHom mulGrp T
35 27 30 34 syl2an ⊢ S ∈ Rng ∧ T ∈ Ring ∖ NzRing → x ∈ B ⟼ 1 T ∈ mulGrp S MgmHom mulGrp T
36 23 35 eqeltrd ⊢ S ∈ Rng ∧ T ∈ Ring ∖ NzRing → H ∈ mulGrp S MgmHom mulGrp T
37 16 36 jca ⊢ S ∈ Rng ∧ T ∈ Ring ∖ NzRing → H ∈ S GrpHom T ∧ H ∈ mulGrp S MgmHom mulGrp T
38 24 28 isrnghmmul ⊢ H ∈ S RngHomo T ↔ S ∈ Rng ∧ T ∈ Rng ∧ H ∈ S GrpHom T ∧ H ∈ mulGrp S MgmHom mulGrp T
39 8 37 38 sylanbrc ⊢ S ∈ Rng ∧ T ∈ Ring ∖ NzRing → H ∈ S RngHomo T