Theorem plysub

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

	Ref	Expression
Hypotheses	plyadd.1	|- ( ph -> F e. ( Poly ` S ) )
	plyadd.2	|- ( ph -> G e. ( Poly ` S ) )
	plyadd.3	|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x + y ) e. S )
	plymul.4	|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x x. y ) e. S )
	plysub.5	|- ( ph -> -u 1 e. S )
Assertion	plysub	|- ( ph -> ( F oF - G ) e. ( Poly ` S ) )

Proof

Step	Hyp	Ref	Expression
1		plyadd.1	|- ( ph -> F e. ( Poly ` S ) )
2		plyadd.2	|- ( ph -> G e. ( Poly ` S ) )
3		plyadd.3	|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x + y ) e. S )
4		plymul.4	|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x x. y ) e. S )
5		plysub.5	|- ( ph -> -u 1 e. S )
6		cnex	|- CC e. _V
7		plyf	|- ( F e. ( Poly ` S ) -> F : CC --> CC )
8	1 7	syl	|- ( ph -> F : CC --> CC )
9		plyf	|- ( G e. ( Poly ` S ) -> G : CC --> CC )
10	2 9	syl	|- ( ph -> G : CC --> CC )
11		ofnegsub	|- ( ( CC e. _V /\ F : CC --> CC /\ G : CC --> CC ) -> ( F oF + ( ( CC X. { -u 1 } ) oF x. G ) ) = ( F oF - G ) )
12	6 8 10 11	mp3an2i	|- ( ph -> ( F oF + ( ( CC X. { -u 1 } ) oF x. G ) ) = ( F oF - G ) )
13		plybss	|- ( F e. ( Poly ` S ) -> S C_ CC )
14	1 13	syl	|- ( ph -> S C_ CC )
15		plyconst	|- ( ( S C_ CC /\ -u 1 e. S ) -> ( CC X. { -u 1 } ) e. ( Poly ` S ) )
16	14 5 15	syl2anc	|- ( ph -> ( CC X. { -u 1 } ) e. ( Poly ` S ) )
17	16 2 3 4	plymul	|- ( ph -> ( ( CC X. { -u 1 } ) oF x. G ) e. ( Poly ` S ) )
18	1 17 3	plyadd	|- ( ph -> ( F oF + ( ( CC X. { -u 1 } ) oF x. G ) ) e. ( Poly ` S ) )
19	12 18	eqeltrrd	|- ( ph -> ( F oF - G ) e. ( Poly ` S ) )