Metamath Proof Explorer

Theorem ply1remlem

Description: A term of the form x - N is linear, monic, and has exactly one zero. (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.u 
|- U = ( Monic1p ` R )
ply1rem.d 
|- D = ( deg1 ` R )
ply1rem.z 
|- .0. = ( 0g ` R )
Assertion ply1remlem 
|- ( ph -> ( G e. U /\ ( D ` G ) = 1 /\ ( `' ( O ` G ) " { .0. } ) = { N } ) )

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.u 
 |-  U = ( Monic1p ` R )
13 ply1rem.d 
 |-  D = ( deg1 ` R )
14 ply1rem.z 
 |-  .0. = ( 0g ` R )
15 nzrring 
 |-  ( R e. NzRing -> R e. Ring )
16 9 15 syl 
 |-  ( ph -> R e. Ring )
17 1 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
18 16 17 syl 
 |-  ( ph -> P e. Ring )
19 ringgrp 
 |-  ( P e. Ring -> P e. Grp )
20 18 19 syl 
 |-  ( ph -> P e. Grp )
21 4 1 2 vr1cl 
 |-  ( R e. Ring -> X e. B )
22 16 21 syl 
 |-  ( ph -> X e. B )
23 1 6 3 2 ply1sclf 
 |-  ( R e. Ring -> A : K --> B )
24 16 23 syl 
 |-  ( ph -> A : K --> B )
25 24 11 ffvelrnd 
 |-  ( ph -> ( A ` N ) e. B )
26 2 5 grpsubcl 
 |-  ( ( P e. Grp /\ X e. B /\ ( A ` N ) e. B ) -> ( X .- ( A ` N ) ) e. B )
27 20 22 25 26 syl3anc 
 |-  ( ph -> ( X .- ( A ` N ) ) e. B )
28 7 27 eqeltrid 
 |-  ( ph -> G e. B )
29 7 fveq2i 
 |-  ( D ` G ) = ( D ` ( X .- ( A ` N ) ) )
30 13 1 2 deg1xrcl 
 |-  ( ( A ` N ) e. B -> ( D ` ( A ` N ) ) e. RR* )
31 25 30 syl 
 |-  ( ph -> ( D ` ( A ` N ) ) e. RR* )
32 0xr 
 |-  0 e. RR*
33 32 a1i 
 |-  ( ph -> 0 e. RR* )
34 1re 
 |-  1 e. RR
35 rexr 
 |-  ( 1 e. RR -> 1 e. RR* )
36 34 35 mp1i 
 |-  ( ph -> 1 e. RR* )
37 13 1 3 6 deg1sclle 
 |-  ( ( R e. Ring /\ N e. K ) -> ( D ` ( A ` N ) ) <_ 0 )
38 16 11 37 syl2anc 
 |-  ( ph -> ( D ` ( A ` N ) ) <_ 0 )
39 0lt1 
 |-  0 < 1
40 39 a1i 
 |-  ( ph -> 0 < 1 )
41 31 33 36 38 40 xrlelttrd 
 |-  ( ph -> ( D ` ( A ` N ) ) < 1 )
42 eqid 
 |-  ( mulGrp ` P ) = ( mulGrp ` P )
43 42 2 mgpbas 
 |-  B = ( Base ` ( mulGrp ` P ) )
44 eqid 
 |-  ( .g ` ( mulGrp ` P ) ) = ( .g ` ( mulGrp ` P ) )
45 43 44 mulg1 
 |-  ( X e. B -> ( 1 ( .g ` ( mulGrp ` P ) ) X ) = X )
46 22 45 syl 
 |-  ( ph -> ( 1 ( .g ` ( mulGrp ` P ) ) X ) = X )
47 46 fveq2d 
 |-  ( ph -> ( D ` ( 1 ( .g ` ( mulGrp ` P ) ) X ) ) = ( D ` X ) )
48 1nn0 
 |-  1 e. NN0
49 13 1 4 42 44 deg1pw 
 |-  ( ( R e. NzRing /\ 1 e. NN0 ) -> ( D ` ( 1 ( .g ` ( mulGrp ` P ) ) X ) ) = 1 )
50 9 48 49 sylancl 
 |-  ( ph -> ( D ` ( 1 ( .g ` ( mulGrp ` P ) ) X ) ) = 1 )
51 47 50 eqtr3d 
 |-  ( ph -> ( D ` X ) = 1 )
52 41 51 breqtrrd 
 |-  ( ph -> ( D ` ( A ` N ) ) < ( D ` X ) )
53 1 13 16 2 5 22 25 52 deg1sub 
 |-  ( ph -> ( D ` ( X .- ( A ` N ) ) ) = ( D ` X ) )
54 29 53 syl5eq 
 |-  ( ph -> ( D ` G ) = ( D ` X ) )
55 54 51 eqtrd 
 |-  ( ph -> ( D ` G ) = 1 )
56 55 48 eqeltrdi 
 |-  ( ph -> ( D ` G ) e. NN0 )
57 eqid 
 |-  ( 0g ` P ) = ( 0g ` P )
58 13 1 57 2 deg1nn0clb 
 |-  ( ( R e. Ring /\ G e. B ) -> ( G =/= ( 0g ` P ) <-> ( D ` G ) e. NN0 ) )
59 16 28 58 syl2anc 
 |-  ( ph -> ( G =/= ( 0g ` P ) <-> ( D ` G ) e. NN0 ) )
60 56 59 mpbird 
 |-  ( ph -> G =/= ( 0g ` P ) )
61 55 fveq2d 
 |-  ( ph -> ( ( coe1 ` G ) ` ( D ` G ) ) = ( ( coe1 ` G ) ` 1 ) )
62 7 fveq2i 
 |-  ( coe1 ` G ) = ( coe1 ` ( X .- ( A ` N ) ) )
63 62 fveq1i 
 |-  ( ( coe1 ` G ) ` 1 ) = ( ( coe1 ` ( X .- ( A ` N ) ) ) ` 1 )
64 48 a1i 
 |-  ( ph -> 1 e. NN0 )
65 eqid 
 |-  ( -g ` R ) = ( -g ` R )
66 1 2 5 65 coe1subfv 
 |-  ( ( ( R e. Ring /\ X e. B /\ ( A ` N ) e. B ) /\ 1 e. NN0 ) -> ( ( coe1 ` ( X .- ( A ` N ) ) ) ` 1 ) = ( ( ( coe1 ` X ) ` 1 ) ( -g ` R ) ( ( coe1 ` ( A ` N ) ) ` 1 ) ) )
67 16 22 25 64 66 syl31anc 
 |-  ( ph -> ( ( coe1 ` ( X .- ( A ` N ) ) ) ` 1 ) = ( ( ( coe1 ` X ) ` 1 ) ( -g ` R ) ( ( coe1 ` ( A ` N ) ) ` 1 ) ) )
68 63 67 syl5eq 
 |-  ( ph -> ( ( coe1 ` G ) ` 1 ) = ( ( ( coe1 ` X ) ` 1 ) ( -g ` R ) ( ( coe1 ` ( A ` N ) ) ` 1 ) ) )
69 46 oveq2d 
 |-  ( ph -> ( ( 1r ` R ) ( .s ` P ) ( 1 ( .g ` ( mulGrp ` P ) ) X ) ) = ( ( 1r ` R ) ( .s ` P ) X ) )
70 1 ply1sca 
 |-  ( R e. NzRing -> R = ( Scalar ` P ) )
71 9 70 syl 
 |-  ( ph -> R = ( Scalar ` P ) )
72 71 fveq2d 
 |-  ( ph -> ( 1r ` R ) = ( 1r ` ( Scalar ` P ) ) )
73 72 oveq1d 
 |-  ( ph -> ( ( 1r ` R ) ( .s ` P ) X ) = ( ( 1r ` ( Scalar ` P ) ) ( .s ` P ) X ) )
74 1 ply1lmod 
 |-  ( R e. Ring -> P e. LMod )
75 16 74 syl 
 |-  ( ph -> P e. LMod )
76 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
77 eqid 
 |-  ( .s ` P ) = ( .s ` P )
78 eqid 
 |-  ( 1r ` ( Scalar ` P ) ) = ( 1r ` ( Scalar ` P ) )
79 2 76 77 78 lmodvs1 
 |-  ( ( P e. LMod /\ X e. B ) -> ( ( 1r ` ( Scalar ` P ) ) ( .s ` P ) X ) = X )
80 75 22 79 syl2anc 
 |-  ( ph -> ( ( 1r ` ( Scalar ` P ) ) ( .s ` P ) X ) = X )
81 69 73 80 3eqtrd 
 |-  ( ph -> ( ( 1r ` R ) ( .s ` P ) ( 1 ( .g ` ( mulGrp ` P ) ) X ) ) = X )
82 81 fveq2d 
 |-  ( ph -> ( coe1 ` ( ( 1r ` R ) ( .s ` P ) ( 1 ( .g ` ( mulGrp ` P ) ) X ) ) ) = ( coe1 ` X ) )
83 82 fveq1d 
 |-  ( ph -> ( ( coe1 ` ( ( 1r ` R ) ( .s ` P ) ( 1 ( .g ` ( mulGrp ` P ) ) X ) ) ) ` 1 ) = ( ( coe1 ` X ) ` 1 ) )
84 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
85 3 84 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. K )
86 16 85 syl 
 |-  ( ph -> ( 1r ` R ) e. K )
87 14 3 1 4 77 42 44 coe1tmfv1 
 |-  ( ( R e. Ring /\ ( 1r ` R ) e. K /\ 1 e. NN0 ) -> ( ( coe1 ` ( ( 1r ` R ) ( .s ` P ) ( 1 ( .g ` ( mulGrp ` P ) ) X ) ) ) ` 1 ) = ( 1r ` R ) )
88 16 86 64 87 syl3anc 
 |-  ( ph -> ( ( coe1 ` ( ( 1r ` R ) ( .s ` P ) ( 1 ( .g ` ( mulGrp ` P ) ) X ) ) ) ` 1 ) = ( 1r ` R ) )
89 83 88 eqtr3d 
 |-  ( ph -> ( ( coe1 ` X ) ` 1 ) = ( 1r ` R ) )
90 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
91 1 6 3 90 coe1scl 
 |-  ( ( R e. Ring /\ N e. K ) -> ( coe1 ` ( A ` N ) ) = ( x e. NN0 |-> if ( x = 0 , N , ( 0g ` R ) ) ) )
92 16 11 91 syl2anc 
 |-  ( ph -> ( coe1 ` ( A ` N ) ) = ( x e. NN0 |-> if ( x = 0 , N , ( 0g ` R ) ) ) )
93 92 fveq1d 
 |-  ( ph -> ( ( coe1 ` ( A ` N ) ) ` 1 ) = ( ( x e. NN0 |-> if ( x = 0 , N , ( 0g ` R ) ) ) ` 1 ) )
94 ax-1ne0 
 |-  1 =/= 0
95 neeq1 
 |-  ( x = 1 -> ( x =/= 0 <-> 1 =/= 0 ) )
96 94 95 mpbiri 
 |-  ( x = 1 -> x =/= 0 )
97 ifnefalse 
 |-  ( x =/= 0 -> if ( x = 0 , N , ( 0g ` R ) ) = ( 0g ` R ) )
98 96 97 syl 
 |-  ( x = 1 -> if ( x = 0 , N , ( 0g ` R ) ) = ( 0g ` R ) )
99 eqid 
 |-  ( x e. NN0 |-> if ( x = 0 , N , ( 0g ` R ) ) ) = ( x e. NN0 |-> if ( x = 0 , N , ( 0g ` R ) ) )
100 fvex 
 |-  ( 0g ` R ) e. _V
101 98 99 100 fvmpt 
 |-  ( 1 e. NN0 -> ( ( x e. NN0 |-> if ( x = 0 , N , ( 0g ` R ) ) ) ` 1 ) = ( 0g ` R ) )
102 48 101 ax-mp 
 |-  ( ( x e. NN0 |-> if ( x = 0 , N , ( 0g ` R ) ) ) ` 1 ) = ( 0g ` R )
103 93 102 eqtrdi 
 |-  ( ph -> ( ( coe1 ` ( A ` N ) ) ` 1 ) = ( 0g ` R ) )
104 89 103 oveq12d 
 |-  ( ph -> ( ( ( coe1 ` X ) ` 1 ) ( -g ` R ) ( ( coe1 ` ( A ` N ) ) ` 1 ) ) = ( ( 1r ` R ) ( -g ` R ) ( 0g ` R ) ) )
105 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
106 16 105 syl 
 |-  ( ph -> R e. Grp )
107 3 90 65 grpsubid1 
 |-  ( ( R e. Grp /\ ( 1r ` R ) e. K ) -> ( ( 1r ` R ) ( -g ` R ) ( 0g ` R ) ) = ( 1r ` R ) )
108 106 86 107 syl2anc 
 |-  ( ph -> ( ( 1r ` R ) ( -g ` R ) ( 0g ` R ) ) = ( 1r ` R ) )
109 104 108 eqtrd 
 |-  ( ph -> ( ( ( coe1 ` X ) ` 1 ) ( -g ` R ) ( ( coe1 ` ( A ` N ) ) ` 1 ) ) = ( 1r ` R ) )
110 61 68 109 3eqtrd 
 |-  ( ph -> ( ( coe1 ` G ) ` ( D ` G ) ) = ( 1r ` R ) )
111 1 2 57 13 12 84 ismon1p 
 |-  ( G e. U <-> ( G e. B /\ G =/= ( 0g ` P ) /\ ( ( coe1 ` G ) ` ( D ` G ) ) = ( 1r ` R ) ) )
112 28 60 110 111 syl3anbrc 
 |-  ( ph -> G e. U )
113 7 fveq2i 
 |-  ( O ` G ) = ( O ` ( X .- ( A ` N ) ) )
114 113 fveq1i 
 |-  ( ( O ` G ) ` x ) = ( ( O ` ( X .- ( A ` N ) ) ) ` x )
115 10 adantr 
 |-  ( ( ph /\ x e. K ) -> R e. CRing )
116 simpr 
 |-  ( ( ph /\ x e. K ) -> x e. K )
117 8 4 3 1 2 115 116 evl1vard 
 |-  ( ( ph /\ x e. K ) -> ( X e. B /\ ( ( O ` X ) ` x ) = x ) )
118 11 adantr 
 |-  ( ( ph /\ x e. K ) -> N e. K )
119 8 1 3 6 2 115 118 116 evl1scad 
 |-  ( ( ph /\ x e. K ) -> ( ( A ` N ) e. B /\ ( ( O ` ( A ` N ) ) ` x ) = N ) )
120 8 1 3 2 115 116 117 119 5 65 evl1subd 
 |-  ( ( ph /\ x e. K ) -> ( ( X .- ( A ` N ) ) e. B /\ ( ( O ` ( X .- ( A ` N ) ) ) ` x ) = ( x ( -g ` R ) N ) ) )
121 120 simprd 
 |-  ( ( ph /\ x e. K ) -> ( ( O ` ( X .- ( A ` N ) ) ) ` x ) = ( x ( -g ` R ) N ) )
122 114 121 syl5eq 
 |-  ( ( ph /\ x e. K ) -> ( ( O ` G ) ` x ) = ( x ( -g ` R ) N ) )
123 122 eqeq1d 
 |-  ( ( ph /\ x e. K ) -> ( ( ( O ` G ) ` x ) = .0. <-> ( x ( -g ` R ) N ) = .0. ) )
124 106 adantr 
 |-  ( ( ph /\ x e. K ) -> R e. Grp )
125 3 14 65 grpsubeq0 
 |-  ( ( R e. Grp /\ x e. K /\ N e. K ) -> ( ( x ( -g ` R ) N ) = .0. <-> x = N ) )
126 124 116 118 125 syl3anc 
 |-  ( ( ph /\ x e. K ) -> ( ( x ( -g ` R ) N ) = .0. <-> x = N ) )
127 123 126 bitrd 
 |-  ( ( ph /\ x e. K ) -> ( ( ( O ` G ) ` x ) = .0. <-> x = N ) )
128 velsn 
 |-  ( x e. { N } <-> x = N )
129 127 128 bitr4di 
 |-  ( ( ph /\ x e. K ) -> ( ( ( O ` G ) ` x ) = .0. <-> x e. { N } ) )
130 129 pm5.32da 
 |-  ( ph -> ( ( x e. K /\ ( ( O ` G ) ` x ) = .0. ) <-> ( x e. K /\ x e. { N } ) ) )
131 eqid 
 |-  ( R ^s K ) = ( R ^s K )
132 eqid 
 |-  ( Base ` ( R ^s K ) ) = ( Base ` ( R ^s K ) )
133 3 fvexi 
 |-  K e. _V
134 133 a1i 
 |-  ( ph -> K e. _V )
135 8 1 131 3 evl1rhm 
 |-  ( R e. CRing -> O e. ( P RingHom ( R ^s K ) ) )
136 10 135 syl 
 |-  ( ph -> O e. ( P RingHom ( R ^s K ) ) )
137 2 132 rhmf 
 |-  ( O e. ( P RingHom ( R ^s K ) ) -> O : B --> ( Base ` ( R ^s K ) ) )
138 136 137 syl 
 |-  ( ph -> O : B --> ( Base ` ( R ^s K ) ) )
139 138 28 ffvelrnd 
 |-  ( ph -> ( O ` G ) e. ( Base ` ( R ^s K ) ) )
140 131 3 132 9 134 139 pwselbas 
 |-  ( ph -> ( O ` G ) : K --> K )
141 140 ffnd 
 |-  ( ph -> ( O ` G ) Fn K )
142 fniniseg 
 |-  ( ( O ` G ) Fn K -> ( x e. ( `' ( O ` G ) " { .0. } ) <-> ( x e. K /\ ( ( O ` G ) ` x ) = .0. ) ) )
143 141 142 syl 
 |-  ( ph -> ( x e. ( `' ( O ` G ) " { .0. } ) <-> ( x e. K /\ ( ( O ` G ) ` x ) = .0. ) ) )
144 11 snssd 
 |-  ( ph -> { N } C_ K )
145 144 sseld 
 |-  ( ph -> ( x e. { N } -> x e. K ) )
146 145 pm4.71rd 
 |-  ( ph -> ( x e. { N } <-> ( x e. K /\ x e. { N } ) ) )
147 130 143 146 3bitr4d 
 |-  ( ph -> ( x e. ( `' ( O ` G ) " { .0. } ) <-> x e. { N } ) )
148 147 eqrdv 
 |-  ( ph -> ( `' ( O ` G ) " { .0. } ) = { N } )
149 112 55 148 3jca 
 |-  ( ph -> ( G e. U /\ ( D ` G ) = 1 /\ ( `' ( O ` G ) " { .0. } ) = { N } ) )