c0mhm

Description: The constant mapping to zero is a monoid homomorphism. (Contributed by AV, 16-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	c0mhm	$⊢ (S \in Mnd \land T \in Mnd) \to H \in (S MndHom 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		eqid	$⊢ {Base}_{T} = {Base}_{T}$
5	4 2	mndidcl	$⊢ T \in Mnd \to \underset{˙}{0} \in {Base}_{T}$
6	5	adantl	$⊢ (S \in Mnd \land T \in Mnd) \to \underset{˙}{0} \in {Base}_{T}$
7	6	adantr	$⊢ ((S \in Mnd \land T \in Mnd) \land x \in B) \to \underset{˙}{0} \in {Base}_{T}$
8	7 3	fmptd	$⊢ (S \in Mnd \land T \in Mnd) \to H : B ⟶ {Base}_{T}$
9	5	ancli	$⊢ T \in Mnd \to (T \in Mnd \land \underset{˙}{0} \in {Base}_{T})$
10	9	adantl	$⊢ (S \in Mnd \land T \in Mnd) \to (T \in Mnd \land \underset{˙}{0} \in {Base}_{T})$
11		eqid	$⊢ +_{T} = +_{T}$
12	4 11 2	mndlid	$⊢ (T \in Mnd \land \underset{˙}{0} \in {Base}_{T}) \to \underset{˙}{0} +_{T} \underset{˙}{0} = \underset{˙}{0}$
13	10 12	syl	$⊢ (S \in Mnd \land T \in Mnd) \to \underset{˙}{0} +_{T} \underset{˙}{0} = \underset{˙}{0}$
14	13	adantr	$⊢ ((S \in Mnd \land T \in Mnd) \land (a \in B \land b \in B)) \to \underset{˙}{0} +_{T} \underset{˙}{0} = \underset{˙}{0}$
15	3	a1i	$⊢ ((S \in Mnd \land T \in Mnd) \land (a \in B \land b \in B)) \to H = (x \in B ⟼ \underset{˙}{0})$
16		eqidd	$⊢ (((S \in Mnd \land T \in Mnd) \land (a \in B \land b \in B)) \land x = a) \to \underset{˙}{0} = \underset{˙}{0}$
17		simprl	$⊢ ((S \in Mnd \land T \in Mnd) \land (a \in B \land b \in B)) \to a \in B$
18	6	adantr	$⊢ ((S \in Mnd \land T \in Mnd) \land (a \in B \land b \in B)) \to \underset{˙}{0} \in {Base}_{T}$
19	15 16 17 18	fvmptd	$⊢ ((S \in Mnd \land T \in Mnd) \land (a \in B \land b \in B)) \to H (a) = \underset{˙}{0}$
20		eqidd	$⊢ (((S \in Mnd \land T \in Mnd) \land (a \in B \land b \in B)) \land x = b) \to \underset{˙}{0} = \underset{˙}{0}$
21		simprr	$⊢ ((S \in Mnd \land T \in Mnd) \land (a \in B \land b \in B)) \to b \in B$
22	15 20 21 18	fvmptd	$⊢ ((S \in Mnd \land T \in Mnd) \land (a \in B \land b \in B)) \to H (b) = \underset{˙}{0}$
23	19 22	oveq12d	$⊢ ((S \in Mnd \land T \in Mnd) \land (a \in B \land b \in B)) \to H (a) +_{T} H (b) = \underset{˙}{0} +_{T} \underset{˙}{0}$
24		eqidd	$⊢ (((S \in Mnd \land T \in Mnd) \land (a \in B \land b \in B)) \land x = a +_{S} b) \to \underset{˙}{0} = \underset{˙}{0}$
25		eqid	$⊢ +_{S} = +_{S}$
26	1 25	mndcl	$⊢ (S \in Mnd \land a \in B \land b \in B) \to a +_{S} b \in B$
27	26	3expb	$⊢ (S \in Mnd \land (a \in B \land b \in B)) \to a +_{S} b \in B$
28	27	adantlr	$⊢ ((S \in Mnd \land T \in Mnd) \land (a \in B \land b \in B)) \to a +_{S} b \in B$
29	15 24 28 18	fvmptd	$⊢ ((S \in Mnd \land T \in Mnd) \land (a \in B \land b \in B)) \to H (a +_{S} b) = \underset{˙}{0}$
30	14 23 29	3eqtr4rd	$⊢ ((S \in Mnd \land T \in Mnd) \land (a \in B \land b \in B)) \to H (a +_{S} b) = H (a) +_{T} H (b)$
31	30	ralrimivva	$⊢ (S \in Mnd \land T \in Mnd) \to \forall a \in B \forall b \in B H (a +_{S} b) = H (a) +_{T} H (b)$
32	3	a1i	$⊢ (S \in Mnd \land T \in Mnd) \to H = (x \in B ⟼ \underset{˙}{0})$
33		eqidd	$⊢ ((S \in Mnd \land T \in Mnd) \land x = 0_{S}) \to \underset{˙}{0} = \underset{˙}{0}$
34		eqid	$⊢ 0_{S} = 0_{S}$
35	1 34	mndidcl	$⊢ S \in Mnd \to 0_{S} \in B$
36	35	adantr	$⊢ (S \in Mnd \land T \in Mnd) \to 0_{S} \in B$
37	32 33 36 6	fvmptd	$⊢ (S \in Mnd \land T \in Mnd) \to H (0_{S}) = \underset{˙}{0}$
38	8 31 37	3jca	$⊢ (S \in Mnd \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) \land H (0_{S}) = \underset{˙}{0})$
39	38	ancli	$⊢ (S \in Mnd \land T \in Mnd) \to ((S \in Mnd \land T \in Mnd) \land (H : B ⟶ {Base}_{T} \land \forall a \in B \forall b \in B H (a +_{S} b) = H (a) +_{T} H (b) \land H (0_{S}) = \underset{˙}{0}))$
40	1 4 25 11 34 2	ismhm	$⊢ H \in (S MndHom T) \leftrightarrow ((S \in Mnd \land T \in Mnd) \land (H : B ⟶ {Base}_{T} \land \forall a \in B \forall b \in B H (a +_{S} b) = H (a) +_{T} H (b) \land H (0_{S}) = \underset{˙}{0}))$
41	39 40	sylibr	$⊢ (S \in Mnd \land T \in Mnd) \to H \in (S MndHom T)$

Metamath Proof Explorer

Theorem c0mhm

Proof