Theorem plysub

Description: The difference of two polynomials is a polynomial. (Contributed by Mario Carneiro, 21-Jul-2014)

	Ref	Expression
Hypotheses	plyadd.1	⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
	plyadd.2	⊢ ( 𝜑 → 𝐺 ∈ ( Poly ‘ 𝑆 ) )
	plyadd.3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
	plymul.4	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 · 𝑦 ) ∈ 𝑆 )
	plysub.5	⊢ ( 𝜑 → - 1 ∈ 𝑆 )
Assertion	plysub	⊢ ( 𝜑 → ( 𝐹 ∘f − 𝐺 ) ∈ ( Poly ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		plyadd.1	⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
2		plyadd.2	⊢ ( 𝜑 → 𝐺 ∈ ( Poly ‘ 𝑆 ) )
3		plyadd.3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
4		plymul.4	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 · 𝑦 ) ∈ 𝑆 )
5		plysub.5	⊢ ( 𝜑 → - 1 ∈ 𝑆 )
6		cnex	⊢ ℂ ∈ V
7		plyf	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 : ℂ ⟶ ℂ )
8	1 7	syl	⊢ ( 𝜑 → 𝐹 : ℂ ⟶ ℂ )
9		plyf	⊢ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → 𝐺 : ℂ ⟶ ℂ )
10	2 9	syl	⊢ ( 𝜑 → 𝐺 : ℂ ⟶ ℂ )
11		ofnegsub	⊢ ( ( ℂ ∈ V ∧ 𝐹 : ℂ ⟶ ℂ ∧ 𝐺 : ℂ ⟶ ℂ ) → ( 𝐹 ∘f + ( ( ℂ × { - 1 } ) ∘f · 𝐺 ) ) = ( 𝐹 ∘f − 𝐺 ) )
12	6 8 10 11	mp3an2i	⊢ ( 𝜑 → ( 𝐹 ∘f + ( ( ℂ × { - 1 } ) ∘f · 𝐺 ) ) = ( 𝐹 ∘f − 𝐺 ) )
13		plybss	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝑆 ⊆ ℂ )
14	1 13	syl	⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
15		plyconst	⊢ ( ( 𝑆 ⊆ ℂ ∧ - 1 ∈ 𝑆 ) → ( ℂ × { - 1 } ) ∈ ( Poly ‘ 𝑆 ) )
16	14 5 15	syl2anc	⊢ ( 𝜑 → ( ℂ × { - 1 } ) ∈ ( Poly ‘ 𝑆 ) )
17	16 2 3 4	plymul	⊢ ( 𝜑 → ( ( ℂ × { - 1 } ) ∘f · 𝐺 ) ∈ ( Poly ‘ 𝑆 ) )
18	1 17 3	plyadd	⊢ ( 𝜑 → ( 𝐹 ∘f + ( ( ℂ × { - 1 } ) ∘f · 𝐺 ) ) ∈ ( Poly ‘ 𝑆 ) )
19	12 18	eqeltrrd	⊢ ( 𝜑 → ( 𝐹 ∘f − 𝐺 ) ∈ ( Poly ‘ 𝑆 ) )