Metamath Proof Explorer

Theorem fta1blem

Description: Lemma for fta1b . (Contributed by Mario Carneiro, 14-Jun-2015)

Ref Expression
Hypotheses fta1b.p 
|- P = ( Poly1 ` R )
fta1b.b 
|- B = ( Base ` P )
fta1b.d 
|- D = ( deg1 ` R )
fta1b.o 
|- O = ( eval1 ` R )
fta1b.w 
|- W = ( 0g ` R )
fta1b.z 
|- .0. = ( 0g ` P )
fta1blem.k 
|- K = ( Base ` R )
fta1blem.t 
|- .X. = ( .r ` R )
fta1blem.x 
|- X = ( var1 ` R )
fta1blem.s 
|- .x. = ( .s ` P )
fta1blem.1 
|- ( ph -> R e. CRing )
fta1blem.2 
|- ( ph -> M e. K )
fta1blem.3 
|- ( ph -> N e. K )
fta1blem.4 
|- ( ph -> ( M .X. N ) = W )
fta1blem.5 
|- ( ph -> M =/= W )
fta1blem.6 
|- ( ph -> ( ( M .x. X ) e. ( B \ { .0. } ) -> ( # ` ( `' ( O ` ( M .x. X ) ) " { W } ) ) <_ ( D ` ( M .x. X ) ) ) )
Assertion fta1blem 
|- ( ph -> N = W )

Proof

Step Hyp Ref Expression
1 fta1b.p 
 |-  P = ( Poly1 ` R )
2 fta1b.b 
 |-  B = ( Base ` P )
3 fta1b.d 
 |-  D = ( deg1 ` R )
4 fta1b.o 
 |-  O = ( eval1 ` R )
5 fta1b.w 
 |-  W = ( 0g ` R )
6 fta1b.z 
 |-  .0. = ( 0g ` P )
7 fta1blem.k 
 |-  K = ( Base ` R )
8 fta1blem.t 
 |-  .X. = ( .r ` R )
9 fta1blem.x 
 |-  X = ( var1 ` R )
10 fta1blem.s 
 |-  .x. = ( .s ` P )
11 fta1blem.1 
 |-  ( ph -> R e. CRing )
12 fta1blem.2 
 |-  ( ph -> M e. K )
13 fta1blem.3 
 |-  ( ph -> N e. K )
14 fta1blem.4 
 |-  ( ph -> ( M .X. N ) = W )
15 fta1blem.5 
 |-  ( ph -> M =/= W )
16 fta1blem.6 
 |-  ( ph -> ( ( M .x. X ) e. ( B \ { .0. } ) -> ( # ` ( `' ( O ` ( M .x. X ) ) " { W } ) ) <_ ( D ` ( M .x. X ) ) ) )
17 4 9 7 1 2 11 13 evl1vard 
 |-  ( ph -> ( X e. B /\ ( ( O ` X ) ` N ) = N ) )
18 4 1 7 2 11 13 17 12 10 8 evl1vsd 
 |-  ( ph -> ( ( M .x. X ) e. B /\ ( ( O ` ( M .x. X ) ) ` N ) = ( M .X. N ) ) )
19 18 simprd 
 |-  ( ph -> ( ( O ` ( M .x. X ) ) ` N ) = ( M .X. N ) )
20 19 14 eqtrd 
 |-  ( ph -> ( ( O ` ( M .x. X ) ) ` N ) = W )
21 eqid 
 |-  ( R ^s K ) = ( R ^s K )
22 eqid 
 |-  ( Base ` ( R ^s K ) ) = ( Base ` ( R ^s K ) )
23 7 fvexi 
 |-  K e. _V
24 23 a1i 
 |-  ( ph -> K e. _V )
25 4 1 21 7 evl1rhm 
 |-  ( R e. CRing -> O e. ( P RingHom ( R ^s K ) ) )
26 11 25 syl 
 |-  ( ph -> O e. ( P RingHom ( R ^s K ) ) )
27 2 22 rhmf 
 |-  ( O e. ( P RingHom ( R ^s K ) ) -> O : B --> ( Base ` ( R ^s K ) ) )
28 26 27 syl 
 |-  ( ph -> O : B --> ( Base ` ( R ^s K ) ) )
29 18 simpld 
 |-  ( ph -> ( M .x. X ) e. B )
30 28 29 ffvelrnd 
 |-  ( ph -> ( O ` ( M .x. X ) ) e. ( Base ` ( R ^s K ) ) )
31 21 7 22 11 24 30 pwselbas 
 |-  ( ph -> ( O ` ( M .x. X ) ) : K --> K )
32 31 ffnd 
 |-  ( ph -> ( O ` ( M .x. X ) ) Fn K )
33 fniniseg 
 |-  ( ( O ` ( M .x. X ) ) Fn K -> ( N e. ( `' ( O ` ( M .x. X ) ) " { W } ) <-> ( N e. K /\ ( ( O ` ( M .x. X ) ) ` N ) = W ) ) )
34 32 33 syl 
 |-  ( ph -> ( N e. ( `' ( O ` ( M .x. X ) ) " { W } ) <-> ( N e. K /\ ( ( O ` ( M .x. X ) ) ` N ) = W ) ) )
35 13 20 34 mpbir2and 
 |-  ( ph -> N e. ( `' ( O ` ( M .x. X ) ) " { W } ) )
36 fvex 
 |-  ( O ` ( M .x. X ) ) e. _V
37 36 cnvex 
 |-  `' ( O ` ( M .x. X ) ) e. _V
38 37 imaex 
 |-  ( `' ( O ` ( M .x. X ) ) " { W } ) e. _V
39 38 a1i 
 |-  ( ph -> ( `' ( O ` ( M .x. X ) ) " { W } ) e. _V )
40 1nn0 
 |-  1 e. NN0
41 40 a1i 
 |-  ( ph -> 1 e. NN0 )
42 crngring 
 |-  ( R e. CRing -> R e. Ring )
43 11 42 syl 
 |-  ( ph -> R e. Ring )
44 9 1 2 vr1cl 
 |-  ( R e. Ring -> X e. B )
45 43 44 syl 
 |-  ( ph -> X e. B )
46 eqid 
 |-  ( mulGrp ` P ) = ( mulGrp ` P )
47 46 2 mgpbas 
 |-  B = ( Base ` ( mulGrp ` P ) )
48 eqid 
 |-  ( .g ` ( mulGrp ` P ) ) = ( .g ` ( mulGrp ` P ) )
49 47 48 mulg1 
 |-  ( X e. B -> ( 1 ( .g ` ( mulGrp ` P ) ) X ) = X )
50 45 49 syl 
 |-  ( ph -> ( 1 ( .g ` ( mulGrp ` P ) ) X ) = X )
51 50 oveq2d 
 |-  ( ph -> ( M .x. ( 1 ( .g ` ( mulGrp ` P ) ) X ) ) = ( M .x. X ) )
52 5 7 1 9 10 46 48 coe1tmfv1 
 |-  ( ( R e. Ring /\ M e. K /\ 1 e. NN0 ) -> ( ( coe1 ` ( M .x. ( 1 ( .g ` ( mulGrp ` P ) ) X ) ) ) ` 1 ) = M )
53 43 12 41 52 syl3anc 
 |-  ( ph -> ( ( coe1 ` ( M .x. ( 1 ( .g ` ( mulGrp ` P ) ) X ) ) ) ` 1 ) = M )
54 1 6 5 coe1z 
 |-  ( R e. Ring -> ( coe1 ` .0. ) = ( NN0 X. { W } ) )
55 43 54 syl 
 |-  ( ph -> ( coe1 ` .0. ) = ( NN0 X. { W } ) )
56 55 fveq1d 
 |-  ( ph -> ( ( coe1 ` .0. ) ` 1 ) = ( ( NN0 X. { W } ) ` 1 ) )
57 5 fvexi 
 |-  W e. _V
58 57 fvconst2 
 |-  ( 1 e. NN0 -> ( ( NN0 X. { W } ) ` 1 ) = W )
59 40 58 ax-mp 
 |-  ( ( NN0 X. { W } ) ` 1 ) = W
60 56 59 eqtrdi 
 |-  ( ph -> ( ( coe1 ` .0. ) ` 1 ) = W )
61 15 53 60 3netr4d 
 |-  ( ph -> ( ( coe1 ` ( M .x. ( 1 ( .g ` ( mulGrp ` P ) ) X ) ) ) ` 1 ) =/= ( ( coe1 ` .0. ) ` 1 ) )
62 fveq2 
 |-  ( ( M .x. ( 1 ( .g ` ( mulGrp ` P ) ) X ) ) = .0. -> ( coe1 ` ( M .x. ( 1 ( .g ` ( mulGrp ` P ) ) X ) ) ) = ( coe1 ` .0. ) )
63 62 fveq1d 
 |-  ( ( M .x. ( 1 ( .g ` ( mulGrp ` P ) ) X ) ) = .0. -> ( ( coe1 ` ( M .x. ( 1 ( .g ` ( mulGrp ` P ) ) X ) ) ) ` 1 ) = ( ( coe1 ` .0. ) ` 1 ) )
64 63 necon3i 
 |-  ( ( ( coe1 ` ( M .x. ( 1 ( .g ` ( mulGrp ` P ) ) X ) ) ) ` 1 ) =/= ( ( coe1 ` .0. ) ` 1 ) -> ( M .x. ( 1 ( .g ` ( mulGrp ` P ) ) X ) ) =/= .0. )
65 61 64 syl 
 |-  ( ph -> ( M .x. ( 1 ( .g ` ( mulGrp ` P ) ) X ) ) =/= .0. )
66 51 65 eqnetrrd 
 |-  ( ph -> ( M .x. X ) =/= .0. )
67 eldifsn 
 |-  ( ( M .x. X ) e. ( B \ { .0. } ) <-> ( ( M .x. X ) e. B /\ ( M .x. X ) =/= .0. ) )
68 29 66 67 sylanbrc 
 |-  ( ph -> ( M .x. X ) e. ( B \ { .0. } ) )
69 68 16 mpd 
 |-  ( ph -> ( # ` ( `' ( O ` ( M .x. X ) ) " { W } ) ) <_ ( D ` ( M .x. X ) ) )
70 51 fveq2d 
 |-  ( ph -> ( D ` ( M .x. ( 1 ( .g ` ( mulGrp ` P ) ) X ) ) ) = ( D ` ( M .x. X ) ) )
71 3 7 1 9 10 46 48 5 deg1tm 
 |-  ( ( R e. Ring /\ ( M e. K /\ M =/= W ) /\ 1 e. NN0 ) -> ( D ` ( M .x. ( 1 ( .g ` ( mulGrp ` P ) ) X ) ) ) = 1 )
72 43 12 15 41 71 syl121anc 
 |-  ( ph -> ( D ` ( M .x. ( 1 ( .g ` ( mulGrp ` P ) ) X ) ) ) = 1 )
73 70 72 eqtr3d 
 |-  ( ph -> ( D ` ( M .x. X ) ) = 1 )
74 69 73 breqtrd 
 |-  ( ph -> ( # ` ( `' ( O ` ( M .x. X ) ) " { W } ) ) <_ 1 )
75 hashbnd 
 |-  ( ( ( `' ( O ` ( M .x. X ) ) " { W } ) e. _V /\ 1 e. NN0 /\ ( # ` ( `' ( O ` ( M .x. X ) ) " { W } ) ) <_ 1 ) -> ( `' ( O ` ( M .x. X ) ) " { W } ) e. Fin )
76 39 41 74 75 syl3anc 
 |-  ( ph -> ( `' ( O ` ( M .x. X ) ) " { W } ) e. Fin )
77 7 5 ring0cl 
 |-  ( R e. Ring -> W e. K )
78 43 77 syl 
 |-  ( ph -> W e. K )
79 eqid 
 |-  ( algSc ` P ) = ( algSc ` P )
80 1 79 7 2 ply1sclf 
 |-  ( R e. Ring -> ( algSc ` P ) : K --> B )
81 43 80 syl 
 |-  ( ph -> ( algSc ` P ) : K --> B )
82 81 12 ffvelrnd 
 |-  ( ph -> ( ( algSc ` P ) ` M ) e. B )
83 eqid 
 |-  ( .r ` P ) = ( .r ` P )
84 eqid 
 |-  ( .r ` ( R ^s K ) ) = ( .r ` ( R ^s K ) )
85 2 83 84 rhmmul 
 |-  ( ( O e. ( P RingHom ( R ^s K ) ) /\ ( ( algSc ` P ) ` M ) e. B /\ X e. B ) -> ( O ` ( ( ( algSc ` P ) ` M ) ( .r ` P ) X ) ) = ( ( O ` ( ( algSc ` P ) ` M ) ) ( .r ` ( R ^s K ) ) ( O ` X ) ) )
86 26 82 45 85 syl3anc 
 |-  ( ph -> ( O ` ( ( ( algSc ` P ) ` M ) ( .r ` P ) X ) ) = ( ( O ` ( ( algSc ` P ) ` M ) ) ( .r ` ( R ^s K ) ) ( O ` X ) ) )
87 1 ply1assa 
 |-  ( R e. CRing -> P e. AssAlg )
88 11 87 syl 
 |-  ( ph -> P e. AssAlg )
89 1 ply1sca 
 |-  ( R e. CRing -> R = ( Scalar ` P ) )
90 11 89 syl 
 |-  ( ph -> R = ( Scalar ` P ) )
91 90 fveq2d 
 |-  ( ph -> ( Base ` R ) = ( Base ` ( Scalar ` P ) ) )
92 7 91 eqtrid 
 |-  ( ph -> K = ( Base ` ( Scalar ` P ) ) )
93 12 92 eleqtrd 
 |-  ( ph -> M e. ( Base ` ( Scalar ` P ) ) )
94 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
95 eqid 
 |-  ( Base ` ( Scalar ` P ) ) = ( Base ` ( Scalar ` P ) )
96 79 94 95 2 83 10 asclmul1 
 |-  ( ( P e. AssAlg /\ M e. ( Base ` ( Scalar ` P ) ) /\ X e. B ) -> ( ( ( algSc ` P ) ` M ) ( .r ` P ) X ) = ( M .x. X ) )
97 88 93 45 96 syl3anc 
 |-  ( ph -> ( ( ( algSc ` P ) ` M ) ( .r ` P ) X ) = ( M .x. X ) )
98 97 fveq2d 
 |-  ( ph -> ( O ` ( ( ( algSc ` P ) ` M ) ( .r ` P ) X ) ) = ( O ` ( M .x. X ) ) )
99 28 82 ffvelrnd 
 |-  ( ph -> ( O ` ( ( algSc ` P ) ` M ) ) e. ( Base ` ( R ^s K ) ) )
100 28 45 ffvelrnd 
 |-  ( ph -> ( O ` X ) e. ( Base ` ( R ^s K ) ) )
101 21 22 11 24 99 100 8 84 pwsmulrval 
 |-  ( ph -> ( ( O ` ( ( algSc ` P ) ` M ) ) ( .r ` ( R ^s K ) ) ( O ` X ) ) = ( ( O ` ( ( algSc ` P ) ` M ) ) oF .X. ( O ` X ) ) )
102 4 1 7 79 evl1sca 
 |-  ( ( R e. CRing /\ M e. K ) -> ( O ` ( ( algSc ` P ) ` M ) ) = ( K X. { M } ) )
103 11 12 102 syl2anc 
 |-  ( ph -> ( O ` ( ( algSc ` P ) ` M ) ) = ( K X. { M } ) )
104 4 9 7 evl1var 
 |-  ( R e. CRing -> ( O ` X ) = ( _I |` K ) )
105 11 104 syl 
 |-  ( ph -> ( O ` X ) = ( _I |` K ) )
106 103 105 oveq12d 
 |-  ( ph -> ( ( O ` ( ( algSc ` P ) ` M ) ) oF .X. ( O ` X ) ) = ( ( K X. { M } ) oF .X. ( _I |` K ) ) )
107 101 106 eqtrd 
 |-  ( ph -> ( ( O ` ( ( algSc ` P ) ` M ) ) ( .r ` ( R ^s K ) ) ( O ` X ) ) = ( ( K X. { M } ) oF .X. ( _I |` K ) ) )
108 86 98 107 3eqtr3d 
 |-  ( ph -> ( O ` ( M .x. X ) ) = ( ( K X. { M } ) oF .X. ( _I |` K ) ) )
109 108 fveq1d 
 |-  ( ph -> ( ( O ` ( M .x. X ) ) ` W ) = ( ( ( K X. { M } ) oF .X. ( _I |` K ) ) ` W ) )
110 fnconstg 
 |-  ( M e. K -> ( K X. { M } ) Fn K )
111 12 110 syl 
 |-  ( ph -> ( K X. { M } ) Fn K )
112 fnresi 
 |-  ( _I |` K ) Fn K
113 112 a1i 
 |-  ( ph -> ( _I |` K ) Fn K )
114 fnfvof 
 |-  ( ( ( ( K X. { M } ) Fn K /\ ( _I |` K ) Fn K ) /\ ( K e. _V /\ W e. K ) ) -> ( ( ( K X. { M } ) oF .X. ( _I |` K ) ) ` W ) = ( ( ( K X. { M } ) ` W ) .X. ( ( _I |` K ) ` W ) ) )
115 111 113 24 78 114 syl22anc 
 |-  ( ph -> ( ( ( K X. { M } ) oF .X. ( _I |` K ) ) ` W ) = ( ( ( K X. { M } ) ` W ) .X. ( ( _I |` K ) ` W ) ) )
116 fvconst2g 
 |-  ( ( M e. K /\ W e. K ) -> ( ( K X. { M } ) ` W ) = M )
117 12 78 116 syl2anc 
 |-  ( ph -> ( ( K X. { M } ) ` W ) = M )
118 fvresi 
 |-  ( W e. K -> ( ( _I |` K ) ` W ) = W )
119 78 118 syl 
 |-  ( ph -> ( ( _I |` K ) ` W ) = W )
120 117 119 oveq12d 
 |-  ( ph -> ( ( ( K X. { M } ) ` W ) .X. ( ( _I |` K ) ` W ) ) = ( M .X. W ) )
121 7 8 5 ringrz 
 |-  ( ( R e. Ring /\ M e. K ) -> ( M .X. W ) = W )
122 43 12 121 syl2anc 
 |-  ( ph -> ( M .X. W ) = W )
123 120 122 eqtrd 
 |-  ( ph -> ( ( ( K X. { M } ) ` W ) .X. ( ( _I |` K ) ` W ) ) = W )
124 115 123 eqtrd 
 |-  ( ph -> ( ( ( K X. { M } ) oF .X. ( _I |` K ) ) ` W ) = W )
125 109 124 eqtrd 
 |-  ( ph -> ( ( O ` ( M .x. X ) ) ` W ) = W )
126 fniniseg 
 |-  ( ( O ` ( M .x. X ) ) Fn K -> ( W e. ( `' ( O ` ( M .x. X ) ) " { W } ) <-> ( W e. K /\ ( ( O ` ( M .x. X ) ) ` W ) = W ) ) )
127 32 126 syl 
 |-  ( ph -> ( W e. ( `' ( O ` ( M .x. X ) ) " { W } ) <-> ( W e. K /\ ( ( O ` ( M .x. X ) ) ` W ) = W ) ) )
128 78 125 127 mpbir2and 
 |-  ( ph -> W e. ( `' ( O ` ( M .x. X ) ) " { W } ) )
129 128 snssd 
 |-  ( ph -> { W } C_ ( `' ( O ` ( M .x. X ) ) " { W } ) )
130 hashsng 
 |-  ( W e. K -> ( # ` { W } ) = 1 )
131 78 130 syl 
 |-  ( ph -> ( # ` { W } ) = 1 )
132 ssdomg 
 |-  ( ( `' ( O ` ( M .x. X ) ) " { W } ) e. _V -> ( { W } C_ ( `' ( O ` ( M .x. X ) ) " { W } ) -> { W } ~<_ ( `' ( O ` ( M .x. X ) ) " { W } ) ) )
133 38 129 132 mpsyl 
 |-  ( ph -> { W } ~<_ ( `' ( O ` ( M .x. X ) ) " { W } ) )
134 snfi 
 |-  { W } e. Fin
135 hashdom 
 |-  ( ( { W } e. Fin /\ ( `' ( O ` ( M .x. X ) ) " { W } ) e. _V ) -> ( ( # ` { W } ) <_ ( # ` ( `' ( O ` ( M .x. X ) ) " { W } ) ) <-> { W } ~<_ ( `' ( O ` ( M .x. X ) ) " { W } ) ) )
136 134 38 135 mp2an 
 |-  ( ( # ` { W } ) <_ ( # ` ( `' ( O ` ( M .x. X ) ) " { W } ) ) <-> { W } ~<_ ( `' ( O ` ( M .x. X ) ) " { W } ) )
137 133 136 sylibr 
 |-  ( ph -> ( # ` { W } ) <_ ( # ` ( `' ( O ` ( M .x. X ) ) " { W } ) ) )
138 131 137 eqbrtrrd 
 |-  ( ph -> 1 <_ ( # ` ( `' ( O ` ( M .x. X ) ) " { W } ) ) )
139 hashcl 
 |-  ( ( `' ( O ` ( M .x. X ) ) " { W } ) e. Fin -> ( # ` ( `' ( O ` ( M .x. X ) ) " { W } ) ) e. NN0 )
140 76 139 syl 
 |-  ( ph -> ( # ` ( `' ( O ` ( M .x. X ) ) " { W } ) ) e. NN0 )
141 140 nn0red 
 |-  ( ph -> ( # ` ( `' ( O ` ( M .x. X ) ) " { W } ) ) e. RR )
142 1re 
 |-  1 e. RR
143 letri3 
 |-  ( ( ( # ` ( `' ( O ` ( M .x. X ) ) " { W } ) ) e. RR /\ 1 e. RR ) -> ( ( # ` ( `' ( O ` ( M .x. X ) ) " { W } ) ) = 1 <-> ( ( # ` ( `' ( O ` ( M .x. X ) ) " { W } ) ) <_ 1 /\ 1 <_ ( # ` ( `' ( O ` ( M .x. X ) ) " { W } ) ) ) ) )
144 141 142 143 sylancl 
 |-  ( ph -> ( ( # ` ( `' ( O ` ( M .x. X ) ) " { W } ) ) = 1 <-> ( ( # ` ( `' ( O ` ( M .x. X ) ) " { W } ) ) <_ 1 /\ 1 <_ ( # ` ( `' ( O ` ( M .x. X ) ) " { W } ) ) ) ) )
145 74 138 144 mpbir2and 
 |-  ( ph -> ( # ` ( `' ( O ` ( M .x. X ) ) " { W } ) ) = 1 )
146 131 145 eqtr4d 
 |-  ( ph -> ( # ` { W } ) = ( # ` ( `' ( O ` ( M .x. X ) ) " { W } ) ) )
147 hashen 
 |-  ( ( { W } e. Fin /\ ( `' ( O ` ( M .x. X ) ) " { W } ) e. Fin ) -> ( ( # ` { W } ) = ( # ` ( `' ( O ` ( M .x. X ) ) " { W } ) ) <-> { W } ~~ ( `' ( O ` ( M .x. X ) ) " { W } ) ) )
148 134 76 147 sylancr 
 |-  ( ph -> ( ( # ` { W } ) = ( # ` ( `' ( O ` ( M .x. X ) ) " { W } ) ) <-> { W } ~~ ( `' ( O ` ( M .x. X ) ) " { W } ) ) )
149 146 148 mpbid 
 |-  ( ph -> { W } ~~ ( `' ( O ` ( M .x. X ) ) " { W } ) )
150 fisseneq 
 |-  ( ( ( `' ( O ` ( M .x. X ) ) " { W } ) e. Fin /\ { W } C_ ( `' ( O ` ( M .x. X ) ) " { W } ) /\ { W } ~~ ( `' ( O ` ( M .x. X ) ) " { W } ) ) -> { W } = ( `' ( O ` ( M .x. X ) ) " { W } ) )
151 76 129 149 150 syl3anc 
 |-  ( ph -> { W } = ( `' ( O ` ( M .x. X ) ) " { W } ) )
152 35 151 eleqtrrd 
 |-  ( ph -> N e. { W } )
153 elsni 
 |-  ( N e. { W } -> N = W )
154 152 153 syl 
 |-  ( ph -> N = W )