Metamath Proof Explorer


Theorem mplmon2cl

Description: A scaled monomial is a polynomial. (Contributed by Stefan O'Rear, 8-Mar-2015)

Ref Expression
Hypotheses mplmon2cl.p โŠข ๐‘ƒ = ( ๐ผ mPoly ๐‘… )
mplmon2cl.d โŠข ๐ท = { ๐‘“ โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก ๐‘“ โ€œ โ„• ) โˆˆ Fin }
mplmon2cl.z โŠข 0 = ( 0g โ€˜ ๐‘… )
mplmon2cl.c โŠข ๐ถ = ( Base โ€˜ ๐‘… )
mplmon2cl.i โŠข ( ๐œ‘ โ†’ ๐ผ โˆˆ ๐‘Š )
mplmon2cl.r โŠข ( ๐œ‘ โ†’ ๐‘… โˆˆ Ring )
mplmon2cl.b โŠข ๐ต = ( Base โ€˜ ๐‘ƒ )
mplmon2cl.x โŠข ( ๐œ‘ โ†’ ๐‘‹ โˆˆ ๐ถ )
mplmon2cl.k โŠข ( ๐œ‘ โ†’ ๐พ โˆˆ ๐ท )
Assertion mplmon2cl ( ๐œ‘ โ†’ ( ๐‘ฆ โˆˆ ๐ท โ†ฆ if ( ๐‘ฆ = ๐พ , ๐‘‹ , 0 ) ) โˆˆ ๐ต )

Proof

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 ) ) โˆˆ ๐ต )