Metamath Proof Explorer


Theorem psrvscafval

Description: The scalar multiplication operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014) (Revised by Mario Carneiro, 2-Oct-2015) (Proof shortened by AV, 2-Nov-2024)

Ref Expression
Hypotheses psrvsca.s โŠข ๐‘† = ( ๐ผ mPwSer ๐‘… )
psrvsca.n โŠข โˆ™ = ( ยท๐‘  โ€˜ ๐‘† )
psrvsca.k โŠข ๐พ = ( Base โ€˜ ๐‘… )
psrvsca.b โŠข ๐ต = ( Base โ€˜ ๐‘† )
psrvsca.m โŠข ยท = ( .r โ€˜ ๐‘… )
psrvsca.d โŠข ๐ท = { โ„Ž โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin }
Assertion psrvscafval โˆ™ = ( ๐‘ฅ โˆˆ ๐พ , ๐‘“ โˆˆ ๐ต โ†ฆ ( ( ๐ท ร— { ๐‘ฅ } ) โˆ˜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 eqid โŠข ( +g โ€˜ ๐‘… ) = ( +g โ€˜ ๐‘… )
8 eqid โŠข ( TopOpen โ€˜ ๐‘… ) = ( TopOpen โ€˜ ๐‘… )
9 simpl โŠข ( ( ๐ผ โˆˆ V โˆง ๐‘… โˆˆ V ) โ†’ ๐ผ โˆˆ V )
10 1 3 6 4 9 psrbas โŠข ( ( ๐ผ โˆˆ V โˆง ๐‘… โˆˆ V ) โ†’ ๐ต = ( ๐พ โ†‘m ๐ท ) )
11 eqid โŠข ( +g โ€˜ ๐‘† ) = ( +g โ€˜ ๐‘† )
12 1 4 7 11 psrplusg โŠข ( +g โ€˜ ๐‘† ) = ( โˆ˜f ( +g โ€˜ ๐‘… ) โ†พ ( ๐ต ร— ๐ต ) )
13 eqid โŠข ( .r โ€˜ ๐‘† ) = ( .r โ€˜ ๐‘† )
14 1 4 5 13 6 psrmulr โŠข ( .r โ€˜ ๐‘† ) = ( ๐‘“ โˆˆ ๐ต , ๐‘” โˆˆ ๐ต โ†ฆ ( ๐‘˜ โˆˆ ๐ท โ†ฆ ( ๐‘… ฮฃg ( ๐‘ฅ โˆˆ { ๐‘ฆ โˆˆ ๐ท โˆฃ ๐‘ฆ โˆ˜r โ‰ค ๐‘˜ } โ†ฆ ( ( ๐‘“ โ€˜ ๐‘ฅ ) ยท ( ๐‘” โ€˜ ( ๐‘˜ โˆ˜f โˆ’ ๐‘ฅ ) ) ) ) ) ) )
15 eqid โŠข ( ๐‘ฅ โˆˆ ๐พ , ๐‘“ โˆˆ ๐ต โ†ฆ ( ( ๐ท ร— { ๐‘ฅ } ) โˆ˜f ยท ๐‘“ ) ) = ( ๐‘ฅ โˆˆ ๐พ , ๐‘“ โˆˆ ๐ต โ†ฆ ( ( ๐ท ร— { ๐‘ฅ } ) โˆ˜f ยท ๐‘“ ) )
16 eqidd โŠข ( ( ๐ผ โˆˆ V โˆง ๐‘… โˆˆ V ) โ†’ ( โˆt โ€˜ ( ๐ท ร— { ( TopOpen โ€˜ ๐‘… ) } ) ) = ( โˆt โ€˜ ( ๐ท ร— { ( TopOpen โ€˜ ๐‘… ) } ) ) )
17 simpr โŠข ( ( ๐ผ โˆˆ V โˆง ๐‘… โˆˆ V ) โ†’ ๐‘… โˆˆ V )
18 1 3 7 5 8 6 10 12 14 15 16 9 17 psrval โŠข ( ( ๐ผ โˆˆ V โˆง ๐‘… โˆˆ V ) โ†’ ๐‘† = ( { โŸจ ( Base โ€˜ ndx ) , ๐ต โŸฉ , โŸจ ( +g โ€˜ ndx ) , ( +g โ€˜ ๐‘† ) โŸฉ , โŸจ ( .r โ€˜ ndx ) , ( .r โ€˜ ๐‘† ) โŸฉ } โˆช { โŸจ ( Scalar โ€˜ ndx ) , ๐‘… โŸฉ , โŸจ ( ยท๐‘  โ€˜ ndx ) , ( ๐‘ฅ โˆˆ ๐พ , ๐‘“ โˆˆ ๐ต โ†ฆ ( ( ๐ท ร— { ๐‘ฅ } ) โˆ˜f ยท ๐‘“ ) ) โŸฉ , โŸจ ( TopSet โ€˜ ndx ) , ( โˆt โ€˜ ( ๐ท ร— { ( TopOpen โ€˜ ๐‘… ) } ) ) โŸฉ } ) )
19 18 fveq2d โŠข ( ( ๐ผ โˆˆ V โˆง ๐‘… โˆˆ V ) โ†’ ( ยท๐‘  โ€˜ ๐‘† ) = ( ยท๐‘  โ€˜ ( { โŸจ ( Base โ€˜ ndx ) , ๐ต โŸฉ , โŸจ ( +g โ€˜ ndx ) , ( +g โ€˜ ๐‘† ) โŸฉ , โŸจ ( .r โ€˜ ndx ) , ( .r โ€˜ ๐‘† ) โŸฉ } โˆช { โŸจ ( Scalar โ€˜ ndx ) , ๐‘… โŸฉ , โŸจ ( ยท๐‘  โ€˜ ndx ) , ( ๐‘ฅ โˆˆ ๐พ , ๐‘“ โˆˆ ๐ต โ†ฆ ( ( ๐ท ร— { ๐‘ฅ } ) โˆ˜f ยท ๐‘“ ) ) โŸฉ , โŸจ ( TopSet โ€˜ ndx ) , ( โˆt โ€˜ ( ๐ท ร— { ( TopOpen โ€˜ ๐‘… ) } ) ) โŸฉ } ) ) )
20 3 fvexi โŠข ๐พ โˆˆ V
21 4 fvexi โŠข ๐ต โˆˆ V
22 20 21 mpoex โŠข ( ๐‘ฅ โˆˆ ๐พ , ๐‘“ โˆˆ ๐ต โ†ฆ ( ( ๐ท ร— { ๐‘ฅ } ) โˆ˜f ยท ๐‘“ ) ) โˆˆ V
23 psrvalstr โŠข ( { โŸจ ( Base โ€˜ ndx ) , ๐ต โŸฉ , โŸจ ( +g โ€˜ ndx ) , ( +g โ€˜ ๐‘† ) โŸฉ , โŸจ ( .r โ€˜ ndx ) , ( .r โ€˜ ๐‘† ) โŸฉ } โˆช { โŸจ ( Scalar โ€˜ ndx ) , ๐‘… โŸฉ , โŸจ ( ยท๐‘  โ€˜ ndx ) , ( ๐‘ฅ โˆˆ ๐พ , ๐‘“ โˆˆ ๐ต โ†ฆ ( ( ๐ท ร— { ๐‘ฅ } ) โˆ˜f ยท ๐‘“ ) ) โŸฉ , โŸจ ( TopSet โ€˜ ndx ) , ( โˆt โ€˜ ( ๐ท ร— { ( TopOpen โ€˜ ๐‘… ) } ) ) โŸฉ } ) Struct โŸจ 1 , 9 โŸฉ
24 vscaid โŠข ยท๐‘  = Slot ( ยท๐‘  โ€˜ ndx )
25 snsstp2 โŠข { โŸจ ( ยท๐‘  โ€˜ ndx ) , ( ๐‘ฅ โˆˆ ๐พ , ๐‘“ โˆˆ ๐ต โ†ฆ ( ( ๐ท ร— { ๐‘ฅ } ) โˆ˜f ยท ๐‘“ ) ) โŸฉ } โІ { โŸจ ( Scalar โ€˜ ndx ) , ๐‘… โŸฉ , โŸจ ( ยท๐‘  โ€˜ ndx ) , ( ๐‘ฅ โˆˆ ๐พ , ๐‘“ โˆˆ ๐ต โ†ฆ ( ( ๐ท ร— { ๐‘ฅ } ) โˆ˜f ยท ๐‘“ ) ) โŸฉ , โŸจ ( TopSet โ€˜ ndx ) , ( โˆt โ€˜ ( ๐ท ร— { ( TopOpen โ€˜ ๐‘… ) } ) ) โŸฉ }
26 ssun2 โŠข { โŸจ ( Scalar โ€˜ ndx ) , ๐‘… โŸฉ , โŸจ ( ยท๐‘  โ€˜ ndx ) , ( ๐‘ฅ โˆˆ ๐พ , ๐‘“ โˆˆ ๐ต โ†ฆ ( ( ๐ท ร— { ๐‘ฅ } ) โˆ˜f ยท ๐‘“ ) ) โŸฉ , โŸจ ( TopSet โ€˜ ndx ) , ( โˆt โ€˜ ( ๐ท ร— { ( TopOpen โ€˜ ๐‘… ) } ) ) โŸฉ } โІ ( { โŸจ ( Base โ€˜ ndx ) , ๐ต โŸฉ , โŸจ ( +g โ€˜ ndx ) , ( +g โ€˜ ๐‘† ) โŸฉ , โŸจ ( .r โ€˜ ndx ) , ( .r โ€˜ ๐‘† ) โŸฉ } โˆช { โŸจ ( Scalar โ€˜ ndx ) , ๐‘… โŸฉ , โŸจ ( ยท๐‘  โ€˜ ndx ) , ( ๐‘ฅ โˆˆ ๐พ , ๐‘“ โˆˆ ๐ต โ†ฆ ( ( ๐ท ร— { ๐‘ฅ } ) โˆ˜f ยท ๐‘“ ) ) โŸฉ , โŸจ ( TopSet โ€˜ ndx ) , ( โˆt โ€˜ ( ๐ท ร— { ( TopOpen โ€˜ ๐‘… ) } ) ) โŸฉ } )
27 25 26 sstri โŠข { โŸจ ( ยท๐‘  โ€˜ ndx ) , ( ๐‘ฅ โˆˆ ๐พ , ๐‘“ โˆˆ ๐ต โ†ฆ ( ( ๐ท ร— { ๐‘ฅ } ) โˆ˜f ยท ๐‘“ ) ) โŸฉ } โІ ( { โŸจ ( Base โ€˜ ndx ) , ๐ต โŸฉ , โŸจ ( +g โ€˜ ndx ) , ( +g โ€˜ ๐‘† ) โŸฉ , โŸจ ( .r โ€˜ ndx ) , ( .r โ€˜ ๐‘† ) โŸฉ } โˆช { โŸจ ( Scalar โ€˜ ndx ) , ๐‘… โŸฉ , โŸจ ( ยท๐‘  โ€˜ ndx ) , ( ๐‘ฅ โˆˆ ๐พ , ๐‘“ โˆˆ ๐ต โ†ฆ ( ( ๐ท ร— { ๐‘ฅ } ) โˆ˜f ยท ๐‘“ ) ) โŸฉ , โŸจ ( TopSet โ€˜ ndx ) , ( โˆt โ€˜ ( ๐ท ร— { ( TopOpen โ€˜ ๐‘… ) } ) ) โŸฉ } )
28 23 24 27 strfv โŠข ( ( ๐‘ฅ โˆˆ ๐พ , ๐‘“ โˆˆ ๐ต โ†ฆ ( ( ๐ท ร— { ๐‘ฅ } ) โˆ˜f ยท ๐‘“ ) ) โˆˆ V โ†’ ( ๐‘ฅ โˆˆ ๐พ , ๐‘“ โˆˆ ๐ต โ†ฆ ( ( ๐ท ร— { ๐‘ฅ } ) โˆ˜f ยท ๐‘“ ) ) = ( ยท๐‘  โ€˜ ( { โŸจ ( Base โ€˜ ndx ) , ๐ต โŸฉ , โŸจ ( +g โ€˜ ndx ) , ( +g โ€˜ ๐‘† ) โŸฉ , โŸจ ( .r โ€˜ ndx ) , ( .r โ€˜ ๐‘† ) โŸฉ } โˆช { โŸจ ( Scalar โ€˜ ndx ) , ๐‘… โŸฉ , โŸจ ( ยท๐‘  โ€˜ ndx ) , ( ๐‘ฅ โˆˆ ๐พ , ๐‘“ โˆˆ ๐ต โ†ฆ ( ( ๐ท ร— { ๐‘ฅ } ) โˆ˜f ยท ๐‘“ ) ) โŸฉ , โŸจ ( TopSet โ€˜ ndx ) , ( โˆt โ€˜ ( ๐ท ร— { ( TopOpen โ€˜ ๐‘… ) } ) ) โŸฉ } ) ) )
29 22 28 ax-mp โŠข ( ๐‘ฅ โˆˆ ๐พ , ๐‘“ โˆˆ ๐ต โ†ฆ ( ( ๐ท ร— { ๐‘ฅ } ) โˆ˜f ยท ๐‘“ ) ) = ( ยท๐‘  โ€˜ ( { โŸจ ( Base โ€˜ ndx ) , ๐ต โŸฉ , โŸจ ( +g โ€˜ ndx ) , ( +g โ€˜ ๐‘† ) โŸฉ , โŸจ ( .r โ€˜ ndx ) , ( .r โ€˜ ๐‘† ) โŸฉ } โˆช { โŸจ ( Scalar โ€˜ ndx ) , ๐‘… โŸฉ , โŸจ ( ยท๐‘  โ€˜ ndx ) , ( ๐‘ฅ โˆˆ ๐พ , ๐‘“ โˆˆ ๐ต โ†ฆ ( ( ๐ท ร— { ๐‘ฅ } ) โˆ˜f ยท ๐‘“ ) ) โŸฉ , โŸจ ( TopSet โ€˜ ndx ) , ( โˆt โ€˜ ( ๐ท ร— { ( TopOpen โ€˜ ๐‘… ) } ) ) โŸฉ } ) )
30 19 2 29 3eqtr4g โŠข ( ( ๐ผ โˆˆ V โˆง ๐‘… โˆˆ V ) โ†’ โˆ™ = ( ๐‘ฅ โˆˆ ๐พ , ๐‘“ โˆˆ ๐ต โ†ฆ ( ( ๐ท ร— { ๐‘ฅ } ) โˆ˜f ยท ๐‘“ ) ) )
31 eqid โŠข โˆ… = โˆ…
32 fn0 โŠข ( โˆ… Fn โˆ… โ†” โˆ… = โˆ… )
33 31 32 mpbir โŠข โˆ… Fn โˆ…
34 reldmpsr โŠข Rel dom mPwSer
35 34 ovprc โŠข ( ยฌ ( ๐ผ โˆˆ V โˆง ๐‘… โˆˆ V ) โ†’ ( ๐ผ mPwSer ๐‘… ) = โˆ… )
36 1 35 eqtrid โŠข ( ยฌ ( ๐ผ โˆˆ V โˆง ๐‘… โˆˆ V ) โ†’ ๐‘† = โˆ… )
37 36 fveq2d โŠข ( ยฌ ( ๐ผ โˆˆ V โˆง ๐‘… โˆˆ V ) โ†’ ( ยท๐‘  โ€˜ ๐‘† ) = ( ยท๐‘  โ€˜ โˆ… ) )
38 24 str0 โŠข โˆ… = ( ยท๐‘  โ€˜ โˆ… )
39 37 2 38 3eqtr4g โŠข ( ยฌ ( ๐ผ โˆˆ V โˆง ๐‘… โˆˆ V ) โ†’ โˆ™ = โˆ… )
40 34 1 4 elbasov โŠข ( ๐‘“ โˆˆ ๐ต โ†’ ( ๐ผ โˆˆ V โˆง ๐‘… โˆˆ V ) )
41 40 con3i โŠข ( ยฌ ( ๐ผ โˆˆ V โˆง ๐‘… โˆˆ V ) โ†’ ยฌ ๐‘“ โˆˆ ๐ต )
42 41 eq0rdv โŠข ( ยฌ ( ๐ผ โˆˆ V โˆง ๐‘… โˆˆ V ) โ†’ ๐ต = โˆ… )
43 42 xpeq2d โŠข ( ยฌ ( ๐ผ โˆˆ V โˆง ๐‘… โˆˆ V ) โ†’ ( ๐พ ร— ๐ต ) = ( ๐พ ร— โˆ… ) )
44 xp0 โŠข ( ๐พ ร— โˆ… ) = โˆ…
45 43 44 eqtrdi โŠข ( ยฌ ( ๐ผ โˆˆ V โˆง ๐‘… โˆˆ V ) โ†’ ( ๐พ ร— ๐ต ) = โˆ… )
46 39 45 fneq12d โŠข ( ยฌ ( ๐ผ โˆˆ V โˆง ๐‘… โˆˆ V ) โ†’ ( โˆ™ Fn ( ๐พ ร— ๐ต ) โ†” โˆ… Fn โˆ… ) )
47 33 46 mpbiri โŠข ( ยฌ ( ๐ผ โˆˆ V โˆง ๐‘… โˆˆ V ) โ†’ โˆ™ Fn ( ๐พ ร— ๐ต ) )
48 fnov โŠข ( โˆ™ Fn ( ๐พ ร— ๐ต ) โ†” โˆ™ = ( ๐‘ฅ โˆˆ ๐พ , ๐‘“ โˆˆ ๐ต โ†ฆ ( ๐‘ฅ โˆ™ ๐‘“ ) ) )
49 47 48 sylib โŠข ( ยฌ ( ๐ผ โˆˆ V โˆง ๐‘… โˆˆ V ) โ†’ โˆ™ = ( ๐‘ฅ โˆˆ ๐พ , ๐‘“ โˆˆ ๐ต โ†ฆ ( ๐‘ฅ โˆ™ ๐‘“ ) ) )
50 41 pm2.21d โŠข ( ยฌ ( ๐ผ โˆˆ V โˆง ๐‘… โˆˆ V ) โ†’ ( ๐‘“ โˆˆ ๐ต โ†’ ( ( ๐ท ร— { ๐‘ฅ } ) โˆ˜f ยท ๐‘“ ) = ( ๐‘ฅ โˆ™ ๐‘“ ) ) )
51 50 a1d โŠข ( ยฌ ( ๐ผ โˆˆ V โˆง ๐‘… โˆˆ V ) โ†’ ( ๐‘ฅ โˆˆ ๐พ โ†’ ( ๐‘“ โˆˆ ๐ต โ†’ ( ( ๐ท ร— { ๐‘ฅ } ) โˆ˜f ยท ๐‘“ ) = ( ๐‘ฅ โˆ™ ๐‘“ ) ) ) )
52 51 3imp โŠข ( ( ยฌ ( ๐ผ โˆˆ V โˆง ๐‘… โˆˆ V ) โˆง ๐‘ฅ โˆˆ ๐พ โˆง ๐‘“ โˆˆ ๐ต ) โ†’ ( ( ๐ท ร— { ๐‘ฅ } ) โˆ˜f ยท ๐‘“ ) = ( ๐‘ฅ โˆ™ ๐‘“ ) )
53 52 mpoeq3dva โŠข ( ยฌ ( ๐ผ โˆˆ V โˆง ๐‘… โˆˆ V ) โ†’ ( ๐‘ฅ โˆˆ ๐พ , ๐‘“ โˆˆ ๐ต โ†ฆ ( ( ๐ท ร— { ๐‘ฅ } ) โˆ˜f ยท ๐‘“ ) ) = ( ๐‘ฅ โˆˆ ๐พ , ๐‘“ โˆˆ ๐ต โ†ฆ ( ๐‘ฅ โˆ™ ๐‘“ ) ) )
54 49 53 eqtr4d โŠข ( ยฌ ( ๐ผ โˆˆ V โˆง ๐‘… โˆˆ V ) โ†’ โˆ™ = ( ๐‘ฅ โˆˆ ๐พ , ๐‘“ โˆˆ ๐ต โ†ฆ ( ( ๐ท ร— { ๐‘ฅ } ) โˆ˜f ยท ๐‘“ ) ) )
55 30 54 pm2.61i โŠข โˆ™ = ( ๐‘ฅ โˆˆ ๐พ , ๐‘“ โˆˆ ๐ต โ†ฆ ( ( ๐ท ร— { ๐‘ฅ } ) โˆ˜f ยท ๐‘“ ) )