plysub

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

Step	Hyp	Ref	Expression
1		plyadd.1	$⊢ φ \to F \in Poly (S)$
2		plyadd.2	$⊢ φ \to G \in Poly (S)$
3		plyadd.3	$⊢ (φ \land (x \in S \land y \in S)) \to x + y \in S$
4		plymul.4	$⊢ (φ \land (x \in S \land y \in S)) \to x y \in S$
5		plysub.5	$⊢ φ \to - 1 \in S$
6		cnex	$⊢ ℂ \in V$
7		plyf	$⊢ F \in Poly (S) \to F : ℂ ⟶ ℂ$
8	1 7	syl	$⊢ φ \to F : ℂ ⟶ ℂ$
9		plyf	$⊢ G \in Poly (S) \to G : ℂ ⟶ ℂ$
10	2 9	syl	$⊢ φ \to G : ℂ ⟶ ℂ$
11		ofnegsub	$⊢ (ℂ \in V \land F : ℂ ⟶ ℂ \land G : ℂ ⟶ ℂ) \to F +_{f} ((ℂ \times \{- 1\}) \times_{f} G) = F -_{f} G$
12	6 8 10 11	mp3an2i	$⊢ φ \to F +_{f} ((ℂ \times \{- 1\}) \times_{f} G) = F -_{f} G$
13		plybss	$⊢ F \in Poly (S) \to S \subseteq ℂ$
14	1 13	syl	$⊢ φ \to S \subseteq ℂ$
15		plyconst	$⊢ (S \subseteq ℂ \land - 1 \in S) \to ℂ \times \{- 1\} \in Poly (S)$
16	14 5 15	syl2anc	$⊢ φ \to ℂ \times \{- 1\} \in Poly (S)$
17	16 2 3 4	plymul	$⊢ φ \to (ℂ \times \{- 1\}) \times_{f} G \in Poly (S)$
18	1 17 3	plyadd	$⊢ φ \to F +_{f} ((ℂ \times \{- 1\}) \times_{f} G) \in Poly (S)$
19	12 18	eqeltrrd	$⊢ φ \to F -_{f} G \in Poly (S)$

Metamath Proof Explorer