Step |
Hyp |
Ref |
Expression |
1 |
|
mplmon2cl.p |
โข ๐ = ( ๐ผ mPoly ๐
) |
2 |
|
mplmon2cl.d |
โข ๐ท = { ๐ โ ( โ0 โm ๐ผ ) โฃ ( โก ๐ โ โ ) โ Fin } |
3 |
|
mplmon2cl.z |
โข 0 = ( 0g โ ๐
) |
4 |
|
mplmon2cl.c |
โข ๐ถ = ( Base โ ๐
) |
5 |
|
mplmon2cl.i |
โข ( ๐ โ ๐ผ โ ๐ ) |
6 |
|
mplmon2cl.r |
โข ( ๐ โ ๐
โ Ring ) |
7 |
|
mplmon2cl.b |
โข ๐ต = ( Base โ ๐ ) |
8 |
|
mplmon2cl.x |
โข ( ๐ โ ๐ โ ๐ถ ) |
9 |
|
mplmon2cl.k |
โข ( ๐ โ ๐พ โ ๐ท ) |
10 |
|
eqid |
โข ( ยท๐ โ ๐ ) = ( ยท๐ โ ๐ ) |
11 |
|
eqid |
โข ( 1r โ ๐
) = ( 1r โ ๐
) |
12 |
1 10 2 11 3 4 5 6 9 8
|
mplmon2 |
โข ( ๐ โ ( ๐ ( ยท๐ โ ๐ ) ( ๐ฆ โ ๐ท โฆ if ( ๐ฆ = ๐พ , ( 1r โ ๐
) , 0 ) ) ) = ( ๐ฆ โ ๐ท โฆ if ( ๐ฆ = ๐พ , ๐ , 0 ) ) ) |
13 |
1 5 6
|
mpllmodd |
โข ( ๐ โ ๐ โ LMod ) |
14 |
1 5 6
|
mplsca |
โข ( ๐ โ ๐
= ( Scalar โ ๐ ) ) |
15 |
14
|
fveq2d |
โข ( ๐ โ ( Base โ ๐
) = ( Base โ ( Scalar โ ๐ ) ) ) |
16 |
4 15
|
eqtrid |
โข ( ๐ โ ๐ถ = ( Base โ ( Scalar โ ๐ ) ) ) |
17 |
8 16
|
eleqtrd |
โข ( ๐ โ ๐ โ ( Base โ ( Scalar โ ๐ ) ) ) |
18 |
1 7 3 11 2 5 6 9
|
mplmon |
โข ( ๐ โ ( ๐ฆ โ ๐ท โฆ if ( ๐ฆ = ๐พ , ( 1r โ ๐
) , 0 ) ) โ ๐ต ) |
19 |
|
eqid |
โข ( Scalar โ ๐ ) = ( Scalar โ ๐ ) |
20 |
|
eqid |
โข ( Base โ ( Scalar โ ๐ ) ) = ( Base โ ( Scalar โ ๐ ) ) |
21 |
7 19 10 20
|
lmodvscl |
โข ( ( ๐ โ LMod โง ๐ โ ( Base โ ( Scalar โ ๐ ) ) โง ( ๐ฆ โ ๐ท โฆ if ( ๐ฆ = ๐พ , ( 1r โ ๐
) , 0 ) ) โ ๐ต ) โ ( ๐ ( ยท๐ โ ๐ ) ( ๐ฆ โ ๐ท โฆ if ( ๐ฆ = ๐พ , ( 1r โ ๐
) , 0 ) ) ) โ ๐ต ) |
22 |
13 17 18 21
|
syl3anc |
โข ( ๐ โ ( ๐ ( ยท๐ โ ๐ ) ( ๐ฆ โ ๐ท โฆ if ( ๐ฆ = ๐พ , ( 1r โ ๐
) , 0 ) ) ) โ ๐ต ) |
23 |
12 22
|
eqeltrrd |
โข ( ๐ โ ( ๐ฆ โ ๐ท โฆ if ( ๐ฆ = ๐พ , ๐ , 0 ) ) โ ๐ต ) |