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 e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( F oF - G ) e. ( Poly ` CC ) )

Proof

Step Hyp Ref Expression
1 plyssc 
 |-  ( Poly ` S ) C_ ( Poly ` CC )
2 simpl 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> F e. ( Poly ` S ) )
3 1 2 sselid 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> F e. ( Poly ` CC ) )
4 simpr 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> G e. ( Poly ` S ) )
5 1 4 sselid 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> G e. ( Poly ` CC ) )
6 addcl 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x + y ) e. CC )
7 6 adantl 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ ( x e. CC /\ y e. CC ) ) -> ( x + y ) e. CC )
8 mulcl 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x x. y ) e. CC )
9 8 adantl 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ ( x e. CC /\ y e. CC ) ) -> ( x x. y ) e. CC )
10 neg1cn 
 |-  -u 1 e. CC
11 10 a1i 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> -u 1 e. CC )
12 3 5 7 9 11 plysub 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( F oF - G ) e. ( Poly ` CC ) )