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 ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\right)\to {F}{-}_{f}{G}\in \mathrm{Poly}\left(ℂ\right)$

Proof

Step Hyp Ref Expression
1 plyssc ${⊢}\mathrm{Poly}\left({S}\right)\subseteq \mathrm{Poly}\left(ℂ\right)$
2 simpl ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\right)\to {F}\in \mathrm{Poly}\left({S}\right)$
3 1 2 sseldi ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\right)\to {F}\in \mathrm{Poly}\left(ℂ\right)$
4 simpr ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\right)\to {G}\in \mathrm{Poly}\left({S}\right)$
5 1 4 sseldi ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\right)\to {G}\in \mathrm{Poly}\left(ℂ\right)$
6 addcl ${⊢}\left({x}\in ℂ\wedge {y}\in ℂ\right)\to {x}+{y}\in ℂ$
7 6 adantl ${⊢}\left(\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\right)\wedge \left({x}\in ℂ\wedge {y}\in ℂ\right)\right)\to {x}+{y}\in ℂ$
8 mulcl ${⊢}\left({x}\in ℂ\wedge {y}\in ℂ\right)\to {x}{y}\in ℂ$
9 8 adantl ${⊢}\left(\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\right)\wedge \left({x}\in ℂ\wedge {y}\in ℂ\right)\right)\to {x}{y}\in ℂ$
10 neg1cn ${⊢}-1\in ℂ$
11 10 a1i ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\right)\to -1\in ℂ$
12 3 5 7 9 11 plysub ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {G}\in \mathrm{Poly}\left({S}\right)\right)\to {F}{-}_{f}{G}\in \mathrm{Poly}\left(ℂ\right)$