Metamath Proof Explorer


Theorem pserval

Description: Value of the function G that gives the sequence of monomials of a power series. (Contributed by Mario Carneiro, 26-Feb-2015)

Ref Expression
Hypothesis pser.g โŠข ๐บ = ( ๐‘ฅ โˆˆ โ„‚ โ†ฆ ( ๐‘› โˆˆ โ„•0 โ†ฆ ( ( ๐ด โ€˜ ๐‘› ) ยท ( ๐‘ฅ โ†‘ ๐‘› ) ) ) )
Assertion pserval ( ๐‘‹ โˆˆ โ„‚ โ†’ ( ๐บ โ€˜ ๐‘‹ ) = ( ๐‘š โˆˆ โ„•0 โ†ฆ ( ( ๐ด โ€˜ ๐‘š ) ยท ( ๐‘‹ โ†‘ ๐‘š ) ) ) )

Proof

Step Hyp Ref Expression
1 pser.g โŠข ๐บ = ( ๐‘ฅ โˆˆ โ„‚ โ†ฆ ( ๐‘› โˆˆ โ„•0 โ†ฆ ( ( ๐ด โ€˜ ๐‘› ) ยท ( ๐‘ฅ โ†‘ ๐‘› ) ) ) )
2 oveq1 โŠข ( ๐‘ฆ = ๐‘‹ โ†’ ( ๐‘ฆ โ†‘ ๐‘š ) = ( ๐‘‹ โ†‘ ๐‘š ) )
3 2 oveq2d โŠข ( ๐‘ฆ = ๐‘‹ โ†’ ( ( ๐ด โ€˜ ๐‘š ) ยท ( ๐‘ฆ โ†‘ ๐‘š ) ) = ( ( ๐ด โ€˜ ๐‘š ) ยท ( ๐‘‹ โ†‘ ๐‘š ) ) )
4 3 mpteq2dv โŠข ( ๐‘ฆ = ๐‘‹ โ†’ ( ๐‘š โˆˆ โ„•0 โ†ฆ ( ( ๐ด โ€˜ ๐‘š ) ยท ( ๐‘ฆ โ†‘ ๐‘š ) ) ) = ( ๐‘š โˆˆ โ„•0 โ†ฆ ( ( ๐ด โ€˜ ๐‘š ) ยท ( ๐‘‹ โ†‘ ๐‘š ) ) ) )
5 fveq2 โŠข ( ๐‘› = ๐‘š โ†’ ( ๐ด โ€˜ ๐‘› ) = ( ๐ด โ€˜ ๐‘š ) )
6 oveq2 โŠข ( ๐‘› = ๐‘š โ†’ ( ๐‘ฅ โ†‘ ๐‘› ) = ( ๐‘ฅ โ†‘ ๐‘š ) )
7 5 6 oveq12d โŠข ( ๐‘› = ๐‘š โ†’ ( ( ๐ด โ€˜ ๐‘› ) ยท ( ๐‘ฅ โ†‘ ๐‘› ) ) = ( ( ๐ด โ€˜ ๐‘š ) ยท ( ๐‘ฅ โ†‘ ๐‘š ) ) )
8 7 cbvmptv โŠข ( ๐‘› โˆˆ โ„•0 โ†ฆ ( ( ๐ด โ€˜ ๐‘› ) ยท ( ๐‘ฅ โ†‘ ๐‘› ) ) ) = ( ๐‘š โˆˆ โ„•0 โ†ฆ ( ( ๐ด โ€˜ ๐‘š ) ยท ( ๐‘ฅ โ†‘ ๐‘š ) ) )
9 oveq1 โŠข ( ๐‘ฅ = ๐‘ฆ โ†’ ( ๐‘ฅ โ†‘ ๐‘š ) = ( ๐‘ฆ โ†‘ ๐‘š ) )
10 9 oveq2d โŠข ( ๐‘ฅ = ๐‘ฆ โ†’ ( ( ๐ด โ€˜ ๐‘š ) ยท ( ๐‘ฅ โ†‘ ๐‘š ) ) = ( ( ๐ด โ€˜ ๐‘š ) ยท ( ๐‘ฆ โ†‘ ๐‘š ) ) )
11 10 mpteq2dv โŠข ( ๐‘ฅ = ๐‘ฆ โ†’ ( ๐‘š โˆˆ โ„•0 โ†ฆ ( ( ๐ด โ€˜ ๐‘š ) ยท ( ๐‘ฅ โ†‘ ๐‘š ) ) ) = ( ๐‘š โˆˆ โ„•0 โ†ฆ ( ( ๐ด โ€˜ ๐‘š ) ยท ( ๐‘ฆ โ†‘ ๐‘š ) ) ) )
12 8 11 eqtrid โŠข ( ๐‘ฅ = ๐‘ฆ โ†’ ( ๐‘› โˆˆ โ„•0 โ†ฆ ( ( ๐ด โ€˜ ๐‘› ) ยท ( ๐‘ฅ โ†‘ ๐‘› ) ) ) = ( ๐‘š โˆˆ โ„•0 โ†ฆ ( ( ๐ด โ€˜ ๐‘š ) ยท ( ๐‘ฆ โ†‘ ๐‘š ) ) ) )
13 12 cbvmptv โŠข ( ๐‘ฅ โˆˆ โ„‚ โ†ฆ ( ๐‘› โˆˆ โ„•0 โ†ฆ ( ( ๐ด โ€˜ ๐‘› ) ยท ( ๐‘ฅ โ†‘ ๐‘› ) ) ) ) = ( ๐‘ฆ โˆˆ โ„‚ โ†ฆ ( ๐‘š โˆˆ โ„•0 โ†ฆ ( ( ๐ด โ€˜ ๐‘š ) ยท ( ๐‘ฆ โ†‘ ๐‘š ) ) ) )
14 1 13 eqtri โŠข ๐บ = ( ๐‘ฆ โˆˆ โ„‚ โ†ฆ ( ๐‘š โˆˆ โ„•0 โ†ฆ ( ( ๐ด โ€˜ ๐‘š ) ยท ( ๐‘ฆ โ†‘ ๐‘š ) ) ) )
15 nn0ex โŠข โ„•0 โˆˆ V
16 15 mptex โŠข ( ๐‘š โˆˆ โ„•0 โ†ฆ ( ( ๐ด โ€˜ ๐‘š ) ยท ( ๐‘‹ โ†‘ ๐‘š ) ) ) โˆˆ V
17 4 14 16 fvmpt โŠข ( ๐‘‹ โˆˆ โ„‚ โ†’ ( ๐บ โ€˜ ๐‘‹ ) = ( ๐‘š โˆˆ โ„•0 โ†ฆ ( ( ๐ด โ€˜ ๐‘š ) ยท ( ๐‘‹ โ†‘ ๐‘š ) ) ) )