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