Metamath Proof Explorer

Theorem plymulcl

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

Ref Expression
Assertion plymulcl 
|- ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( F oF x. 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 sseldi 
 |-  ( ( 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 sseldi 
 |-  ( ( 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 3 5 7 9 plymul 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( F oF x. G ) e. ( Poly ` CC ) )