0mhm

Description: The constant zero linear function between two monoids. (Contributed by Stefan O'Rear, 5-Sep-2015)

	Ref	Expression
Hypotheses	0mhm.z	$⊢ \underset{˙}{0} = 0_{N}$
	0mhm.b	$⊢ B = {Base}_{M}$
Assertion	0mhm	$⊢ (M \in Mnd \land N \in Mnd) \to B \times \{\underset{˙}{0}\} \in (M MndHom N)$

Proof

Step	Hyp	Ref	Expression
1		0mhm.z	$⊢ \underset{˙}{0} = 0_{N}$
2		0mhm.b	$⊢ B = {Base}_{M}$
3		id	$⊢ (M \in Mnd \land N \in Mnd) \to (M \in Mnd \land N \in Mnd)$
4		eqid	$⊢ {Base}_{N} = {Base}_{N}$
5	4 1	mndidcl	$⊢ N \in Mnd \to \underset{˙}{0} \in {Base}_{N}$
6	5	adantl	$⊢ (M \in Mnd \land N \in Mnd) \to \underset{˙}{0} \in {Base}_{N}$
7		fconst6g	$⊢ \underset{˙}{0} \in {Base}_{N} \to (B \times \{\underset{˙}{0}\}) : B ⟶ {Base}_{N}$
8	6 7	syl	$⊢ (M \in Mnd \land N \in Mnd) \to (B \times \{\underset{˙}{0}\}) : B ⟶ {Base}_{N}$
9		simpr	$⊢ (M \in Mnd \land N \in Mnd) \to N \in Mnd$
10		eqid	$⊢ +_{N} = +_{N}$
11	4 10 1	mndlid	$⊢ (N \in Mnd \land \underset{˙}{0} \in {Base}_{N}) \to \underset{˙}{0} +_{N} \underset{˙}{0} = \underset{˙}{0}$
12	11	eqcomd	$⊢ (N \in Mnd \land \underset{˙}{0} \in {Base}_{N}) \to \underset{˙}{0} = \underset{˙}{0} +_{N} \underset{˙}{0}$
13	9 5 12	syl2anc2	$⊢ (M \in Mnd \land N \in Mnd) \to \underset{˙}{0} = \underset{˙}{0} +_{N} \underset{˙}{0}$
14	13	adantr	$⊢ ((M \in Mnd \land N \in Mnd) \land (x \in B \land y \in B)) \to \underset{˙}{0} = \underset{˙}{0} +_{N} \underset{˙}{0}$
15		eqid	$⊢ +_{M} = +_{M}$
16	2 15	mndcl	$⊢ (M \in Mnd \land x \in B \land y \in B) \to x +_{M} y \in B$
17	16	3expb	$⊢ (M \in Mnd \land (x \in B \land y \in B)) \to x +_{M} y \in B$
18	17	adantlr	$⊢ ((M \in Mnd \land N \in Mnd) \land (x \in B \land y \in B)) \to x +_{M} y \in B$
19	1	fvexi	$⊢ \underset{˙}{0} \in V$
20	19	fvconst2	$⊢ x +_{M} y \in B \to (B \times \{\underset{˙}{0}\}) (x +_{M} y) = \underset{˙}{0}$
21	18 20	syl	$⊢ ((M \in Mnd \land N \in Mnd) \land (x \in B \land y \in B)) \to (B \times \{\underset{˙}{0}\}) (x +_{M} y) = \underset{˙}{0}$
22	19	fvconst2	$⊢ x \in B \to (B \times \{\underset{˙}{0}\}) (x) = \underset{˙}{0}$
23	19	fvconst2	$⊢ y \in B \to (B \times \{\underset{˙}{0}\}) (y) = \underset{˙}{0}$
24	22 23	oveqan12d	$⊢ (x \in B \land y \in B) \to (B \times \{\underset{˙}{0}\}) (x) +_{N} (B \times \{\underset{˙}{0}\}) (y) = \underset{˙}{0} +_{N} \underset{˙}{0}$
25	24	adantl	$⊢ ((M \in Mnd \land N \in Mnd) \land (x \in B \land y \in B)) \to (B \times \{\underset{˙}{0}\}) (x) +_{N} (B \times \{\underset{˙}{0}\}) (y) = \underset{˙}{0} +_{N} \underset{˙}{0}$
26	14 21 25	3eqtr4d	$⊢ ((M \in Mnd \land N \in Mnd) \land (x \in B \land y \in B)) \to (B \times \{\underset{˙}{0}\}) (x +_{M} y) = (B \times \{\underset{˙}{0}\}) (x) +_{N} (B \times \{\underset{˙}{0}\}) (y)$
27	26	ralrimivva	$⊢ (M \in Mnd \land N \in Mnd) \to \forall x \in B \forall y \in B (B \times \{\underset{˙}{0}\}) (x +_{M} y) = (B \times \{\underset{˙}{0}\}) (x) +_{N} (B \times \{\underset{˙}{0}\}) (y)$
28		eqid	$⊢ 0_{M} = 0_{M}$
29	2 28	mndidcl	$⊢ M \in Mnd \to 0_{M} \in B$
30	29	adantr	$⊢ (M \in Mnd \land N \in Mnd) \to 0_{M} \in B$
31	19	fvconst2	$⊢ 0_{M} \in B \to (B \times \{\underset{˙}{0}\}) (0_{M}) = \underset{˙}{0}$
32	30 31	syl	$⊢ (M \in Mnd \land N \in Mnd) \to (B \times \{\underset{˙}{0}\}) (0_{M}) = \underset{˙}{0}$
33	8 27 32	3jca	$⊢ (M \in Mnd \land N \in Mnd) \to ((B \times \{\underset{˙}{0}\}) : B ⟶ {Base}_{N} \land \forall x \in B \forall y \in B (B \times \{\underset{˙}{0}\}) (x +_{M} y) = (B \times \{\underset{˙}{0}\}) (x) +_{N} (B \times \{\underset{˙}{0}\}) (y) \land (B \times \{\underset{˙}{0}\}) (0_{M}) = \underset{˙}{0})$
34	2 4 15 10 28 1	ismhm	$⊢ B \times \{\underset{˙}{0}\} \in (M MndHom N) \leftrightarrow ((M \in Mnd \land N \in Mnd) \land ((B \times \{\underset{˙}{0}\}) : B ⟶ {Base}_{N} \land \forall x \in B \forall y \in B (B \times \{\underset{˙}{0}\}) (x +_{M} y) = (B \times \{\underset{˙}{0}\}) (x) +_{N} (B \times \{\underset{˙}{0}\}) (y) \land (B \times \{\underset{˙}{0}\}) (0_{M}) = \underset{˙}{0}))$
35	3 33 34	sylanbrc	$⊢ (M \in Mnd \land N \in Mnd) \to B \times \{\underset{˙}{0}\} \in (M MndHom N)$

Metamath Proof Explorer

Theorem 0mhm

Proof