Metamath Proof Explorer

Theorem plyaddcl

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

Ref Expression
Assertion plyaddcl 
|- ( ( 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 3 5 7 plyadd 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( F oF + G ) e. ( Poly ` CC ) )