Metamath Proof Explorer


Theorem plyremlem

Description: Closure of a linear factor. (Contributed by Mario Carneiro, 26-Jul-2014)

Ref Expression
Hypothesis plyrem.1
|- G = ( Xp oF - ( CC X. { A } ) )
Assertion plyremlem
|- ( A e. CC -> ( G e. ( Poly ` CC ) /\ ( deg ` G ) = 1 /\ ( `' G " { 0 } ) = { A } ) )

Proof

Step Hyp Ref Expression
1 plyrem.1
 |-  G = ( Xp oF - ( CC X. { A } ) )
2 ssid
 |-  CC C_ CC
3 ax-1cn
 |-  1 e. CC
4 plyid
 |-  ( ( CC C_ CC /\ 1 e. CC ) -> Xp e. ( Poly ` CC ) )
5 2 3 4 mp2an
 |-  Xp e. ( Poly ` CC )
6 plyconst
 |-  ( ( CC C_ CC /\ A e. CC ) -> ( CC X. { A } ) e. ( Poly ` CC ) )
7 2 6 mpan
 |-  ( A e. CC -> ( CC X. { A } ) e. ( Poly ` CC ) )
8 plysubcl
 |-  ( ( Xp e. ( Poly ` CC ) /\ ( CC X. { A } ) e. ( Poly ` CC ) ) -> ( Xp oF - ( CC X. { A } ) ) e. ( Poly ` CC ) )
9 5 7 8 sylancr
 |-  ( A e. CC -> ( Xp oF - ( CC X. { A } ) ) e. ( Poly ` CC ) )
10 1 9 eqeltrid
 |-  ( A e. CC -> G e. ( Poly ` CC ) )
11 negcl
 |-  ( A e. CC -> -u A e. CC )
12 addcom
 |-  ( ( -u A e. CC /\ z e. CC ) -> ( -u A + z ) = ( z + -u A ) )
13 11 12 sylan
 |-  ( ( A e. CC /\ z e. CC ) -> ( -u A + z ) = ( z + -u A ) )
14 negsub
 |-  ( ( z e. CC /\ A e. CC ) -> ( z + -u A ) = ( z - A ) )
15 14 ancoms
 |-  ( ( A e. CC /\ z e. CC ) -> ( z + -u A ) = ( z - A ) )
16 13 15 eqtrd
 |-  ( ( A e. CC /\ z e. CC ) -> ( -u A + z ) = ( z - A ) )
17 16 mpteq2dva
 |-  ( A e. CC -> ( z e. CC |-> ( -u A + z ) ) = ( z e. CC |-> ( z - A ) ) )
18 cnex
 |-  CC e. _V
19 18 a1i
 |-  ( A e. CC -> CC e. _V )
20 negex
 |-  -u A e. _V
21 20 a1i
 |-  ( ( A e. CC /\ z e. CC ) -> -u A e. _V )
22 simpr
 |-  ( ( A e. CC /\ z e. CC ) -> z e. CC )
23 fconstmpt
 |-  ( CC X. { -u A } ) = ( z e. CC |-> -u A )
24 23 a1i
 |-  ( A e. CC -> ( CC X. { -u A } ) = ( z e. CC |-> -u A ) )
25 df-idp
 |-  Xp = ( _I |` CC )
26 mptresid
 |-  ( _I |` CC ) = ( z e. CC |-> z )
27 25 26 eqtri
 |-  Xp = ( z e. CC |-> z )
28 27 a1i
 |-  ( A e. CC -> Xp = ( z e. CC |-> z ) )
29 19 21 22 24 28 offval2
 |-  ( A e. CC -> ( ( CC X. { -u A } ) oF + Xp ) = ( z e. CC |-> ( -u A + z ) ) )
30 simpl
 |-  ( ( A e. CC /\ z e. CC ) -> A e. CC )
31 fconstmpt
 |-  ( CC X. { A } ) = ( z e. CC |-> A )
32 31 a1i
 |-  ( A e. CC -> ( CC X. { A } ) = ( z e. CC |-> A ) )
33 19 22 30 28 32 offval2
 |-  ( A e. CC -> ( Xp oF - ( CC X. { A } ) ) = ( z e. CC |-> ( z - A ) ) )
34 17 29 33 3eqtr4d
 |-  ( A e. CC -> ( ( CC X. { -u A } ) oF + Xp ) = ( Xp oF - ( CC X. { A } ) ) )
35 34 1 eqtr4di
 |-  ( A e. CC -> ( ( CC X. { -u A } ) oF + Xp ) = G )
36 35 fveq2d
 |-  ( A e. CC -> ( deg ` ( ( CC X. { -u A } ) oF + Xp ) ) = ( deg ` G ) )
37 plyconst
 |-  ( ( CC C_ CC /\ -u A e. CC ) -> ( CC X. { -u A } ) e. ( Poly ` CC ) )
38 2 11 37 sylancr
 |-  ( A e. CC -> ( CC X. { -u A } ) e. ( Poly ` CC ) )
39 5 a1i
 |-  ( A e. CC -> Xp e. ( Poly ` CC ) )
40 0dgr
 |-  ( -u A e. CC -> ( deg ` ( CC X. { -u A } ) ) = 0 )
41 11 40 syl
 |-  ( A e. CC -> ( deg ` ( CC X. { -u A } ) ) = 0 )
42 0lt1
 |-  0 < 1
43 41 42 eqbrtrdi
 |-  ( A e. CC -> ( deg ` ( CC X. { -u A } ) ) < 1 )
44 eqid
 |-  ( deg ` ( CC X. { -u A } ) ) = ( deg ` ( CC X. { -u A } ) )
45 dgrid
 |-  ( deg ` Xp ) = 1
46 45 eqcomi
 |-  1 = ( deg ` Xp )
47 44 46 dgradd2
 |-  ( ( ( CC X. { -u A } ) e. ( Poly ` CC ) /\ Xp e. ( Poly ` CC ) /\ ( deg ` ( CC X. { -u A } ) ) < 1 ) -> ( deg ` ( ( CC X. { -u A } ) oF + Xp ) ) = 1 )
48 38 39 43 47 syl3anc
 |-  ( A e. CC -> ( deg ` ( ( CC X. { -u A } ) oF + Xp ) ) = 1 )
49 36 48 eqtr3d
 |-  ( A e. CC -> ( deg ` G ) = 1 )
50 1 33 syl5eq
 |-  ( A e. CC -> G = ( z e. CC |-> ( z - A ) ) )
51 50 fveq1d
 |-  ( A e. CC -> ( G ` z ) = ( ( z e. CC |-> ( z - A ) ) ` z ) )
52 51 adantr
 |-  ( ( A e. CC /\ z e. CC ) -> ( G ` z ) = ( ( z e. CC |-> ( z - A ) ) ` z ) )
53 ovex
 |-  ( z - A ) e. _V
54 eqid
 |-  ( z e. CC |-> ( z - A ) ) = ( z e. CC |-> ( z - A ) )
55 54 fvmpt2
 |-  ( ( z e. CC /\ ( z - A ) e. _V ) -> ( ( z e. CC |-> ( z - A ) ) ` z ) = ( z - A ) )
56 22 53 55 sylancl
 |-  ( ( A e. CC /\ z e. CC ) -> ( ( z e. CC |-> ( z - A ) ) ` z ) = ( z - A ) )
57 52 56 eqtrd
 |-  ( ( A e. CC /\ z e. CC ) -> ( G ` z ) = ( z - A ) )
58 57 eqeq1d
 |-  ( ( A e. CC /\ z e. CC ) -> ( ( G ` z ) = 0 <-> ( z - A ) = 0 ) )
59 subeq0
 |-  ( ( z e. CC /\ A e. CC ) -> ( ( z - A ) = 0 <-> z = A ) )
60 59 ancoms
 |-  ( ( A e. CC /\ z e. CC ) -> ( ( z - A ) = 0 <-> z = A ) )
61 58 60 bitrd
 |-  ( ( A e. CC /\ z e. CC ) -> ( ( G ` z ) = 0 <-> z = A ) )
62 61 pm5.32da
 |-  ( A e. CC -> ( ( z e. CC /\ ( G ` z ) = 0 ) <-> ( z e. CC /\ z = A ) ) )
63 plyf
 |-  ( G e. ( Poly ` CC ) -> G : CC --> CC )
64 ffn
 |-  ( G : CC --> CC -> G Fn CC )
65 fniniseg
 |-  ( G Fn CC -> ( z e. ( `' G " { 0 } ) <-> ( z e. CC /\ ( G ` z ) = 0 ) ) )
66 10 63 64 65 4syl
 |-  ( A e. CC -> ( z e. ( `' G " { 0 } ) <-> ( z e. CC /\ ( G ` z ) = 0 ) ) )
67 eleq1a
 |-  ( A e. CC -> ( z = A -> z e. CC ) )
68 67 pm4.71rd
 |-  ( A e. CC -> ( z = A <-> ( z e. CC /\ z = A ) ) )
69 62 66 68 3bitr4d
 |-  ( A e. CC -> ( z e. ( `' G " { 0 } ) <-> z = A ) )
70 velsn
 |-  ( z e. { A } <-> z = A )
71 69 70 bitr4di
 |-  ( A e. CC -> ( z e. ( `' G " { 0 } ) <-> z e. { A } ) )
72 71 eqrdv
 |-  ( A e. CC -> ( `' G " { 0 } ) = { A } )
73 10 49 72 3jca
 |-  ( A e. CC -> ( G e. ( Poly ` CC ) /\ ( deg ` G ) = 1 /\ ( `' G " { 0 } ) = { A } ) )