plyaddcl

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

		Ref	Expression
	Assertion	plyaddcl	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to F +_{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	sseldi	$⊢ (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	sseldi	$⊢ (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	3 5 7	plyadd	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to F +_{f} G \in Poly (ℂ)$

Metamath Proof Explorer