Metamath Proof Explorer

Theorem 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 ⊢ + ˙ = + M
Assertion ofaddmndmap ⊢ M ∈ Mnd ∧ V ∈ Y ∧ A ∈ R V ∧ B ∈ R V → A + ˙ f B ∈ R V

Proof

Step Hyp Ref Expression
1 ofaddmndmap.r ⊢ R = Base M
2 ofaddmndmap.p ⊢ + ˙ = + M
3 simpl1 ⊢ M ∈ Mnd ∧ V ∈ Y ∧ A ∈ R V ∧ B ∈ R V ∧ x ∈ R ∧ y ∈ R → M ∈ Mnd
4 simprl ⊢ M ∈ Mnd ∧ V ∈ Y ∧ A ∈ R V ∧ B ∈ R V ∧ x ∈ R ∧ y ∈ R → x ∈ R
5 simprr ⊢ M ∈ Mnd ∧ V ∈ Y ∧ A ∈ R V ∧ B ∈ R V ∧ x ∈ R ∧ y ∈ R → y ∈ R
6 1 2 mndcl ⊢ M ∈ Mnd ∧ x ∈ R ∧ y ∈ R → x + ˙ y ∈ R
7 3 4 5 6 syl3anc ⊢ M ∈ Mnd ∧ V ∈ Y ∧ A ∈ R V ∧ B ∈ R V ∧ x ∈ R ∧ y ∈ R → x + ˙ y ∈ R
8 elmapi ⊢ A ∈ R V → A : V ⟶ R
9 8 adantr ⊢ A ∈ R V ∧ B ∈ R V → A : V ⟶ R
10 9 3ad2ant3 ⊢ M ∈ Mnd ∧ V ∈ Y ∧ A ∈ R V ∧ B ∈ R V → A : V ⟶ R
11 elmapi ⊢ B ∈ R V → B : V ⟶ R
12 11 adantl ⊢ A ∈ R V ∧ B ∈ R V → B : V ⟶ R
13 12 3ad2ant3 ⊢ M ∈ Mnd ∧ V ∈ Y ∧ A ∈ R V ∧ B ∈ R V → B : V ⟶ R
14 simp2 ⊢ M ∈ Mnd ∧ V ∈ Y ∧ A ∈ R V ∧ B ∈ R V → V ∈ Y
15 inidm ⊢ V ∩ V = V
16 7 10 13 14 14 15 off ⊢ M ∈ Mnd ∧ V ∈ Y ∧ A ∈ R V ∧ B ∈ R V → A + ˙ f B : V ⟶ R
17 1 fvexi ⊢ R ∈ V
18 elmapg ⊢ R ∈ V ∧ V ∈ Y → A + ˙ f B ∈ R V ↔ A + ˙ f B : V ⟶ R
19 17 14 18 sylancr ⊢ M ∈ Mnd ∧ V ∈ Y ∧ A ∈ R V ∧ B ∈ R V → A + ˙ f B ∈ R V ↔ A + ˙ f B : V ⟶ R
20 16 19 mpbird ⊢ M ∈ Mnd ∧ V ∈ Y ∧ A ∈ R V ∧ B ∈ R V → A + ˙ f B ∈ R V