Metamath Proof Explorer

Theorem plysubcl

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

Ref Expression
Assertion plysubcl ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ S → F − f G ∈ Poly ⁡ ℂ

Proof

Step Hyp Ref Expression
1 plyssc ⊢ Poly ⁡ S ⊆ Poly ⁡ ℂ
2 simpl ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ S → F ∈ Poly ⁡ S
3 1 2 sseldi ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ S → F ∈ Poly ⁡ ℂ
4 simpr ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ S → G ∈ Poly ⁡ S
5 1 4 sseldi ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ S → G ∈ Poly ⁡ ℂ
6 addcl ⊢ x ∈ ℂ ∧ y ∈ ℂ → x + y ∈ ℂ
7 6 adantl ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ S ∧ x ∈ ℂ ∧ y ∈ ℂ → x + y ∈ ℂ
8 mulcl ⊢ x ∈ ℂ ∧ y ∈ ℂ → x ⁢ y ∈ ℂ
9 8 adantl ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ S ∧ x ∈ ℂ ∧ y ∈ ℂ → x ⁢ y ∈ ℂ
10 neg1cn ⊢ − 1 ∈ ℂ
11 10 a1i ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ S → − 1 ∈ ℂ
12 3 5 7 9 11 plysub ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ S → F − f G ∈ Poly ⁡ ℂ