Step |
Hyp |
Ref |
Expression |
1 |
|
mhpvscacl.h |
|- H = ( I mHomP R ) |
2 |
|
mhpvscacl.p |
|- P = ( I mPoly R ) |
3 |
|
mhpvscacl.t |
|- .x. = ( .s ` P ) |
4 |
|
mhpvscacl.k |
|- K = ( Base ` R ) |
5 |
|
mhpvscacl.i |
|- ( ph -> I e. V ) |
6 |
|
mhpvscacl.r |
|- ( ph -> R e. Ring ) |
7 |
|
mhpvscacl.n |
|- ( ph -> N e. NN0 ) |
8 |
|
mhpvscacl.x |
|- ( ph -> X e. K ) |
9 |
|
mhpvscacl.f |
|- ( ph -> F e. ( H ` N ) ) |
10 |
|
eqid |
|- ( Base ` P ) = ( Base ` P ) |
11 |
|
eqid |
|- ( 0g ` R ) = ( 0g ` R ) |
12 |
|
eqid |
|- { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |
13 |
2
|
mpllmod |
|- ( ( I e. V /\ R e. Ring ) -> P e. LMod ) |
14 |
5 6 13
|
syl2anc |
|- ( ph -> P e. LMod ) |
15 |
8 4
|
eleqtrdi |
|- ( ph -> X e. ( Base ` R ) ) |
16 |
2 5 6
|
mplsca |
|- ( ph -> R = ( Scalar ` P ) ) |
17 |
16
|
fveq2d |
|- ( ph -> ( Base ` R ) = ( Base ` ( Scalar ` P ) ) ) |
18 |
15 17
|
eleqtrd |
|- ( ph -> X e. ( Base ` ( Scalar ` P ) ) ) |
19 |
1 2 10 5 6 7 9
|
mhpmpl |
|- ( ph -> F e. ( Base ` P ) ) |
20 |
|
eqid |
|- ( Scalar ` P ) = ( Scalar ` P ) |
21 |
|
eqid |
|- ( Base ` ( Scalar ` P ) ) = ( Base ` ( Scalar ` P ) ) |
22 |
10 20 3 21
|
lmodvscl |
|- ( ( P e. LMod /\ X e. ( Base ` ( Scalar ` P ) ) /\ F e. ( Base ` P ) ) -> ( X .x. F ) e. ( Base ` P ) ) |
23 |
14 18 19 22
|
syl3anc |
|- ( ph -> ( X .x. F ) e. ( Base ` P ) ) |
24 |
2 4 10 12 23
|
mplelf |
|- ( ph -> ( X .x. F ) : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } --> K ) |
25 |
|
eqid |
|- ( .r ` R ) = ( .r ` R ) |
26 |
8
|
adantr |
|- ( ( ph /\ k e. ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } \ ( F supp ( 0g ` R ) ) ) ) -> X e. K ) |
27 |
19
|
adantr |
|- ( ( ph /\ k e. ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } \ ( F supp ( 0g ` R ) ) ) ) -> F e. ( Base ` P ) ) |
28 |
|
eldifi |
|- ( k e. ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } \ ( F supp ( 0g ` R ) ) ) -> k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) |
29 |
28
|
adantl |
|- ( ( ph /\ k e. ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } \ ( F supp ( 0g ` R ) ) ) ) -> k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) |
30 |
2 3 4 10 25 12 26 27 29
|
mplvscaval |
|- ( ( ph /\ k e. ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } \ ( F supp ( 0g ` R ) ) ) ) -> ( ( X .x. F ) ` k ) = ( X ( .r ` R ) ( F ` k ) ) ) |
31 |
2 4 10 12 19
|
mplelf |
|- ( ph -> F : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } --> K ) |
32 |
|
ssidd |
|- ( ph -> ( F supp ( 0g ` R ) ) C_ ( F supp ( 0g ` R ) ) ) |
33 |
|
ovexd |
|- ( ph -> ( NN0 ^m I ) e. _V ) |
34 |
12 33
|
rabexd |
|- ( ph -> { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } e. _V ) |
35 |
|
fvexd |
|- ( ph -> ( 0g ` R ) e. _V ) |
36 |
31 32 34 35
|
suppssr |
|- ( ( ph /\ k e. ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } \ ( F supp ( 0g ` R ) ) ) ) -> ( F ` k ) = ( 0g ` R ) ) |
37 |
36
|
oveq2d |
|- ( ( ph /\ k e. ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } \ ( F supp ( 0g ` R ) ) ) ) -> ( X ( .r ` R ) ( F ` k ) ) = ( X ( .r ` R ) ( 0g ` R ) ) ) |
38 |
4 25 11
|
ringrz |
|- ( ( R e. Ring /\ X e. K ) -> ( X ( .r ` R ) ( 0g ` R ) ) = ( 0g ` R ) ) |
39 |
6 8 38
|
syl2anc |
|- ( ph -> ( X ( .r ` R ) ( 0g ` R ) ) = ( 0g ` R ) ) |
40 |
39
|
adantr |
|- ( ( ph /\ k e. ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } \ ( F supp ( 0g ` R ) ) ) ) -> ( X ( .r ` R ) ( 0g ` R ) ) = ( 0g ` R ) ) |
41 |
30 37 40
|
3eqtrd |
|- ( ( ph /\ k e. ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } \ ( F supp ( 0g ` R ) ) ) ) -> ( ( X .x. F ) ` k ) = ( 0g ` R ) ) |
42 |
24 41
|
suppss |
|- ( ph -> ( ( X .x. F ) supp ( 0g ` R ) ) C_ ( F supp ( 0g ` R ) ) ) |
43 |
1 11 12 5 6 7 9
|
mhpdeg |
|- ( ph -> ( F supp ( 0g ` R ) ) C_ { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) |
44 |
42 43
|
sstrd |
|- ( ph -> ( ( X .x. F ) supp ( 0g ` R ) ) C_ { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) |
45 |
1 2 10 11 12 5 6 7 23 44
|
ismhp2 |
|- ( ph -> ( X .x. F ) e. ( H ` N ) ) |