Metamath Proof Explorer


Theorem psrvsca

Description: The scalar multiplication operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014)

Ref Expression
Hypotheses psrvsca.s โŠข ๐‘† = ( ๐ผ mPwSer ๐‘… )
psrvsca.n โŠข โˆ™ = ( ยท๐‘  โ€˜ ๐‘† )
psrvsca.k โŠข ๐พ = ( Base โ€˜ ๐‘… )
psrvsca.b โŠข ๐ต = ( Base โ€˜ ๐‘† )
psrvsca.m โŠข ยท = ( .r โ€˜ ๐‘… )
psrvsca.d โŠข ๐ท = { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin }
psrvsca.x โŠข ( ๐œ‘ โ†’ ๐‘‹ โˆˆ ๐พ )
psrvsca.y โŠข ( ๐œ‘ โ†’ ๐น โˆˆ ๐ต )
Assertion psrvsca ( ๐œ‘ โ†’ ( ๐‘‹ โˆ™ ๐น ) = ( ( ๐ท ร— { ๐‘‹ } ) โˆ˜f ยท ๐น ) )

Proof

Step Hyp Ref Expression
1 psrvsca.s โŠข ๐‘† = ( ๐ผ mPwSer ๐‘… )
2 psrvsca.n โŠข โˆ™ = ( ยท๐‘  โ€˜ ๐‘† )
3 psrvsca.k โŠข ๐พ = ( Base โ€˜ ๐‘… )
4 psrvsca.b โŠข ๐ต = ( Base โ€˜ ๐‘† )
5 psrvsca.m โŠข ยท = ( .r โ€˜ ๐‘… )
6 psrvsca.d โŠข ๐ท = { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin }
7 psrvsca.x โŠข ( ๐œ‘ โ†’ ๐‘‹ โˆˆ ๐พ )
8 psrvsca.y โŠข ( ๐œ‘ โ†’ ๐น โˆˆ ๐ต )
9 sneq โŠข ( ๐‘ฅ = ๐‘‹ โ†’ { ๐‘ฅ } = { ๐‘‹ } )
10 9 xpeq2d โŠข ( ๐‘ฅ = ๐‘‹ โ†’ ( ๐ท ร— { ๐‘ฅ } ) = ( ๐ท ร— { ๐‘‹ } ) )
11 10 oveq1d โŠข ( ๐‘ฅ = ๐‘‹ โ†’ ( ( ๐ท ร— { ๐‘ฅ } ) โˆ˜f ยท ๐‘“ ) = ( ( ๐ท ร— { ๐‘‹ } ) โˆ˜f ยท ๐‘“ ) )
12 oveq2 โŠข ( ๐‘“ = ๐น โ†’ ( ( ๐ท ร— { ๐‘‹ } ) โˆ˜f ยท ๐‘“ ) = ( ( ๐ท ร— { ๐‘‹ } ) โˆ˜f ยท ๐น ) )
13 1 2 3 4 5 6 psrvscafval โŠข โˆ™ = ( ๐‘ฅ โˆˆ ๐พ , ๐‘“ โˆˆ ๐ต โ†ฆ ( ( ๐ท ร— { ๐‘ฅ } ) โˆ˜f ยท ๐‘“ ) )
14 ovex โŠข ( ( ๐ท ร— { ๐‘‹ } ) โˆ˜f ยท ๐น ) โˆˆ V
15 11 12 13 14 ovmpo โŠข ( ( ๐‘‹ โˆˆ ๐พ โˆง ๐น โˆˆ ๐ต ) โ†’ ( ๐‘‹ โˆ™ ๐น ) = ( ( ๐ท ร— { ๐‘‹ } ) โˆ˜f ยท ๐น ) )
16 7 8 15 syl2anc โŠข ( ๐œ‘ โ†’ ( ๐‘‹ โˆ™ ๐น ) = ( ( ๐ท ร— { ๐‘‹ } ) โˆ˜f ยท ๐น ) )