Theorem psrmulfval

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

	Ref	Expression
Hypotheses	psrmulr.s	$$⊢S=I\mathrm{mPwSer}R$$
	psrmulr.b	$$⊢B={\mathrm{Base}}_S$$
	psrmulr.m	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	psrmulr.t	$$⊢\underset{\dot{}}{\bullet }={\cdot }_S$$
	psrmulr.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
	psrmulfval.i	$$⊢\phi \to F\in B$$
	psrmulfval.r	$$⊢\phi \to G\in B$$
Assertion	psrmulfval	$$⊢\phi \to F\underset{\dot{}}{\bullet }G=\left(k\in D⟼\underset{x\in \left\{y\in D|y{\le }_{f}k\right\}}{{\sum }_R}\left(F\left(x\right)\underset{\dot{}}{·}G\left(k{-}_{f}x\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		psrmulr.s	$$⊢S=I\mathrm{mPwSer}R$$
2		psrmulr.b	$$⊢B={\mathrm{Base}}_S$$
3		psrmulr.m	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
4		psrmulr.t	$$⊢\underset{\dot{}}{\bullet }={\cdot }_S$$
5		psrmulr.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
6		psrmulfval.i	$$⊢\phi \to F\in B$$
7		psrmulfval.r	$$⊢\phi \to G\in B$$
8		fveq1	$$⊢f=F\to f\left(x\right)=F\left(x\right)$$
9		fveq1	$$⊢g=G\to g\left(k{-}_{f}x\right)=G\left(k{-}_{f}x\right)$$
10	8 9	oveqan12d	$$⊢\left(f=F\wedge g=G\right)\to f\left(x\right)\underset{\dot{}}{·}g\left(k{-}_{f}x\right)=F\left(x\right)\underset{\dot{}}{·}G\left(k{-}_{f}x\right)$$
11	10	mpteq2dv	$$⊢\left(f=F\wedge g=G\right)\to \left(x\in \left\{y\in D|y{\le }_{f}k\right\}⟼f\left(x\right)\underset{\dot{}}{·}g\left(k{-}_{f}x\right)\right)=\left(x\in \left\{y\in D|y{\le }_{f}k\right\}⟼F\left(x\right)\underset{\dot{}}{·}G\left(k{-}_{f}x\right)\right)$$
12	11	oveq2d	$$⊢\left(f=F\wedge g=G\right)\to \underset{x\in \left\{y\in D|y{\le }_{f}k\right\}}{{\sum }_R}\left(f\left(x\right)\underset{\dot{}}{·}g\left(k{-}_{f}x\right)\right)=\underset{x\in \left\{y\in D|y{\le }_{f}k\right\}}{{\sum }_R}\left(F\left(x\right)\underset{\dot{}}{·}G\left(k{-}_{f}x\right)\right)$$
13	12	mpteq2dv	$$⊢\left(f=F\wedge g=G\right)\to \left(k\in D⟼\underset{x\in \left\{y\in D|y{\le }_{f}k\right\}}{{\sum }_R}\left(f\left(x\right)\underset{\dot{}}{·}g\left(k{-}_{f}x\right)\right)\right)=\left(k\in D⟼\underset{x\in \left\{y\in D|y{\le }_{f}k\right\}}{{\sum }_R}\left(F\left(x\right)\underset{\dot{}}{·}G\left(k{-}_{f}x\right)\right)\right)$$
14	1 2 3 4 5	psrmulr	$$⊢\underset{\dot{}}{\bullet }=\left(f\in B,g\in B⟼\left(k\in D⟼\underset{x\in \left\{y\in D|y{\le }_{f}k\right\}}{{\sum }_R}\left(f\left(x\right)\underset{\dot{}}{·}g\left(k{-}_{f}x\right)\right)\right)\right)$$
15		ovex	$$⊢{{\mathbb{N}}_0}^I\in \mathrm{V}$$
16	5 15	rabex2	$$⊢D\in \mathrm{V}$$
17	16	mptex	$$⊢\left(k\in D⟼\underset{x\in \left\{y\in D|y{\le }_{f}k\right\}}{{\sum }_R}\left(F\left(x\right)\underset{\dot{}}{·}G\left(k{-}_{f}x\right)\right)\right)\in \mathrm{V}$$
18	13 14 17	ovmpoa	$$⊢\left(F\in B\wedge G\in B\right)\to F\underset{\dot{}}{\bullet }G=\left(k\in D⟼\underset{x\in \left\{y\in D|y{\le }_{f}k\right\}}{{\sum }_R}\left(F\left(x\right)\underset{\dot{}}{·}G\left(k{-}_{f}x\right)\right)\right)$$
19	6 7 18	syl2anc	$$⊢\phi \to F\underset{\dot{}}{\bullet }G=\left(k\in D⟼\underset{x\in \left\{y\in D|y{\le }_{f}k\right\}}{{\sum }_R}\left(F\left(x\right)\underset{\dot{}}{·}G\left(k{-}_{f}x\right)\right)\right)$$