ofaddmndmap

Description: The function operation applied to the addition for functions (with the same domain) into a monoid is a function (with the same domain) into the monoid. (Contributed by AV, 6-Apr-2019)

	Ref	Expression
Hypotheses	ofaddmndmap.r	$⊢ R = {Base}_{M}$
	ofaddmndmap.p	$⊢ \underset{˙}{+} = +_{M}$
Assertion	ofaddmndmap	$⊢ (M \in Mnd \land V \in Y \land (A \in (R^{V}) \land B \in (R^{V}))) \to A {\underset{˙}{+}}_{f} B \in (R^{V})$

Proof

Step	Hyp	Ref	Expression
1		ofaddmndmap.r	$⊢ R = {Base}_{M}$
2		ofaddmndmap.p	$⊢ \underset{˙}{+} = +_{M}$
3		simpl1	$⊢ ((M \in Mnd \land V \in Y \land (A \in (R^{V}) \land B \in (R^{V}))) \land (x \in R \land y \in R)) \to M \in Mnd$
4		simprl	$⊢ ((M \in Mnd \land V \in Y \land (A \in (R^{V}) \land B \in (R^{V}))) \land (x \in R \land y \in R)) \to x \in R$
5		simprr	$⊢ ((M \in Mnd \land V \in Y \land (A \in (R^{V}) \land B \in (R^{V}))) \land (x \in R \land y \in R)) \to y \in R$
6	1 2	mndcl	$⊢ (M \in Mnd \land x \in R \land y \in R) \to x \underset{˙}{+} y \in R$
7	3 4 5 6	syl3anc	$⊢ ((M \in Mnd \land V \in Y \land (A \in (R^{V}) \land B \in (R^{V}))) \land (x \in R \land y \in R)) \to x \underset{˙}{+} y \in R$
8		elmapi	$⊢ A \in (R^{V}) \to A : V ⟶ R$
9	8	adantr	$⊢ (A \in (R^{V}) \land B \in (R^{V})) \to A : V ⟶ R$
10	9	3ad2ant3	$⊢ (M \in Mnd \land V \in Y \land (A \in (R^{V}) \land B \in (R^{V}))) \to A : V ⟶ R$
11		elmapi	$⊢ B \in (R^{V}) \to B : V ⟶ R$
12	11	adantl	$⊢ (A \in (R^{V}) \land B \in (R^{V})) \to B : V ⟶ R$
13	12	3ad2ant3	$⊢ (M \in Mnd \land V \in Y \land (A \in (R^{V}) \land B \in (R^{V}))) \to B : V ⟶ R$
14		simp2	$⊢ (M \in Mnd \land V \in Y \land (A \in (R^{V}) \land B \in (R^{V}))) \to V \in Y$
15		inidm	$⊢ V \cap V = V$
16	7 10 13 14 14 15	off	$⊢ (M \in Mnd \land V \in Y \land (A \in (R^{V}) \land B \in (R^{V}))) \to (A {\underset{˙}{+}}_{f} B) : V ⟶ R$
17	1	fvexi	$⊢ R \in V$
18		elmapg	$⊢ (R \in V \land V \in Y) \to (A {\underset{˙}{+}}_{f} B \in (R^{V}) \leftrightarrow (A {\underset{˙}{+}}_{f} B) : V ⟶ R)$
19	17 14 18	sylancr	$⊢ (M \in Mnd \land V \in Y \land (A \in (R^{V}) \land B \in (R^{V}))) \to (A {\underset{˙}{+}}_{f} B \in (R^{V}) \leftrightarrow (A {\underset{˙}{+}}_{f} B) : V ⟶ R)$
20	16 19	mpbird	$⊢ (M \in Mnd \land V \in Y \land (A \in (R^{V}) \land B \in (R^{V}))) \to A {\underset{˙}{+}}_{f} B \in (R^{V})$

Metamath Proof Explorer

Theorem ofaddmndmap

Proof