Metamath Proof Explorer


Theorem psrmulcllem

Description: Closure of the power series multiplication operation. (Contributed by Mario Carneiro, 29-Dec-2014)

Ref Expression
Hypotheses psrmulcl.s โŠข ๐‘† = ( ๐ผ mPwSer ๐‘… )
psrmulcl.b โŠข ๐ต = ( Base โ€˜ ๐‘† )
psrmulcl.t โŠข ยท = ( .r โ€˜ ๐‘† )
psrmulcl.r โŠข ( ๐œ‘ โ†’ ๐‘… โˆˆ Ring )
psrmulcl.x โŠข ( ๐œ‘ โ†’ ๐‘‹ โˆˆ ๐ต )
psrmulcl.y โŠข ( ๐œ‘ โ†’ ๐‘Œ โˆˆ ๐ต )
psrmulcl.d โŠข ๐ท = { ๐‘“ โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก ๐‘“ โ€œ โ„• ) โˆˆ Fin }
Assertion psrmulcllem ( ๐œ‘ โ†’ ( ๐‘‹ ยท ๐‘Œ ) โˆˆ ๐ต )

Proof

Step Hyp Ref Expression
1 psrmulcl.s โŠข ๐‘† = ( ๐ผ mPwSer ๐‘… )
2 psrmulcl.b โŠข ๐ต = ( Base โ€˜ ๐‘† )
3 psrmulcl.t โŠข ยท = ( .r โ€˜ ๐‘† )
4 psrmulcl.r โŠข ( ๐œ‘ โ†’ ๐‘… โˆˆ Ring )
5 psrmulcl.x โŠข ( ๐œ‘ โ†’ ๐‘‹ โˆˆ ๐ต )
6 psrmulcl.y โŠข ( ๐œ‘ โ†’ ๐‘Œ โˆˆ ๐ต )
7 psrmulcl.d โŠข ๐ท = { ๐‘“ โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก ๐‘“ โ€œ โ„• ) โˆˆ Fin }
8 eqid โŠข ( Base โ€˜ ๐‘… ) = ( Base โ€˜ ๐‘… )
9 eqid โŠข ( 0g โ€˜ ๐‘… ) = ( 0g โ€˜ ๐‘… )
10 4 adantr โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ๐ท ) โ†’ ๐‘… โˆˆ Ring )
11 10 ringcmnd โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ๐ท ) โ†’ ๐‘… โˆˆ CMnd )
12 7 psrbaglefi โŠข ( ๐‘˜ โˆˆ ๐ท โ†’ { ๐‘ฆ โˆˆ ๐ท โˆฃ ๐‘ฆ โˆ˜r โ‰ค ๐‘˜ } โˆˆ Fin )
13 12 adantl โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ๐ท ) โ†’ { ๐‘ฆ โˆˆ ๐ท โˆฃ ๐‘ฆ โˆ˜r โ‰ค ๐‘˜ } โˆˆ Fin )
14 eqid โŠข ( .r โ€˜ ๐‘… ) = ( .r โ€˜ ๐‘… )
15 4 ad2antrr โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ๐ท ) โˆง ๐‘ฅ โˆˆ { ๐‘ฆ โˆˆ ๐ท โˆฃ ๐‘ฆ โˆ˜r โ‰ค ๐‘˜ } ) โ†’ ๐‘… โˆˆ Ring )
16 1 8 7 2 5 psrelbas โŠข ( ๐œ‘ โ†’ ๐‘‹ : ๐ท โŸถ ( Base โ€˜ ๐‘… ) )
17 16 ad2antrr โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ๐ท ) โˆง ๐‘ฅ โˆˆ { ๐‘ฆ โˆˆ ๐ท โˆฃ ๐‘ฆ โˆ˜r โ‰ค ๐‘˜ } ) โ†’ ๐‘‹ : ๐ท โŸถ ( Base โ€˜ ๐‘… ) )
18 simpr โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ๐ท ) โˆง ๐‘ฅ โˆˆ { ๐‘ฆ โˆˆ ๐ท โˆฃ ๐‘ฆ โˆ˜r โ‰ค ๐‘˜ } ) โ†’ ๐‘ฅ โˆˆ { ๐‘ฆ โˆˆ ๐ท โˆฃ ๐‘ฆ โˆ˜r โ‰ค ๐‘˜ } )
19 breq1 โŠข ( ๐‘ฆ = ๐‘ฅ โ†’ ( ๐‘ฆ โˆ˜r โ‰ค ๐‘˜ โ†” ๐‘ฅ โˆ˜r โ‰ค ๐‘˜ ) )
20 19 elrab โŠข ( ๐‘ฅ โˆˆ { ๐‘ฆ โˆˆ ๐ท โˆฃ ๐‘ฆ โˆ˜r โ‰ค ๐‘˜ } โ†” ( ๐‘ฅ โˆˆ ๐ท โˆง ๐‘ฅ โˆ˜r โ‰ค ๐‘˜ ) )
21 18 20 sylib โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ๐ท ) โˆง ๐‘ฅ โˆˆ { ๐‘ฆ โˆˆ ๐ท โˆฃ ๐‘ฆ โˆ˜r โ‰ค ๐‘˜ } ) โ†’ ( ๐‘ฅ โˆˆ ๐ท โˆง ๐‘ฅ โˆ˜r โ‰ค ๐‘˜ ) )
22 21 simpld โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ๐ท ) โˆง ๐‘ฅ โˆˆ { ๐‘ฆ โˆˆ ๐ท โˆฃ ๐‘ฆ โˆ˜r โ‰ค ๐‘˜ } ) โ†’ ๐‘ฅ โˆˆ ๐ท )
23 17 22 ffvelcdmd โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ๐ท ) โˆง ๐‘ฅ โˆˆ { ๐‘ฆ โˆˆ ๐ท โˆฃ ๐‘ฆ โˆ˜r โ‰ค ๐‘˜ } ) โ†’ ( ๐‘‹ โ€˜ ๐‘ฅ ) โˆˆ ( Base โ€˜ ๐‘… ) )
24 1 8 7 2 6 psrelbas โŠข ( ๐œ‘ โ†’ ๐‘Œ : ๐ท โŸถ ( Base โ€˜ ๐‘… ) )
25 24 ad2antrr โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ๐ท ) โˆง ๐‘ฅ โˆˆ { ๐‘ฆ โˆˆ ๐ท โˆฃ ๐‘ฆ โˆ˜r โ‰ค ๐‘˜ } ) โ†’ ๐‘Œ : ๐ท โŸถ ( Base โ€˜ ๐‘… ) )
26 simplr โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ๐ท ) โˆง ๐‘ฅ โˆˆ { ๐‘ฆ โˆˆ ๐ท โˆฃ ๐‘ฆ โˆ˜r โ‰ค ๐‘˜ } ) โ†’ ๐‘˜ โˆˆ ๐ท )
27 7 psrbagf โŠข ( ๐‘ฅ โˆˆ ๐ท โ†’ ๐‘ฅ : ๐ผ โŸถ โ„•0 )
28 22 27 syl โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ๐ท ) โˆง ๐‘ฅ โˆˆ { ๐‘ฆ โˆˆ ๐ท โˆฃ ๐‘ฆ โˆ˜r โ‰ค ๐‘˜ } ) โ†’ ๐‘ฅ : ๐ผ โŸถ โ„•0 )
29 21 simprd โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ๐ท ) โˆง ๐‘ฅ โˆˆ { ๐‘ฆ โˆˆ ๐ท โˆฃ ๐‘ฆ โˆ˜r โ‰ค ๐‘˜ } ) โ†’ ๐‘ฅ โˆ˜r โ‰ค ๐‘˜ )
30 7 psrbagcon โŠข ( ( ๐‘˜ โˆˆ ๐ท โˆง ๐‘ฅ : ๐ผ โŸถ โ„•0 โˆง ๐‘ฅ โˆ˜r โ‰ค ๐‘˜ ) โ†’ ( ( ๐‘˜ โˆ˜f โˆ’ ๐‘ฅ ) โˆˆ ๐ท โˆง ( ๐‘˜ โˆ˜f โˆ’ ๐‘ฅ ) โˆ˜r โ‰ค ๐‘˜ ) )
31 26 28 29 30 syl3anc โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ๐ท ) โˆง ๐‘ฅ โˆˆ { ๐‘ฆ โˆˆ ๐ท โˆฃ ๐‘ฆ โˆ˜r โ‰ค ๐‘˜ } ) โ†’ ( ( ๐‘˜ โˆ˜f โˆ’ ๐‘ฅ ) โˆˆ ๐ท โˆง ( ๐‘˜ โˆ˜f โˆ’ ๐‘ฅ ) โˆ˜r โ‰ค ๐‘˜ ) )
32 31 simpld โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ๐ท ) โˆง ๐‘ฅ โˆˆ { ๐‘ฆ โˆˆ ๐ท โˆฃ ๐‘ฆ โˆ˜r โ‰ค ๐‘˜ } ) โ†’ ( ๐‘˜ โˆ˜f โˆ’ ๐‘ฅ ) โˆˆ ๐ท )
33 25 32 ffvelcdmd โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ๐ท ) โˆง ๐‘ฅ โˆˆ { ๐‘ฆ โˆˆ ๐ท โˆฃ ๐‘ฆ โˆ˜r โ‰ค ๐‘˜ } ) โ†’ ( ๐‘Œ โ€˜ ( ๐‘˜ โˆ˜f โˆ’ ๐‘ฅ ) ) โˆˆ ( Base โ€˜ ๐‘… ) )
34 8 14 15 23 33 ringcld โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ๐ท ) โˆง ๐‘ฅ โˆˆ { ๐‘ฆ โˆˆ ๐ท โˆฃ ๐‘ฆ โˆ˜r โ‰ค ๐‘˜ } ) โ†’ ( ( ๐‘‹ โ€˜ ๐‘ฅ ) ( .r โ€˜ ๐‘… ) ( ๐‘Œ โ€˜ ( ๐‘˜ โˆ˜f โˆ’ ๐‘ฅ ) ) ) โˆˆ ( Base โ€˜ ๐‘… ) )
35 34 fmpttd โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ๐ท ) โ†’ ( ๐‘ฅ โˆˆ { ๐‘ฆ โˆˆ ๐ท โˆฃ ๐‘ฆ โˆ˜r โ‰ค ๐‘˜ } โ†ฆ ( ( ๐‘‹ โ€˜ ๐‘ฅ ) ( .r โ€˜ ๐‘… ) ( ๐‘Œ โ€˜ ( ๐‘˜ โˆ˜f โˆ’ ๐‘ฅ ) ) ) ) : { ๐‘ฆ โˆˆ ๐ท โˆฃ ๐‘ฆ โˆ˜r โ‰ค ๐‘˜ } โŸถ ( Base โ€˜ ๐‘… ) )
36 fvexd โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ๐ท ) โ†’ ( 0g โ€˜ ๐‘… ) โˆˆ V )
37 35 13 36 fdmfifsupp โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ๐ท ) โ†’ ( ๐‘ฅ โˆˆ { ๐‘ฆ โˆˆ ๐ท โˆฃ ๐‘ฆ โˆ˜r โ‰ค ๐‘˜ } โ†ฆ ( ( ๐‘‹ โ€˜ ๐‘ฅ ) ( .r โ€˜ ๐‘… ) ( ๐‘Œ โ€˜ ( ๐‘˜ โˆ˜f โˆ’ ๐‘ฅ ) ) ) ) finSupp ( 0g โ€˜ ๐‘… ) )
38 8 9 11 13 35 37 gsumcl โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ๐ท ) โ†’ ( ๐‘… ฮฃg ( ๐‘ฅ โˆˆ { ๐‘ฆ โˆˆ ๐ท โˆฃ ๐‘ฆ โˆ˜r โ‰ค ๐‘˜ } โ†ฆ ( ( ๐‘‹ โ€˜ ๐‘ฅ ) ( .r โ€˜ ๐‘… ) ( ๐‘Œ โ€˜ ( ๐‘˜ โˆ˜f โˆ’ ๐‘ฅ ) ) ) ) ) โˆˆ ( Base โ€˜ ๐‘… ) )
39 38 fmpttd โŠข ( ๐œ‘ โ†’ ( ๐‘˜ โˆˆ ๐ท โ†ฆ ( ๐‘… ฮฃg ( ๐‘ฅ โˆˆ { ๐‘ฆ โˆˆ ๐ท โˆฃ ๐‘ฆ โˆ˜r โ‰ค ๐‘˜ } โ†ฆ ( ( ๐‘‹ โ€˜ ๐‘ฅ ) ( .r โ€˜ ๐‘… ) ( ๐‘Œ โ€˜ ( ๐‘˜ โˆ˜f โˆ’ ๐‘ฅ ) ) ) ) ) ) : ๐ท โŸถ ( Base โ€˜ ๐‘… ) )
40 fvex โŠข ( Base โ€˜ ๐‘… ) โˆˆ V
41 ovex โŠข ( โ„•0 โ†‘m ๐ผ ) โˆˆ V
42 7 41 rabex2 โŠข ๐ท โˆˆ V
43 40 42 elmap โŠข ( ( ๐‘˜ โˆˆ ๐ท โ†ฆ ( ๐‘… ฮฃg ( ๐‘ฅ โˆˆ { ๐‘ฆ โˆˆ ๐ท โˆฃ ๐‘ฆ โˆ˜r โ‰ค ๐‘˜ } โ†ฆ ( ( ๐‘‹ โ€˜ ๐‘ฅ ) ( .r โ€˜ ๐‘… ) ( ๐‘Œ โ€˜ ( ๐‘˜ โˆ˜f โˆ’ ๐‘ฅ ) ) ) ) ) ) โˆˆ ( ( Base โ€˜ ๐‘… ) โ†‘m ๐ท ) โ†” ( ๐‘˜ โˆˆ ๐ท โ†ฆ ( ๐‘… ฮฃg ( ๐‘ฅ โˆˆ { ๐‘ฆ โˆˆ ๐ท โˆฃ ๐‘ฆ โˆ˜r โ‰ค ๐‘˜ } โ†ฆ ( ( ๐‘‹ โ€˜ ๐‘ฅ ) ( .r โ€˜ ๐‘… ) ( ๐‘Œ โ€˜ ( ๐‘˜ โˆ˜f โˆ’ ๐‘ฅ ) ) ) ) ) ) : ๐ท โŸถ ( Base โ€˜ ๐‘… ) )
44 39 43 sylibr โŠข ( ๐œ‘ โ†’ ( ๐‘˜ โˆˆ ๐ท โ†ฆ ( ๐‘… ฮฃg ( ๐‘ฅ โˆˆ { ๐‘ฆ โˆˆ ๐ท โˆฃ ๐‘ฆ โˆ˜r โ‰ค ๐‘˜ } โ†ฆ ( ( ๐‘‹ โ€˜ ๐‘ฅ ) ( .r โ€˜ ๐‘… ) ( ๐‘Œ โ€˜ ( ๐‘˜ โˆ˜f โˆ’ ๐‘ฅ ) ) ) ) ) ) โˆˆ ( ( Base โ€˜ ๐‘… ) โ†‘m ๐ท ) )
45 1 2 14 3 7 5 6 psrmulfval โŠข ( ๐œ‘ โ†’ ( ๐‘‹ ยท ๐‘Œ ) = ( ๐‘˜ โˆˆ ๐ท โ†ฆ ( ๐‘… ฮฃg ( ๐‘ฅ โˆˆ { ๐‘ฆ โˆˆ ๐ท โˆฃ ๐‘ฆ โˆ˜r โ‰ค ๐‘˜ } โ†ฆ ( ( ๐‘‹ โ€˜ ๐‘ฅ ) ( .r โ€˜ ๐‘… ) ( ๐‘Œ โ€˜ ( ๐‘˜ โˆ˜f โˆ’ ๐‘ฅ ) ) ) ) ) ) )
46 reldmpsr โŠข Rel dom mPwSer
47 46 1 2 elbasov โŠข ( ๐‘‹ โˆˆ ๐ต โ†’ ( ๐ผ โˆˆ V โˆง ๐‘… โˆˆ V ) )
48 5 47 syl โŠข ( ๐œ‘ โ†’ ( ๐ผ โˆˆ V โˆง ๐‘… โˆˆ V ) )
49 48 simpld โŠข ( ๐œ‘ โ†’ ๐ผ โˆˆ V )
50 1 8 7 2 49 psrbas โŠข ( ๐œ‘ โ†’ ๐ต = ( ( Base โ€˜ ๐‘… ) โ†‘m ๐ท ) )
51 44 45 50 3eltr4d โŠข ( ๐œ‘ โ†’ ( ๐‘‹ ยท ๐‘Œ ) โˆˆ ๐ต )