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	⊢ 𝑅 = ( Base ‘ 𝑀 )
	ofaddmndmap.p	⊢ + = ( +g ‘ 𝑀 )
Assertion	ofaddmndmap	⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑌 ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( 𝐴 ∘f + 𝐵 ) ∈ ( 𝑅 ↑m 𝑉 ) )

Proof

Step	Hyp	Ref	Expression
1		ofaddmndmap.r	⊢ 𝑅 = ( Base ‘ 𝑀 )
2		ofaddmndmap.p	⊢ + = ( +g ‘ 𝑀 )
3		simpl1	⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑌 ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → 𝑀 ∈ Mnd )
4		simprl	⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑌 ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → 𝑥 ∈ 𝑅 )
5		simprr	⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑌 ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → 𝑦 ∈ 𝑅 )
6	1 2	mndcl	⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) → ( 𝑥 + 𝑦 ) ∈ 𝑅 )
7	3 4 5 6	syl3anc	⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑌 ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑅 )
8		elmapi	⊢ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) → 𝐴 : 𝑉 ⟶ 𝑅 )
9	8	adantr	⊢ ( ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) → 𝐴 : 𝑉 ⟶ 𝑅 )
10	9	3ad2ant3	⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑌 ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → 𝐴 : 𝑉 ⟶ 𝑅 )
11		elmapi	⊢ ( 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) → 𝐵 : 𝑉 ⟶ 𝑅 )
12	11	adantl	⊢ ( ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) → 𝐵 : 𝑉 ⟶ 𝑅 )
13	12	3ad2ant3	⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑌 ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → 𝐵 : 𝑉 ⟶ 𝑅 )
14		simp2	⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑌 ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → 𝑉 ∈ 𝑌 )
15		inidm	⊢ ( 𝑉 ∩ 𝑉 ) = 𝑉
16	7 10 13 14 14 15	off	⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑌 ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( 𝐴 ∘f + 𝐵 ) : 𝑉 ⟶ 𝑅 )
17	1	fvexi	⊢ 𝑅 ∈ V
18		elmapg	⊢ ( ( 𝑅 ∈ V ∧ 𝑉 ∈ 𝑌 ) → ( ( 𝐴 ∘f + 𝐵 ) ∈ ( 𝑅 ↑m 𝑉 ) ↔ ( 𝐴 ∘f + 𝐵 ) : 𝑉 ⟶ 𝑅 ) )
19	17 14 18	sylancr	⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑌 ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( ( 𝐴 ∘f + 𝐵 ) ∈ ( 𝑅 ↑m 𝑉 ) ↔ ( 𝐴 ∘f + 𝐵 ) : 𝑉 ⟶ 𝑅 ) )
20	16 19	mpbird	⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑌 ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( 𝐴 ∘f + 𝐵 ) ∈ ( 𝑅 ↑m 𝑉 ) )