Metamath Proof Explorer

Theorem facth

Description: The factor theorem. If a polynomial F has a root at A , then G = x - A is a factor of F (and the other factor is F quot G ). This is part of Metamath 100 proof #89. (Contributed by Mario Carneiro, 26-Jul-2014)

Ref Expression
Hypothesis facth.1 
|- G = ( Xp oF - ( CC X. { A } ) )
Assertion facth 
|- ( ( F e. ( Poly ` S ) /\ A e. CC /\ ( F ` A ) = 0 ) -> F = ( G oF x. ( F quot G ) ) )

Proof

Step Hyp Ref Expression
1 facth.1 
 |-  G = ( Xp oF - ( CC X. { A } ) )
2 eqid 
 |-  ( F oF - ( G oF x. ( F quot G ) ) ) = ( F oF - ( G oF x. ( F quot G ) ) )
3 1 2 plyrem 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC ) -> ( F oF - ( G oF x. ( F quot G ) ) ) = ( CC X. { ( F ` A ) } ) )
4 3 3adant3 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC /\ ( F ` A ) = 0 ) -> ( F oF - ( G oF x. ( F quot G ) ) ) = ( CC X. { ( F ` A ) } ) )
5 simp3 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC /\ ( F ` A ) = 0 ) -> ( F ` A ) = 0 )
6 5 sneqd 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC /\ ( F ` A ) = 0 ) -> { ( F ` A ) } = { 0 } )
7 6 xpeq2d 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC /\ ( F ` A ) = 0 ) -> ( CC X. { ( F ` A ) } ) = ( CC X. { 0 } ) )
8 4 7 eqtrd 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC /\ ( F ` A ) = 0 ) -> ( F oF - ( G oF x. ( F quot G ) ) ) = ( CC X. { 0 } ) )
9 cnex 
 |-  CC e. _V
10 9 a1i 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC /\ ( F ` A ) = 0 ) -> CC e. _V )
11 simp1 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC /\ ( F ` A ) = 0 ) -> F e. ( Poly ` S ) )
12 plyf 
 |-  ( F e. ( Poly ` S ) -> F : CC --> CC )
13 11 12 syl 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC /\ ( F ` A ) = 0 ) -> F : CC --> CC )
14 1 plyremlem 
 |-  ( A e. CC -> ( G e. ( Poly ` CC ) /\ ( deg ` G ) = 1 /\ ( `' G " { 0 } ) = { A } ) )
15 14 3ad2ant2 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC /\ ( F ` A ) = 0 ) -> ( G e. ( Poly ` CC ) /\ ( deg ` G ) = 1 /\ ( `' G " { 0 } ) = { A } ) )
16 15 simp1d 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC /\ ( F ` A ) = 0 ) -> G e. ( Poly ` CC ) )
17 plyssc 
 |-  ( Poly ` S ) C_ ( Poly ` CC )
18 17 11 sselid 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC /\ ( F ` A ) = 0 ) -> F e. ( Poly ` CC ) )
19 15 simp2d 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC /\ ( F ` A ) = 0 ) -> ( deg ` G ) = 1 )
20 ax-1ne0 
 |-  1 =/= 0
21 20 a1i 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC /\ ( F ` A ) = 0 ) -> 1 =/= 0 )
22 19 21 eqnetrd 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC /\ ( F ` A ) = 0 ) -> ( deg ` G ) =/= 0 )
23 fveq2 
 |-  ( G = 0p -> ( deg ` G ) = ( deg ` 0p ) )
24 dgr0 
 |-  ( deg ` 0p ) = 0
25 23 24 eqtrdi 
 |-  ( G = 0p -> ( deg ` G ) = 0 )
26 25 necon3i 
 |-  ( ( deg ` G ) =/= 0 -> G =/= 0p )
27 22 26 syl 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC /\ ( F ` A ) = 0 ) -> G =/= 0p )
28 quotcl2 
 |-  ( ( F e. ( Poly ` CC ) /\ G e. ( Poly ` CC ) /\ G =/= 0p ) -> ( F quot G ) e. ( Poly ` CC ) )
29 18 16 27 28 syl3anc 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC /\ ( F ` A ) = 0 ) -> ( F quot G ) e. ( Poly ` CC ) )
30 plymulcl 
 |-  ( ( G e. ( Poly ` CC ) /\ ( F quot G ) e. ( Poly ` CC ) ) -> ( G oF x. ( F quot G ) ) e. ( Poly ` CC ) )
31 16 29 30 syl2anc 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC /\ ( F ` A ) = 0 ) -> ( G oF x. ( F quot G ) ) e. ( Poly ` CC ) )
32 plyf 
 |-  ( ( G oF x. ( F quot G ) ) e. ( Poly ` CC ) -> ( G oF x. ( F quot G ) ) : CC --> CC )
33 31 32 syl 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC /\ ( F ` A ) = 0 ) -> ( G oF x. ( F quot G ) ) : CC --> CC )
34 ofsubeq0 
 |-  ( ( CC e. _V /\ F : CC --> CC /\ ( G oF x. ( F quot G ) ) : CC --> CC ) -> ( ( F oF - ( G oF x. ( F quot G ) ) ) = ( CC X. { 0 } ) <-> F = ( G oF x. ( F quot G ) ) ) )
35 10 13 33 34 syl3anc 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC /\ ( F ` A ) = 0 ) -> ( ( F oF - ( G oF x. ( F quot G ) ) ) = ( CC X. { 0 } ) <-> F = ( G oF x. ( F quot G ) ) ) )
36 8 35 mpbid 
 |-  ( ( F e. ( Poly ` S ) /\ A e. CC /\ ( F ` A ) = 0 ) -> F = ( G oF x. ( F quot G ) ) )