This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )