c0rnghm

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

	Ref	Expression
Hypotheses	c0rhm.b	$⊢ B = {Base}_{S}$
	c0rhm.0	$⊢ \underset{˙}{0} = 0_{T}$
	c0rhm.h	$⊢ H = (x \in B ⟼ \underset{˙}{0})$
Assertion	c0rnghm	$⊢ (S \in Rng \land T \in (Ring ∖ NzRing)) \to H \in (S RngHom T)$

Proof

Step	Hyp	Ref	Expression
1		c0rhm.b	$⊢ B = {Base}_{S}$
2		c0rhm.0	$⊢ \underset{˙}{0} = 0_{T}$
3		c0rhm.h	$⊢ H = (x \in B ⟼ \underset{˙}{0})$
4		ringssrng	$⊢ Ring \subseteq Rng$
5	4	a1i	$⊢ S \in Rng \to Ring \subseteq Rng$
6	5	ssdifssd	$⊢ S \in Rng \to Ring ∖ NzRing \subseteq Rng$
7	6	sseld	$⊢ S \in Rng \to (T \in (Ring ∖ NzRing) \to T \in Rng)$
8	7	imdistani	$⊢ (S \in Rng \land T \in (Ring ∖ NzRing)) \to (S \in Rng \land T \in Rng)$
9		rngabl	$⊢ S \in Rng \to S \in Abel$
10		ablgrp	$⊢ S \in Abel \to S \in Grp$
11	9 10	syl	$⊢ S \in Rng \to S \in Grp$
12		eldifi	$⊢ T \in (Ring ∖ NzRing) \to T \in Ring$
13		ringgrp	$⊢ T \in Ring \to T \in Grp$
14	12 13	syl	$⊢ T \in (Ring ∖ NzRing) \to T \in Grp$
15	1 2 3	c0ghm	$⊢ (S \in Grp \land T \in Grp) \to H \in (S GrpHom T)$
16	11 14 15	syl2an	$⊢ (S \in Rng \land T \in (Ring ∖ NzRing)) \to H \in (S GrpHom T)$
17		eqid	$⊢ {Base}_{T} = {Base}_{T}$
18		eqid	$⊢ 1_{T} = 1_{T}$
19	17 2 18	0ring1eq0	$⊢ T \in (Ring ∖ NzRing) \to 1_{T} = \underset{˙}{0}$
20	19	eqcomd	$⊢ T \in (Ring ∖ NzRing) \to \underset{˙}{0} = 1_{T}$
21	20	mpteq2dv	$⊢ T \in (Ring ∖ NzRing) \to (x \in B ⟼ \underset{˙}{0}) = (x \in B ⟼ 1_{T})$
22	21	adantl	$⊢ (S \in Rng \land T \in (Ring ∖ NzRing)) \to (x \in B ⟼ \underset{˙}{0}) = (x \in B ⟼ 1_{T})$
23	3 22	eqtrid	$⊢ (S \in Rng \land T \in (Ring ∖ NzRing)) \to H = (x \in 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 \in Rng \to {mulGrp}_{S} \in Mgm$
28		eqid	$⊢ {mulGrp}_{T} = {mulGrp}_{T}$
29	28	ringmgp	$⊢ T \in Ring \to {mulGrp}_{T} \in Mnd$
30	12 29	syl	$⊢ T \in (Ring ∖ NzRing) \to {mulGrp}_{T} \in Mnd$
31	24 1	mgpbas	$⊢ B = {Base}_{{mulGrp}_{S}}$
32	28 18	ringidval	$⊢ 1_{T} = 0_{{mulGrp}_{T}}$
33		eqid	$⊢ (x \in B ⟼ 1_{T}) = (x \in B ⟼ 1_{T})$
34	31 32 33	c0mgm	$⊢ ({mulGrp}_{S} \in Mgm \land {mulGrp}_{T} \in Mnd) \to (x \in B ⟼ 1_{T}) \in ({mulGrp}_{S} MgmHom {mulGrp}_{T})$
35	27 30 34	syl2an	$⊢ (S \in Rng \land T \in (Ring ∖ NzRing)) \to (x \in B ⟼ 1_{T}) \in ({mulGrp}_{S} MgmHom {mulGrp}_{T})$
36	23 35	eqeltrd	$⊢ (S \in Rng \land T \in (Ring ∖ NzRing)) \to H \in ({mulGrp}_{S} MgmHom {mulGrp}_{T})$
37	16 36	jca	$⊢ (S \in Rng \land T \in (Ring ∖ NzRing)) \to (H \in (S GrpHom T) \land H \in ({mulGrp}_{S} MgmHom {mulGrp}_{T}))$
38	24 28	isrnghmmul	$⊢ H \in (S RngHom T) \leftrightarrow ((S \in Rng \land T \in Rng) \land (H \in (S GrpHom T) \land H \in ({mulGrp}_{S} MgmHom {mulGrp}_{T})))$
39	8 37 38	sylanbrc	$⊢ (S \in Rng \land T \in (Ring ∖ NzRing)) \to H \in (S RngHom T)$

Metamath Proof Explorer

Theorem c0rnghm

Proof