plymulcl

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

		Ref	Expression
	Assertion	plymulcl	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to F \times_{f} G \in Poly (ℂ)$

Step	Hyp	Ref	Expression
1		plyssc	$⊢ Poly (S) \subseteq Poly (ℂ)$
2		simpl	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to F \in Poly (S)$
3	1 2	sselid	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to F \in Poly (ℂ)$
4		simpr	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to G \in Poly (S)$
5	1 4	sselid	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to G \in Poly (ℂ)$
6		addcl	$⊢ (x \in ℂ \land y \in ℂ) \to x + y \in ℂ$
7	6	adantl	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land (x \in ℂ \land y \in ℂ)) \to x + y \in ℂ$
8		mulcl	$⊢ (x \in ℂ \land y \in ℂ) \to x y \in ℂ$
9	8	adantl	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land (x \in ℂ \land y \in ℂ)) \to x y \in ℂ$
10	3 5 7 9	plymul	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to F \times_{f} G \in Poly (ℂ)$

Metamath Proof Explorer