c0snmgmhm

Description: The constant mapping to zero is a magma homomorphism from a magma with one element to any monoid. (Contributed by AV, 17-Apr-2020)

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

Proof

Step	Hyp	Ref	Expression
1		zrrhm.b	$⊢ B = {Base}_{T}$
2		zrrhm.0	$⊢ \underset{˙}{0} = 0_{S}$
3		zrrhm.h	$⊢ H = (x \in B ⟼ \underset{˙}{0})$
4		mndmgm	$⊢ S \in Mnd \to S \in Mgm$
5	4	anim1i	$⊢ (S \in Mnd \land T \in Mgm) \to (S \in Mgm \land T \in Mgm)$
6	5	3adant3	$⊢ (S \in Mnd \land T \in Mgm \land \|B\| = 1) \to (S \in Mgm \land T \in Mgm)$
7	6	ancomd	$⊢ (S \in Mnd \land T \in Mgm \land \|B\| = 1) \to (T \in Mgm \land S \in Mgm)$
8	1	fvexi	$⊢ B \in V$
9		hash1snb	$⊢ B \in V \to (\|B\| = 1 \leftrightarrow \exists b B = \{b\})$
10	8 9	ax-mp	$⊢ \|B\| = 1 \leftrightarrow \exists b B = \{b\}$
11		eqid	$⊢ {Base}_{S} = {Base}_{S}$
12	11 2	mndidcl	$⊢ S \in Mnd \to \underset{˙}{0} \in {Base}_{S}$
13	12	adantr	$⊢ (S \in Mnd \land T \in Mgm) \to \underset{˙}{0} \in {Base}_{S}$
14	13	adantr	$⊢ ((S \in Mnd \land T \in Mgm) \land B = \{b\}) \to \underset{˙}{0} \in {Base}_{S}$
15	14	adantr	$⊢ (((S \in Mnd \land T \in Mgm) \land B = \{b\}) \land x \in B) \to \underset{˙}{0} \in {Base}_{S}$
16	15 3	fmptd	$⊢ ((S \in Mnd \land T \in Mgm) \land B = \{b\}) \to H : B ⟶ {Base}_{S}$
17	3	a1i	$⊢ ((S \in Mnd \land T \in Mgm) \land B = \{b\}) \to H = (x \in B ⟼ \underset{˙}{0})$
18		eqidd	$⊢ (((S \in Mnd \land T \in Mgm) \land B = \{b\}) \land x = b) \to \underset{˙}{0} = \underset{˙}{0}$
19		vsnid	$⊢ b \in \{b\}$
20	19	a1i	$⊢ B = \{b\} \to b \in \{b\}$
21		eleq2	$⊢ B = \{b\} \to (b \in B \leftrightarrow b \in \{b\})$
22	20 21	mpbird	$⊢ B = \{b\} \to b \in B$
23	22	adantl	$⊢ ((S \in Mnd \land T \in Mgm) \land B = \{b\}) \to b \in B$
24	17 18 23 14	fvmptd	$⊢ ((S \in Mnd \land T \in Mgm) \land B = \{b\}) \to H (b) = \underset{˙}{0}$
25		simpr	$⊢ (((S \in Mnd \land T \in Mgm) \land B = \{b\}) \land H (b) = \underset{˙}{0}) \to H (b) = \underset{˙}{0}$
26	25 25	oveq12d	$⊢ (((S \in Mnd \land T \in Mgm) \land B = \{b\}) \land H (b) = \underset{˙}{0}) \to H (b) +_{S} H (b) = \underset{˙}{0} +_{S} \underset{˙}{0}$
27		eqid	$⊢ +_{S} = +_{S}$
28	11 27 2	mndlid	$⊢ (S \in Mnd \land \underset{˙}{0} \in {Base}_{S}) \to \underset{˙}{0} +_{S} \underset{˙}{0} = \underset{˙}{0}$
29	12 28	mpdan	$⊢ S \in Mnd \to \underset{˙}{0} +_{S} \underset{˙}{0} = \underset{˙}{0}$
30	29	adantr	$⊢ (S \in Mnd \land T \in Mgm) \to \underset{˙}{0} +_{S} \underset{˙}{0} = \underset{˙}{0}$
31	30	adantr	$⊢ ((S \in Mnd \land T \in Mgm) \land B = \{b\}) \to \underset{˙}{0} +_{S} \underset{˙}{0} = \underset{˙}{0}$
32	31	adantr	$⊢ (((S \in Mnd \land T \in Mgm) \land B = \{b\}) \land H (b) = \underset{˙}{0}) \to \underset{˙}{0} +_{S} \underset{˙}{0} = \underset{˙}{0}$
33		simpr	$⊢ (S \in Mnd \land T \in Mgm) \to T \in Mgm$
34	33	adantr	$⊢ ((S \in Mnd \land T \in Mgm) \land B = \{b\}) \to T \in Mgm$
35	34	adantr	$⊢ (((S \in Mnd \land T \in Mgm) \land B = \{b\}) \land b \in B) \to T \in Mgm$
36		simpr	$⊢ (((S \in Mnd \land T \in Mgm) \land B = \{b\}) \land b \in B) \to b \in B$
37		eqid	$⊢ +_{T} = +_{T}$
38	1 37	mgmcl	$⊢ (T \in Mgm \land b \in B \land b \in B) \to b +_{T} b \in B$
39	35 36 36 38	syl3anc	$⊢ (((S \in Mnd \land T \in Mgm) \land B = \{b\}) \land b \in B) \to b +_{T} b \in B$
40		eleq2	$⊢ B = \{b\} \to (b +_{T} b \in B \leftrightarrow b +_{T} b \in \{b\})$
41		elsni	$⊢ b +_{T} b \in \{b\} \to b +_{T} b = b$
42	40 41	syl6bi	$⊢ B = \{b\} \to (b +_{T} b \in B \to b +_{T} b = b)$
43	42	adantl	$⊢ ((S \in Mnd \land T \in Mgm) \land B = \{b\}) \to (b +_{T} b \in B \to b +_{T} b = b)$
44	43	adantr	$⊢ (((S \in Mnd \land T \in Mgm) \land B = \{b\}) \land b \in B) \to (b +_{T} b \in B \to b +_{T} b = b)$
45	39 44	mpd	$⊢ (((S \in Mnd \land T \in Mgm) \land B = \{b\}) \land b \in B) \to b +_{T} b = b$
46	23 45	mpdan	$⊢ ((S \in Mnd \land T \in Mgm) \land B = \{b\}) \to b +_{T} b = b$
47	46	fveq2d	$⊢ ((S \in Mnd \land T \in Mgm) \land B = \{b\}) \to H (b +_{T} b) = H (b)$
48	47	adantr	$⊢ (((S \in Mnd \land T \in Mgm) \land B = \{b\}) \land H (b) = \underset{˙}{0}) \to H (b +_{T} b) = H (b)$
49	48 25	eqtr2d	$⊢ (((S \in Mnd \land T \in Mgm) \land B = \{b\}) \land H (b) = \underset{˙}{0}) \to \underset{˙}{0} = H (b +_{T} b)$
50	26 32 49	3eqtrrd	$⊢ (((S \in Mnd \land T \in Mgm) \land B = \{b\}) \land H (b) = \underset{˙}{0}) \to H (b +_{T} b) = H (b) +_{S} H (b)$
51	24 50	mpdan	$⊢ ((S \in Mnd \land T \in Mgm) \land B = \{b\}) \to H (b +_{T} b) = H (b) +_{S} H (b)$
52		id	$⊢ B = \{b\} \to B = \{b\}$
53	52	raleqdv	$⊢ B = \{b\} \to (\forall c \in B H (a +_{T} c) = H (a) +_{S} H (c) \leftrightarrow \forall c \in \{b\} H (a +_{T} c) = H (a) +_{S} H (c))$
54	52 53	raleqbidv	$⊢ B = \{b\} \to (\forall a \in B \forall c \in B H (a +_{T} c) = H (a) +_{S} H (c) \leftrightarrow \forall a \in \{b\} \forall c \in \{b\} H (a +_{T} c) = H (a) +_{S} H (c))$
55	54	adantl	$⊢ ((S \in Mnd \land T \in Mgm) \land B = \{b\}) \to (\forall a \in B \forall c \in B H (a +_{T} c) = H (a) +_{S} H (c) \leftrightarrow \forall a \in \{b\} \forall c \in \{b\} H (a +_{T} c) = H (a) +_{S} H (c))$
56		fvoveq1	$⊢ a = b \to H (a +_{T} c) = H (b +_{T} c)$
57		fveq2	$⊢ a = b \to H (a) = H (b)$
58	57	oveq1d	$⊢ a = b \to H (a) +_{S} H (c) = H (b) +_{S} H (c)$
59	56 58	eqeq12d	$⊢ a = b \to (H (a +_{T} c) = H (a) +_{S} H (c) \leftrightarrow H (b +_{T} c) = H (b) +_{S} H (c))$
60		oveq2	$⊢ c = b \to b +_{T} c = b +_{T} b$
61	60	fveq2d	$⊢ c = b \to H (b +_{T} c) = H (b +_{T} b)$
62		fveq2	$⊢ c = b \to H (c) = H (b)$
63	62	oveq2d	$⊢ c = b \to H (b) +_{S} H (c) = H (b) +_{S} H (b)$
64	61 63	eqeq12d	$⊢ c = b \to (H (b +_{T} c) = H (b) +_{S} H (c) \leftrightarrow H (b +_{T} b) = H (b) +_{S} H (b))$
65	59 64	2ralsng	$⊢ (b \in V \land b \in V) \to (\forall a \in \{b\} \forall c \in \{b\} H (a +_{T} c) = H (a) +_{S} H (c) \leftrightarrow H (b +_{T} b) = H (b) +_{S} H (b))$
66	65	el2v	$⊢ \forall a \in \{b\} \forall c \in \{b\} H (a +_{T} c) = H (a) +_{S} H (c) \leftrightarrow H (b +_{T} b) = H (b) +_{S} H (b)$
67	55 66	bitrdi	$⊢ ((S \in Mnd \land T \in Mgm) \land B = \{b\}) \to (\forall a \in B \forall c \in B H (a +_{T} c) = H (a) +_{S} H (c) \leftrightarrow H (b +_{T} b) = H (b) +_{S} H (b))$
68	51 67	mpbird	$⊢ ((S \in Mnd \land T \in Mgm) \land B = \{b\}) \to \forall a \in B \forall c \in B H (a +_{T} c) = H (a) +_{S} H (c)$
69	16 68	jca	$⊢ ((S \in Mnd \land T \in Mgm) \land B = \{b\}) \to (H : B ⟶ {Base}_{S} \land \forall a \in B \forall c \in B H (a +_{T} c) = H (a) +_{S} H (c))$
70	69	ex	$⊢ (S \in Mnd \land T \in Mgm) \to (B = \{b\} \to (H : B ⟶ {Base}_{S} \land \forall a \in B \forall c \in B H (a +_{T} c) = H (a) +_{S} H (c)))$
71	70	exlimdv	$⊢ (S \in Mnd \land T \in Mgm) \to (\exists b B = \{b\} \to (H : B ⟶ {Base}_{S} \land \forall a \in B \forall c \in B H (a +_{T} c) = H (a) +_{S} H (c)))$
72	10 71	syl5bi	$⊢ (S \in Mnd \land T \in Mgm) \to (\|B\| = 1 \to (H : B ⟶ {Base}_{S} \land \forall a \in B \forall c \in B H (a +_{T} c) = H (a) +_{S} H (c)))$
73	72	3impia	$⊢ (S \in Mnd \land T \in Mgm \land \|B\| = 1) \to (H : B ⟶ {Base}_{S} \land \forall a \in B \forall c \in B H (a +_{T} c) = H (a) +_{S} H (c))$
74	1 11 37 27	ismgmhm	$⊢ H \in (T MgmHom S) \leftrightarrow ((T \in Mgm \land S \in Mgm) \land (H : B ⟶ {Base}_{S} \land \forall a \in B \forall c \in B H (a +_{T} c) = H (a) +_{S} H (c)))$
75	7 73 74	sylanbrc	$⊢ (S \in Mnd \land T \in Mgm \land \|B\| = 1) \to H \in (T MgmHom S)$

Metamath Proof Explorer

Theorem c0snmgmhm

Proof