Metamath Proof Explorer

Theorem facth1

Description: The factor theorem and its converse. A polynomial F has a root at A iff G = x - A is a factor of F . (Contributed by Mario Carneiro, 12-Jun-2015)

Ref Expression
Hypotheses ply1rem.p 
|- P = ( Poly1 ` R )
ply1rem.b 
|- B = ( Base ` P )
ply1rem.k 
|- K = ( Base ` R )
ply1rem.x 
|- X = ( var1 ` R )
ply1rem.m 
|- .- = ( -g ` P )
ply1rem.a 
|- A = ( algSc ` P )
ply1rem.g 
|- G = ( X .- ( A ` N ) )
ply1rem.o 
|- O = ( eval1 ` R )
ply1rem.1 
|- ( ph -> R e. NzRing )
ply1rem.2 
|- ( ph -> R e. CRing )
ply1rem.3 
|- ( ph -> N e. K )
ply1rem.4 
|- ( ph -> F e. B )
facth1.z 
|- .0. = ( 0g ` R )
facth1.d 
|- .|| = ( ||r ` P )
Assertion facth1 
|- ( ph -> ( G .|| F <-> ( ( O ` F ) ` N ) = .0. ) )

Proof

Step Hyp Ref Expression
1 ply1rem.p 
 |-  P = ( Poly1 ` R )
2 ply1rem.b 
 |-  B = ( Base ` P )
3 ply1rem.k 
 |-  K = ( Base ` R )
4 ply1rem.x 
 |-  X = ( var1 ` R )
5 ply1rem.m 
 |-  .- = ( -g ` P )
6 ply1rem.a 
 |-  A = ( algSc ` P )
7 ply1rem.g 
 |-  G = ( X .- ( A ` N ) )
8 ply1rem.o 
 |-  O = ( eval1 ` R )
9 ply1rem.1 
 |-  ( ph -> R e. NzRing )
10 ply1rem.2 
 |-  ( ph -> R e. CRing )
11 ply1rem.3 
 |-  ( ph -> N e. K )
12 ply1rem.4 
 |-  ( ph -> F e. B )
13 facth1.z 
 |-  .0. = ( 0g ` R )
14 facth1.d 
 |-  .|| = ( ||r ` P )
15 nzrring 
 |-  ( R e. NzRing -> R e. Ring )
16 9 15 syl 
 |-  ( ph -> R e. Ring )
17 eqid 
 |-  ( Monic1p ` R ) = ( Monic1p ` R )
18 eqid 
 |-  ( deg1 ` R ) = ( deg1 ` R )
19 1 2 3 4 5 6 7 8 9 10 11 17 18 13 ply1remlem 
 |-  ( ph -> ( G e. ( Monic1p ` R ) /\ ( ( deg1 ` R ) ` G ) = 1 /\ ( `' ( O ` G ) " { .0. } ) = { N } ) )
20 19 simp1d 
 |-  ( ph -> G e. ( Monic1p ` R ) )
21 eqid 
 |-  ( Unic1p ` R ) = ( Unic1p ` R )
22 21 17 mon1puc1p 
 |-  ( ( R e. Ring /\ G e. ( Monic1p ` R ) ) -> G e. ( Unic1p ` R ) )
23 16 20 22 syl2anc 
 |-  ( ph -> G e. ( Unic1p ` R ) )
24 eqid 
 |-  ( 0g ` P ) = ( 0g ` P )
25 eqid 
 |-  ( rem1p ` R ) = ( rem1p ` R )
26 1 14 2 21 24 25 dvdsr1p 
 |-  ( ( R e. Ring /\ F e. B /\ G e. ( Unic1p ` R ) ) -> ( G .|| F <-> ( F ( rem1p ` R ) G ) = ( 0g ` P ) ) )
27 16 12 23 26 syl3anc 
 |-  ( ph -> ( G .|| F <-> ( F ( rem1p ` R ) G ) = ( 0g ` P ) ) )
28 1 2 3 4 5 6 7 8 9 10 11 12 25 ply1rem 
 |-  ( ph -> ( F ( rem1p ` R ) G ) = ( A ` ( ( O ` F ) ` N ) ) )
29 1 6 13 24 ply1scl0 
 |-  ( R e. Ring -> ( A ` .0. ) = ( 0g ` P ) )
30 16 29 syl 
 |-  ( ph -> ( A ` .0. ) = ( 0g ` P ) )
31 30 eqcomd 
 |-  ( ph -> ( 0g ` P ) = ( A ` .0. ) )
32 28 31 eqeq12d 
 |-  ( ph -> ( ( F ( rem1p ` R ) G ) = ( 0g ` P ) <-> ( A ` ( ( O ` F ) ` N ) ) = ( A ` .0. ) ) )
33 1 6 3 2 ply1sclf1 
 |-  ( R e. Ring -> A : K -1-1-> B )
34 16 33 syl 
 |-  ( ph -> A : K -1-1-> B )
35 8 1 3 2 10 11 12 fveval1fvcl 
 |-  ( ph -> ( ( O ` F ) ` N ) e. K )
36 3 13 ring0cl 
 |-  ( R e. Ring -> .0. e. K )
37 16 36 syl 
 |-  ( ph -> .0. e. K )
38 f1fveq 
 |-  ( ( A : K -1-1-> B /\ ( ( ( O ` F ) ` N ) e. K /\ .0. e. K ) ) -> ( ( A ` ( ( O ` F ) ` N ) ) = ( A ` .0. ) <-> ( ( O ` F ) ` N ) = .0. ) )
39 34 35 37 38 syl12anc 
 |-  ( ph -> ( ( A ` ( ( O ` F ) ` N ) ) = ( A ` .0. ) <-> ( ( O ` F ) ` N ) = .0. ) )
40 27 32 39 3bitrd 
 |-  ( ph -> ( G .|| F <-> ( ( O ` F ) ` N ) = .0. ) )