Metamath Proof Explorer

Theorem zrrnghm

Description: The constant mapping to zero is a non-unital ring homomorphism from the zero ring to any non-unital ring. (Contributed by AV, 17-Apr-2020)

Ref Expression
Hypotheses zrrhm.b ⊢B=BaseT
zrrhm.0 ⊢0˙=0S
zrrhm.h ⊢H=x∈B⟼0˙
Assertion zrrnghm ⊢S∈Rng∧T∈Ring∖NzRing→H∈TRngHomoS

Proof

Step Hyp Ref Expression
1 zrrhm.b ⊢B=BaseT
2 zrrhm.0 ⊢0˙=0S
3 zrrhm.h ⊢H=x∈B⟼0˙
4 eldifi ⊢T∈Ring∖NzRing→T∈Ring
5 ringrng ⊢T∈Ring→T∈Rng
6 4 5 syl ⊢T∈Ring∖NzRing→T∈Rng
7 6 anim1i ⊢T∈Ring∖NzRing∧S∈Rng→T∈Rng∧S∈Rng
8 7 ancoms ⊢S∈Rng∧T∈Ring∖NzRing→T∈Rng∧S∈Rng
9 rngabl ⊢S∈Rng→S∈Abel
10 ablgrp ⊢S∈Abel→S∈Grp
11 9 10 syl ⊢S∈Rng→S∈Grp
12 11 adantr ⊢S∈Rng∧T∈Ring∖NzRing→S∈Grp
13 ringgrp ⊢T∈Ring→T∈Grp
14 4 13 syl ⊢T∈Ring∖NzRing→T∈Grp
15 14 adantl ⊢S∈Rng∧T∈Ring∖NzRing→T∈Grp
16 eqid ⊢0T=0T
17 1 16 0ringbas ⊢T∈Ring∖NzRing→B=0T
18 17 adantl ⊢S∈Rng∧T∈Ring∖NzRing→B=0T
19 1 2 3 16 c0snghm ⊢S∈Grp∧T∈Grp∧B=0T→H∈TGrpHomS
20 12 15 18 19 syl3anc ⊢S∈Rng∧T∈Ring∖NzRing→H∈TGrpHomS
21 3 a1i ⊢S∈Rng∧T∈Ring∖NzRing∧B=0T→H=x∈B⟼0˙
22 eqidd ⊢S∈Rng∧T∈Ring∖NzRing∧B=0T∧x=0T→0˙=0˙
23 1 16 ring0cl ⊢T∈Ring→0T∈B
24 4 23 syl ⊢T∈Ring∖NzRing→0T∈B
25 24 ad2antlr ⊢S∈Rng∧T∈Ring∖NzRing∧B=0T→0T∈B
26 2 fvexi ⊢0˙∈V
27 26 a1i ⊢S∈Rng∧T∈Ring∖NzRing∧B=0T→0˙∈V
28 21 22 25 27 fvmptd ⊢S∈Rng∧T∈Ring∖NzRing∧B=0T→H⁡0T=0˙
29 eqid ⊢BaseS=BaseS
30 29 2 grpidcl ⊢S∈Grp→0˙∈BaseS
31 11 30 syl ⊢S∈Rng→0˙∈BaseS
32 eqid ⊢⋅S=⋅S
33 29 32 2 rnglz ⊢S∈Rng∧0˙∈BaseS→0˙⋅S0˙=0˙
34 31 33 mpdan ⊢S∈Rng→0˙⋅S0˙=0˙
35 34 adantr ⊢S∈Rng∧T∈Ring∖NzRing→0˙⋅S0˙=0˙
36 35 adantr ⊢S∈Rng∧T∈Ring∖NzRing∧B=0T→0˙⋅S0˙=0˙
37 36 adantr ⊢S∈Rng∧T∈Ring∖NzRing∧B=0T∧H⁡0T=0˙→0˙⋅S0˙=0˙
38 simpr ⊢S∈Rng∧T∈Ring∖NzRing∧B=0T∧H⁡0T=0˙→H⁡0T=0˙
39 38 38 oveq12d ⊢S∈Rng∧T∈Ring∖NzRing∧B=0T∧H⁡0T=0˙→H⁡0T⋅SH⁡0T=0˙⋅S0˙
40 eqid ⊢⋅T=⋅T
41 1 40 16 ringlz ⊢T∈Ring∧0T∈B→0T⋅T0T=0T
42 4 23 41 syl2anc2 ⊢T∈Ring∖NzRing→0T⋅T0T=0T
43 42 ad2antlr ⊢S∈Rng∧T∈Ring∖NzRing∧B=0T→0T⋅T0T=0T
44 43 adantr ⊢S∈Rng∧T∈Ring∖NzRing∧B=0T∧H⁡0T=0˙→0T⋅T0T=0T
45 44 fveq2d ⊢S∈Rng∧T∈Ring∖NzRing∧B=0T∧H⁡0T=0˙→H⁡0T⋅T0T=H⁡0T
46 45 38 eqtrd ⊢S∈Rng∧T∈Ring∖NzRing∧B=0T∧H⁡0T=0˙→H⁡0T⋅T0T=0˙
47 37 39 46 3eqtr4rd ⊢S∈Rng∧T∈Ring∖NzRing∧B=0T∧H⁡0T=0˙→H⁡0T⋅T0T=H⁡0T⋅SH⁡0T
48 28 47 mpdan ⊢S∈Rng∧T∈Ring∖NzRing∧B=0T→H⁡0T⋅T0T=H⁡0T⋅SH⁡0T
49 23 23 jca ⊢T∈Ring→0T∈B∧0T∈B
50 4 49 syl ⊢T∈Ring∖NzRing→0T∈B∧0T∈B
51 50 ad2antlr ⊢S∈Rng∧T∈Ring∖NzRing∧B=0T→0T∈B∧0T∈B
52 fvoveq1 ⊢a=0T→H⁡a⋅Tc=H⁡0T⋅Tc
53 fveq2 ⊢a=0T→H⁡a=H⁡0T
54 53 oveq1d ⊢a=0T→H⁡a⋅SH⁡c=H⁡0T⋅SH⁡c
55 52 54 eqeq12d ⊢a=0T→H⁡a⋅Tc=H⁡a⋅SH⁡c↔H⁡0T⋅Tc=H⁡0T⋅SH⁡c
56 oveq2 ⊢c=0T→0T⋅Tc=0T⋅T0T
57 56 fveq2d ⊢c=0T→H⁡0T⋅Tc=H⁡0T⋅T0T
58 fveq2 ⊢c=0T→H⁡c=H⁡0T
59 58 oveq2d ⊢c=0T→H⁡0T⋅SH⁡c=H⁡0T⋅SH⁡0T
60 57 59 eqeq12d ⊢c=0T→H⁡0T⋅Tc=H⁡0T⋅SH⁡c↔H⁡0T⋅T0T=H⁡0T⋅SH⁡0T
61 55 60 2ralsng ⊢0T∈B∧0T∈B→∀a∈0T∀c∈0TH⁡a⋅Tc=H⁡a⋅SH⁡c↔H⁡0T⋅T0T=H⁡0T⋅SH⁡0T
62 51 61 syl ⊢S∈Rng∧T∈Ring∖NzRing∧B=0T→∀a∈0T∀c∈0TH⁡a⋅Tc=H⁡a⋅SH⁡c↔H⁡0T⋅T0T=H⁡0T⋅SH⁡0T
63 48 62 mpbird ⊢S∈Rng∧T∈Ring∖NzRing∧B=0T→∀a∈0T∀c∈0TH⁡a⋅Tc=H⁡a⋅SH⁡c
64 raleq ⊢B=0T→∀c∈BH⁡a⋅Tc=H⁡a⋅SH⁡c↔∀c∈0TH⁡a⋅Tc=H⁡a⋅SH⁡c
65 64 raleqbi1dv ⊢B=0T→∀a∈B∀c∈BH⁡a⋅Tc=H⁡a⋅SH⁡c↔∀a∈0T∀c∈0TH⁡a⋅Tc=H⁡a⋅SH⁡c
66 65 adantl ⊢S∈Rng∧T∈Ring∖NzRing∧B=0T→∀a∈B∀c∈BH⁡a⋅Tc=H⁡a⋅SH⁡c↔∀a∈0T∀c∈0TH⁡a⋅Tc=H⁡a⋅SH⁡c
67 63 66 mpbird ⊢S∈Rng∧T∈Ring∖NzRing∧B=0T→∀a∈B∀c∈BH⁡a⋅Tc=H⁡a⋅SH⁡c
68 18 67 mpdan ⊢S∈Rng∧T∈Ring∖NzRing→∀a∈B∀c∈BH⁡a⋅Tc=H⁡a⋅SH⁡c
69 20 68 jca ⊢S∈Rng∧T∈Ring∖NzRing→H∈TGrpHomS∧∀a∈B∀c∈BH⁡a⋅Tc=H⁡a⋅SH⁡c
70 1 40 32 isrnghm ⊢H∈TRngHomoS↔T∈Rng∧S∈Rng∧H∈TGrpHomS∧∀a∈B∀c∈BH⁡a⋅Tc=H⁡a⋅SH⁡c
71 8 69 70 sylanbrc ⊢S∈Rng∧T∈Ring∖NzRing→H∈TRngHomoS