Theorem psrmulval

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$$
	psrmulval.r	$$⊢\phi \to X\in D$$
Assertion	psrmulval	$$⊢\phi \to \left(F\underset{\dot{}}{\bullet }G\right)\left(X\right)=\underset{k\in \left\{y\in D|y{\le }_{f}X\right\}}{{\sum }_R}\left(F\left(k\right)\underset{\dot{}}{·}G\left(X{-}_{f}k\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		psrmulval.r	$$⊢\phi \to X\in D$$
9	1 2 3 4 5 6 7	psrmulfval	$$⊢\phi \to F\underset{\dot{}}{\bullet }G=\left(x\in D⟼\underset{k\in \left\{y\in D|y{\le }_{f}x\right\}}{{\sum }_R}\left(F\left(k\right)\underset{\dot{}}{·}G\left(x{-}_{f}k\right)\right)\right)$$
10	9	fveq1d	$$⊢\phi \to \left(F\underset{\dot{}}{\bullet }G\right)\left(X\right)=\left(x\in D⟼\underset{k\in \left\{y\in D|y{\le }_{f}x\right\}}{{\sum }_R}\left(F\left(k\right)\underset{\dot{}}{·}G\left(x{-}_{f}k\right)\right)\right)\left(X\right)$$
11		breq2	$$⊢x=X\to \left(y{\le }_{f}x\leftrightarrow y{\le }_{f}X\right)$$
12	11	rabbidv	$$⊢x=X\to \left\{y\in D|y{\le }_{f}x\right\}=\left\{y\in D|y{\le }_{f}X\right\}$$
13		fvoveq1	$$⊢x=X\to G\left(x{-}_{f}k\right)=G\left(X{-}_{f}k\right)$$
14	13	oveq2d	$$⊢x=X\to F\left(k\right)\underset{\dot{}}{·}G\left(x{-}_{f}k\right)=F\left(k\right)\underset{\dot{}}{·}G\left(X{-}_{f}k\right)$$
15	12 14	mpteq12dv	$$⊢x=X\to \left(k\in \left\{y\in D|y{\le }_{f}x\right\}⟼F\left(k\right)\underset{\dot{}}{·}G\left(x{-}_{f}k\right)\right)=\left(k\in \left\{y\in D|y{\le }_{f}X\right\}⟼F\left(k\right)\underset{\dot{}}{·}G\left(X{-}_{f}k\right)\right)$$
16	15	oveq2d	$$⊢x=X\to \underset{k\in \left\{y\in D|y{\le }_{f}x\right\}}{{\sum }_R}\left(F\left(k\right)\underset{\dot{}}{·}G\left(x{-}_{f}k\right)\right)=\underset{k\in \left\{y\in D|y{\le }_{f}X\right\}}{{\sum }_R}\left(F\left(k\right)\underset{\dot{}}{·}G\left(X{-}_{f}k\right)\right)$$
17		eqid	$$⊢\left(x\in D⟼\underset{k\in \left\{y\in D|y{\le }_{f}x\right\}}{{\sum }_R}\left(F\left(k\right)\underset{\dot{}}{·}G\left(x{-}_{f}k\right)\right)\right)=\left(x\in D⟼\underset{k\in \left\{y\in D|y{\le }_{f}x\right\}}{{\sum }_R}\left(F\left(k\right)\underset{\dot{}}{·}G\left(x{-}_{f}k\right)\right)\right)$$
18		ovex	$$⊢\underset{k\in \left\{y\in D|y{\le }_{f}X\right\}}{{\sum }_R}\left(F\left(k\right)\underset{\dot{}}{·}G\left(X{-}_{f}k\right)\right)\in \mathrm{V}$$
19	16 17 18	fvmpt	$$⊢X\in D\to \left(x\in D⟼\underset{k\in \left\{y\in D|y{\le }_{f}x\right\}}{{\sum }_R}\left(F\left(k\right)\underset{\dot{}}{·}G\left(x{-}_{f}k\right)\right)\right)\left(X\right)=\underset{k\in \left\{y\in D|y{\le }_{f}X\right\}}{{\sum }_R}\left(F\left(k\right)\underset{\dot{}}{·}G\left(X{-}_{f}k\right)\right)$$
20	8 19	syl	$$⊢\phi \to \left(x\in D⟼\underset{k\in \left\{y\in D|y{\le }_{f}x\right\}}{{\sum }_R}\left(F\left(k\right)\underset{\dot{}}{·}G\left(x{-}_{f}k\right)\right)\right)\left(X\right)=\underset{k\in \left\{y\in D|y{\le }_{f}X\right\}}{{\sum }_R}\left(F\left(k\right)\underset{\dot{}}{·}G\left(X{-}_{f}k\right)\right)$$
21	10 20	eqtrd	$$⊢\phi \to \left(F\underset{\dot{}}{\bullet }G\right)\left(X\right)=\underset{k\in \left\{y\in D|y{\le }_{f}X\right\}}{{\sum }_R}\left(F\left(k\right)\underset{\dot{}}{·}G\left(X{-}_{f}k\right)\right)$$