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