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