Theorem mzpaddmpt

Description: Sum of polynomial functions is polynomial. Maps-to version of mzpadd . (Contributed by Stefan O'Rear, 5-Oct-2014)

	Ref	Expression
Assertion	mzpaddmpt	⊢ ( ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐵 ) ∈ ( mzPoly ‘ 𝑉 ) ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 + 𝐵 ) ) ∈ ( mzPoly ‘ 𝑉 ) )

Proof

Step	Hyp	Ref	Expression
1		mzpf	⊢ ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) : ( ℤ ↑m 𝑉 ) ⟶ ℤ )
2	1	ffnd	⊢ ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) Fn ( ℤ ↑m 𝑉 ) )
3		mzpf	⊢ ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐵 ) ∈ ( mzPoly ‘ 𝑉 ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐵 ) : ( ℤ ↑m 𝑉 ) ⟶ ℤ )
4	3	ffnd	⊢ ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐵 ) ∈ ( mzPoly ‘ 𝑉 ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐵 ) Fn ( ℤ ↑m 𝑉 ) )
5		ovex	⊢ ( ℤ ↑m 𝑉 ) ∈ V
6		ofmpteq	⊢ ( ( ( ℤ ↑m 𝑉 ) ∈ V ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) Fn ( ℤ ↑m 𝑉 ) ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐵 ) Fn ( ℤ ↑m 𝑉 ) ) → ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∘f + ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐵 ) ) = ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 + 𝐵 ) ) )
7	5 6	mp3an1	⊢ ( ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) Fn ( ℤ ↑m 𝑉 ) ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐵 ) Fn ( ℤ ↑m 𝑉 ) ) → ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∘f + ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐵 ) ) = ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 + 𝐵 ) ) )
8	2 4 7	syl2an	⊢ ( ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐵 ) ∈ ( mzPoly ‘ 𝑉 ) ) → ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∘f + ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐵 ) ) = ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 + 𝐵 ) ) )
9		mzpadd	⊢ ( ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐵 ) ∈ ( mzPoly ‘ 𝑉 ) ) → ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∘f + ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐵 ) ) ∈ ( mzPoly ‘ 𝑉 ) )
10	8 9	eqeltrrd	⊢ ( ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐴 ) ∈ ( mzPoly ‘ 𝑉 ) ∧ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ 𝐵 ) ∈ ( mzPoly ‘ 𝑉 ) ) → ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝐴 + 𝐵 ) ) ∈ ( mzPoly ‘ 𝑉 ) )