plysubcl

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

		Ref	Expression
	Assertion	plysubcl	$⊢ (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	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		neg1cn	$⊢ - 1 \in ℂ$
11	10	a1i	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to - 1 \in ℂ$
12	3 5 7 9 11	plysub	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to F -_{f} G \in Poly (ℂ)$

Metamath Proof Explorer