c0mgm

Description: The constant mapping to zero is a magma homomorphism into a monoid. Remark: Instead of the assumption that T is a monoid, it would be sufficient that T is a magma with a right or left identity. (Contributed by AV, 17-Apr-2020)

	Ref	Expression
Hypotheses	c0mhm.b	$⊢ B = {Base}_{S}$
	c0mhm.0	$⊢ \underset{˙}{0} = 0_{T}$
	c0mhm.h	$⊢ H = (x \in B ⟼ \underset{˙}{0})$
Assertion	c0mgm	$⊢ (S \in Mgm \land T \in Mnd) \to H \in (S MgmHom T)$

Proof

Step	Hyp	Ref	Expression
1		c0mhm.b	$⊢ B = {Base}_{S}$
2		c0mhm.0	$⊢ \underset{˙}{0} = 0_{T}$
3		c0mhm.h	$⊢ H = (x \in B ⟼ \underset{˙}{0})$
4		mndmgm	$⊢ T \in Mnd \to T \in Mgm$
5	4	anim2i	$⊢ (S \in Mgm \land T \in Mnd) \to (S \in Mgm \land T \in Mgm)$
6		eqid	$⊢ {Base}_{T} = {Base}_{T}$
7	6 2	mndidcl	$⊢ T \in Mnd \to \underset{˙}{0} \in {Base}_{T}$
8	7	adantl	$⊢ (S \in Mgm \land T \in Mnd) \to \underset{˙}{0} \in {Base}_{T}$
9	8	adantr	$⊢ ((S \in Mgm \land T \in Mnd) \land x \in B) \to \underset{˙}{0} \in {Base}_{T}$
10	9 3	fmptd	$⊢ (S \in Mgm \land T \in Mnd) \to H : B ⟶ {Base}_{T}$
11	7	ancli	$⊢ T \in Mnd \to (T \in Mnd \land \underset{˙}{0} \in {Base}_{T})$
12	11	adantl	$⊢ (S \in Mgm \land T \in Mnd) \to (T \in Mnd \land \underset{˙}{0} \in {Base}_{T})$
13		eqid	$⊢ +_{T} = +_{T}$
14	6 13 2	mndlid	$⊢ (T \in Mnd \land \underset{˙}{0} \in {Base}_{T}) \to \underset{˙}{0} +_{T} \underset{˙}{0} = \underset{˙}{0}$
15	12 14	syl	$⊢ (S \in Mgm \land T \in Mnd) \to \underset{˙}{0} +_{T} \underset{˙}{0} = \underset{˙}{0}$
16	15	adantr	$⊢ ((S \in Mgm \land T \in Mnd) \land (a \in B \land b \in B)) \to \underset{˙}{0} +_{T} \underset{˙}{0} = \underset{˙}{0}$
17	3	a1i	$⊢ ((S \in Mgm \land T \in Mnd) \land (a \in B \land b \in B)) \to H = (x \in B ⟼ \underset{˙}{0})$
18		eqidd	$⊢ (((S \in Mgm \land T \in Mnd) \land (a \in B \land b \in B)) \land x = a) \to \underset{˙}{0} = \underset{˙}{0}$
19		simprl	$⊢ ((S \in Mgm \land T \in Mnd) \land (a \in B \land b \in B)) \to a \in B$
20	8	adantr	$⊢ ((S \in Mgm \land T \in Mnd) \land (a \in B \land b \in B)) \to \underset{˙}{0} \in {Base}_{T}$
21	17 18 19 20	fvmptd	$⊢ ((S \in Mgm \land T \in Mnd) \land (a \in B \land b \in B)) \to H (a) = \underset{˙}{0}$
22		eqidd	$⊢ (((S \in Mgm \land T \in Mnd) \land (a \in B \land b \in B)) \land x = b) \to \underset{˙}{0} = \underset{˙}{0}$
23		simprr	$⊢ ((S \in Mgm \land T \in Mnd) \land (a \in B \land b \in B)) \to b \in B$
24	17 22 23 20	fvmptd	$⊢ ((S \in Mgm \land T \in Mnd) \land (a \in B \land b \in B)) \to H (b) = \underset{˙}{0}$
25	21 24	oveq12d	$⊢ ((S \in Mgm \land T \in Mnd) \land (a \in B \land b \in B)) \to H (a) +_{T} H (b) = \underset{˙}{0} +_{T} \underset{˙}{0}$
26		eqidd	$⊢ (((S \in Mgm \land T \in Mnd) \land (a \in B \land b \in B)) \land x = a +_{S} b) \to \underset{˙}{0} = \underset{˙}{0}$
27		eqid	$⊢ +_{S} = +_{S}$
28	1 27	mgmcl	$⊢ (S \in Mgm \land a \in B \land b \in B) \to a +_{S} b \in B$
29	28	3expb	$⊢ (S \in Mgm \land (a \in B \land b \in B)) \to a +_{S} b \in B$
30	29	adantlr	$⊢ ((S \in Mgm \land T \in Mnd) \land (a \in B \land b \in B)) \to a +_{S} b \in B$
31	17 26 30 20	fvmptd	$⊢ ((S \in Mgm \land T \in Mnd) \land (a \in B \land b \in B)) \to H (a +_{S} b) = \underset{˙}{0}$
32	16 25 31	3eqtr4rd	$⊢ ((S \in Mgm \land T \in Mnd) \land (a \in B \land b \in B)) \to H (a +_{S} b) = H (a) +_{T} H (b)$
33	32	ralrimivva	$⊢ (S \in Mgm \land T \in Mnd) \to \forall a \in B \forall b \in B H (a +_{S} b) = H (a) +_{T} H (b)$
34	10 33	jca	$⊢ (S \in Mgm \land T \in Mnd) \to (H : B ⟶ {Base}_{T} \land \forall a \in B \forall b \in B H (a +_{S} b) = H (a) +_{T} H (b))$
35	1 6 27 13	ismgmhm	$⊢ H \in (S MgmHom T) \leftrightarrow ((S \in Mgm \land T \in Mgm) \land (H : B ⟶ {Base}_{T} \land \forall a \in B \forall b \in B H (a +_{S} b) = H (a) +_{T} H (b)))$
36	5 34 35	sylanbrc	$⊢ (S \in Mgm \land T \in Mnd) \to H \in (S MgmHom T)$

Metamath Proof Explorer

Theorem c0mgm

Proof