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 syl5eq
 |-  ( 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 )