Metamath Proof Explorer


Theorem psrascl

Description: Value of the scalar injection into the power series algebra. (Contributed by SN, 18-May-2025)

Ref Expression
Hypotheses psrascl.s โŠข ๐‘† = ( ๐ผ mPwSer ๐‘… )
psrascl.d โŠข ๐ท = { ๐‘“ โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก ๐‘“ โ€œ โ„• ) โˆˆ Fin }
psrascl.z โŠข 0 = ( 0g โ€˜ ๐‘… )
psrascl.k โŠข ๐พ = ( Base โ€˜ ๐‘… )
psrascl.a โŠข ๐ด = ( algSc โ€˜ ๐‘† )
psrascl.i โŠข ( ๐œ‘ โ†’ ๐ผ โˆˆ ๐‘‰ )
psrascl.r โŠข ( ๐œ‘ โ†’ ๐‘… โˆˆ Ring )
psrascl.x โŠข ( ๐œ‘ โ†’ ๐‘‹ โˆˆ ๐พ )
Assertion psrascl ( ๐œ‘ โ†’ ( ๐ด โ€˜ ๐‘‹ ) = ( ๐‘ฆ โˆˆ ๐ท โ†ฆ if ( ๐‘ฆ = ( ๐ผ ร— { 0 } ) , ๐‘‹ , 0 ) ) )

Proof

Step Hyp Ref Expression
1 psrascl.s โŠข ๐‘† = ( ๐ผ mPwSer ๐‘… )
2 psrascl.d โŠข ๐ท = { ๐‘“ โˆˆ ( โ„•0 โ†‘m ๐ผ ) โˆฃ ( โ—ก ๐‘“ โ€œ โ„• ) โˆˆ Fin }
3 psrascl.z โŠข 0 = ( 0g โ€˜ ๐‘… )
4 psrascl.k โŠข ๐พ = ( Base โ€˜ ๐‘… )
5 psrascl.a โŠข ๐ด = ( algSc โ€˜ ๐‘† )
6 psrascl.i โŠข ( ๐œ‘ โ†’ ๐ผ โˆˆ ๐‘‰ )
7 psrascl.r โŠข ( ๐œ‘ โ†’ ๐‘… โˆˆ Ring )
8 psrascl.x โŠข ( ๐œ‘ โ†’ ๐‘‹ โˆˆ ๐พ )
9 1 6 7 psrsca โŠข ( ๐œ‘ โ†’ ๐‘… = ( Scalar โ€˜ ๐‘† ) )
10 9 fveq2d โŠข ( ๐œ‘ โ†’ ( Base โ€˜ ๐‘… ) = ( Base โ€˜ ( Scalar โ€˜ ๐‘† ) ) )
11 4 10 eqtrid โŠข ( ๐œ‘ โ†’ ๐พ = ( Base โ€˜ ( Scalar โ€˜ ๐‘† ) ) )
12 8 11 eleqtrd โŠข ( ๐œ‘ โ†’ ๐‘‹ โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘† ) ) )
13 eqid โŠข ( Scalar โ€˜ ๐‘† ) = ( Scalar โ€˜ ๐‘† )
14 eqid โŠข ( Base โ€˜ ( Scalar โ€˜ ๐‘† ) ) = ( Base โ€˜ ( Scalar โ€˜ ๐‘† ) )
15 eqid โŠข ( ยท๐‘  โ€˜ ๐‘† ) = ( ยท๐‘  โ€˜ ๐‘† )
16 eqid โŠข ( 1r โ€˜ ๐‘† ) = ( 1r โ€˜ ๐‘† )
17 5 13 14 15 16 asclval โŠข ( ๐‘‹ โˆˆ ( Base โ€˜ ( Scalar โ€˜ ๐‘† ) ) โ†’ ( ๐ด โ€˜ ๐‘‹ ) = ( ๐‘‹ ( ยท๐‘  โ€˜ ๐‘† ) ( 1r โ€˜ ๐‘† ) ) )
18 12 17 syl โŠข ( ๐œ‘ โ†’ ( ๐ด โ€˜ ๐‘‹ ) = ( ๐‘‹ ( ยท๐‘  โ€˜ ๐‘† ) ( 1r โ€˜ ๐‘† ) ) )
19 eqid โŠข ( Base โ€˜ ๐‘† ) = ( Base โ€˜ ๐‘† )
20 eqid โŠข ( .r โ€˜ ๐‘… ) = ( .r โ€˜ ๐‘… )
21 1 6 7 psrring โŠข ( ๐œ‘ โ†’ ๐‘† โˆˆ Ring )
22 19 16 ringidcl โŠข ( ๐‘† โˆˆ Ring โ†’ ( 1r โ€˜ ๐‘† ) โˆˆ ( Base โ€˜ ๐‘† ) )
23 21 22 syl โŠข ( ๐œ‘ โ†’ ( 1r โ€˜ ๐‘† ) โˆˆ ( Base โ€˜ ๐‘† ) )
24 1 15 4 19 20 2 8 23 psrvsca โŠข ( ๐œ‘ โ†’ ( ๐‘‹ ( ยท๐‘  โ€˜ ๐‘† ) ( 1r โ€˜ ๐‘† ) ) = ( ( ๐ท ร— { ๐‘‹ } ) โˆ˜f ( .r โ€˜ ๐‘… ) ( 1r โ€˜ ๐‘† ) ) )
25 fnconstg โŠข ( ๐‘‹ โˆˆ ๐พ โ†’ ( ๐ท ร— { ๐‘‹ } ) Fn ๐ท )
26 8 25 syl โŠข ( ๐œ‘ โ†’ ( ๐ท ร— { ๐‘‹ } ) Fn ๐ท )
27 1 4 2 19 23 psrelbas โŠข ( ๐œ‘ โ†’ ( 1r โ€˜ ๐‘† ) : ๐ท โŸถ ๐พ )
28 27 ffnd โŠข ( ๐œ‘ โ†’ ( 1r โ€˜ ๐‘† ) Fn ๐ท )
29 ovexd โŠข ( ๐œ‘ โ†’ ( โ„•0 โ†‘m ๐ผ ) โˆˆ V )
30 2 29 rabexd โŠข ( ๐œ‘ โ†’ ๐ท โˆˆ V )
31 inidm โŠข ( ๐ท โˆฉ ๐ท ) = ๐ท
32 fvconst2g โŠข ( ( ๐‘‹ โˆˆ ๐พ โˆง ๐‘ฆ โˆˆ ๐ท ) โ†’ ( ( ๐ท ร— { ๐‘‹ } ) โ€˜ ๐‘ฆ ) = ๐‘‹ )
33 8 32 sylan โŠข ( ( ๐œ‘ โˆง ๐‘ฆ โˆˆ ๐ท ) โ†’ ( ( ๐ท ร— { ๐‘‹ } ) โ€˜ ๐‘ฆ ) = ๐‘‹ )
34 eqid โŠข ( 1r โ€˜ ๐‘… ) = ( 1r โ€˜ ๐‘… )
35 1 6 7 2 3 34 16 psr1 โŠข ( ๐œ‘ โ†’ ( 1r โ€˜ ๐‘† ) = ( ๐‘‘ โˆˆ ๐ท โ†ฆ if ( ๐‘‘ = ( ๐ผ ร— { 0 } ) , ( 1r โ€˜ ๐‘… ) , 0 ) ) )
36 35 adantr โŠข ( ( ๐œ‘ โˆง ๐‘ฆ โˆˆ ๐ท ) โ†’ ( 1r โ€˜ ๐‘† ) = ( ๐‘‘ โˆˆ ๐ท โ†ฆ if ( ๐‘‘ = ( ๐ผ ร— { 0 } ) , ( 1r โ€˜ ๐‘… ) , 0 ) ) )
37 36 fveq1d โŠข ( ( ๐œ‘ โˆง ๐‘ฆ โˆˆ ๐ท ) โ†’ ( ( 1r โ€˜ ๐‘† ) โ€˜ ๐‘ฆ ) = ( ( ๐‘‘ โˆˆ ๐ท โ†ฆ if ( ๐‘‘ = ( ๐ผ ร— { 0 } ) , ( 1r โ€˜ ๐‘… ) , 0 ) ) โ€˜ ๐‘ฆ ) )
38 eqeq1 โŠข ( ๐‘‘ = ๐‘ฆ โ†’ ( ๐‘‘ = ( ๐ผ ร— { 0 } ) โ†” ๐‘ฆ = ( ๐ผ ร— { 0 } ) ) )
39 38 ifbid โŠข ( ๐‘‘ = ๐‘ฆ โ†’ if ( ๐‘‘ = ( ๐ผ ร— { 0 } ) , ( 1r โ€˜ ๐‘… ) , 0 ) = if ( ๐‘ฆ = ( ๐ผ ร— { 0 } ) , ( 1r โ€˜ ๐‘… ) , 0 ) )
40 eqid โŠข ( ๐‘‘ โˆˆ ๐ท โ†ฆ if ( ๐‘‘ = ( ๐ผ ร— { 0 } ) , ( 1r โ€˜ ๐‘… ) , 0 ) ) = ( ๐‘‘ โˆˆ ๐ท โ†ฆ if ( ๐‘‘ = ( ๐ผ ร— { 0 } ) , ( 1r โ€˜ ๐‘… ) , 0 ) )
41 fvex โŠข ( 1r โ€˜ ๐‘… ) โˆˆ V
42 3 fvexi โŠข 0 โˆˆ V
43 41 42 ifex โŠข if ( ๐‘ฆ = ( ๐ผ ร— { 0 } ) , ( 1r โ€˜ ๐‘… ) , 0 ) โˆˆ V
44 39 40 43 fvmpt โŠข ( ๐‘ฆ โˆˆ ๐ท โ†’ ( ( ๐‘‘ โˆˆ ๐ท โ†ฆ if ( ๐‘‘ = ( ๐ผ ร— { 0 } ) , ( 1r โ€˜ ๐‘… ) , 0 ) ) โ€˜ ๐‘ฆ ) = if ( ๐‘ฆ = ( ๐ผ ร— { 0 } ) , ( 1r โ€˜ ๐‘… ) , 0 ) )
45 44 adantl โŠข ( ( ๐œ‘ โˆง ๐‘ฆ โˆˆ ๐ท ) โ†’ ( ( ๐‘‘ โˆˆ ๐ท โ†ฆ if ( ๐‘‘ = ( ๐ผ ร— { 0 } ) , ( 1r โ€˜ ๐‘… ) , 0 ) ) โ€˜ ๐‘ฆ ) = if ( ๐‘ฆ = ( ๐ผ ร— { 0 } ) , ( 1r โ€˜ ๐‘… ) , 0 ) )
46 37 45 eqtrd โŠข ( ( ๐œ‘ โˆง ๐‘ฆ โˆˆ ๐ท ) โ†’ ( ( 1r โ€˜ ๐‘† ) โ€˜ ๐‘ฆ ) = if ( ๐‘ฆ = ( ๐ผ ร— { 0 } ) , ( 1r โ€˜ ๐‘… ) , 0 ) )
47 26 28 30 30 31 33 46 offval โŠข ( ๐œ‘ โ†’ ( ( ๐ท ร— { ๐‘‹ } ) โˆ˜f ( .r โ€˜ ๐‘… ) ( 1r โ€˜ ๐‘† ) ) = ( ๐‘ฆ โˆˆ ๐ท โ†ฆ ( ๐‘‹ ( .r โ€˜ ๐‘… ) if ( ๐‘ฆ = ( ๐ผ ร— { 0 } ) , ( 1r โ€˜ ๐‘… ) , 0 ) ) ) )
48 ovif2 โŠข ( ๐‘‹ ( .r โ€˜ ๐‘… ) if ( ๐‘ฆ = ( ๐ผ ร— { 0 } ) , ( 1r โ€˜ ๐‘… ) , 0 ) ) = if ( ๐‘ฆ = ( ๐ผ ร— { 0 } ) , ( ๐‘‹ ( .r โ€˜ ๐‘… ) ( 1r โ€˜ ๐‘… ) ) , ( ๐‘‹ ( .r โ€˜ ๐‘… ) 0 ) )
49 4 20 34 7 8 ringridmd โŠข ( ๐œ‘ โ†’ ( ๐‘‹ ( .r โ€˜ ๐‘… ) ( 1r โ€˜ ๐‘… ) ) = ๐‘‹ )
50 4 20 3 7 8 ringrzd โŠข ( ๐œ‘ โ†’ ( ๐‘‹ ( .r โ€˜ ๐‘… ) 0 ) = 0 )
51 49 50 ifeq12d โŠข ( ๐œ‘ โ†’ if ( ๐‘ฆ = ( ๐ผ ร— { 0 } ) , ( ๐‘‹ ( .r โ€˜ ๐‘… ) ( 1r โ€˜ ๐‘… ) ) , ( ๐‘‹ ( .r โ€˜ ๐‘… ) 0 ) ) = if ( ๐‘ฆ = ( ๐ผ ร— { 0 } ) , ๐‘‹ , 0 ) )
52 48 51 eqtrid โŠข ( ๐œ‘ โ†’ ( ๐‘‹ ( .r โ€˜ ๐‘… ) if ( ๐‘ฆ = ( ๐ผ ร— { 0 } ) , ( 1r โ€˜ ๐‘… ) , 0 ) ) = if ( ๐‘ฆ = ( ๐ผ ร— { 0 } ) , ๐‘‹ , 0 ) )
53 52 mpteq2dv โŠข ( ๐œ‘ โ†’ ( ๐‘ฆ โˆˆ ๐ท โ†ฆ ( ๐‘‹ ( .r โ€˜ ๐‘… ) if ( ๐‘ฆ = ( ๐ผ ร— { 0 } ) , ( 1r โ€˜ ๐‘… ) , 0 ) ) ) = ( ๐‘ฆ โˆˆ ๐ท โ†ฆ if ( ๐‘ฆ = ( ๐ผ ร— { 0 } ) , ๐‘‹ , 0 ) ) )
54 47 53 eqtrd โŠข ( ๐œ‘ โ†’ ( ( ๐ท ร— { ๐‘‹ } ) โˆ˜f ( .r โ€˜ ๐‘… ) ( 1r โ€˜ ๐‘† ) ) = ( ๐‘ฆ โˆˆ ๐ท โ†ฆ if ( ๐‘ฆ = ( ๐ผ ร— { 0 } ) , ๐‘‹ , 0 ) ) )
55 18 24 54 3eqtrd โŠข ( ๐œ‘ โ†’ ( ๐ด โ€˜ ๐‘‹ ) = ( ๐‘ฆ โˆˆ ๐ท โ†ฆ if ( ๐‘ฆ = ( ๐ผ ร— { 0 } ) , ๐‘‹ , 0 ) ) )