Theorem psrvsca

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

	Ref	Expression
Hypotheses	psrvsca.s	$$⊢S=I\mathrm{mPwSer}R$$
	psrvsca.n	$$⊢\underset{\dot{}}{\bullet }={\cdot }_S$$
	psrvsca.k	$$⊢K={\mathrm{Base}}_R$$
	psrvsca.b	$$⊢B={\mathrm{Base}}_S$$
	psrvsca.m	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	psrvsca.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
	psrvsca.x	$$⊢\phi \to X\in K$$
	psrvsca.y	$$⊢\phi \to F\in B$$
Assertion	psrvsca	$$⊢\phi \to X\underset{\dot{}}{\bullet }F=\left(D\times \left\{X\right\}\right){\underset{\dot{}}{·}}_{f}F$$

Proof

Step	Hyp	Ref	Expression
1		psrvsca.s	$$⊢S=I\mathrm{mPwSer}R$$
2		psrvsca.n	$$⊢\underset{\dot{}}{\bullet }={\cdot }_S$$
3		psrvsca.k	$$⊢K={\mathrm{Base}}_R$$
4		psrvsca.b	$$⊢B={\mathrm{Base}}_S$$
5		psrvsca.m	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
6		psrvsca.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
7		psrvsca.x	$$⊢\phi \to X\in K$$
8		psrvsca.y	$$⊢\phi \to F\in B$$
9		sneq	$$⊢x=X\to \left\{x\right\}=\left\{X\right\}$$
10	9	xpeq2d	$$⊢x=X\to D\times \left\{x\right\}=D\times \left\{X\right\}$$
11	10	oveq1d	$$⊢x=X\to \left(D\times \left\{x\right\}\right){\underset{\dot{}}{·}}_{f}f=\left(D\times \left\{X\right\}\right){\underset{\dot{}}{·}}_{f}f$$
12		oveq2	$$⊢f=F\to \left(D\times \left\{X\right\}\right){\underset{\dot{}}{·}}_{f}f=\left(D\times \left\{X\right\}\right){\underset{\dot{}}{·}}_{f}F$$
13	1 2 3 4 5 6	psrvscafval	$$⊢\underset{\dot{}}{\bullet }=\left(x\in K,f\in B⟼\left(D\times \left\{x\right\}\right){\underset{\dot{}}{·}}_{f}f\right)$$
14		ovex	$$⊢\left(D\times \left\{X\right\}\right){\underset{\dot{}}{·}}_{f}F\in \mathrm{V}$$
15	11 12 13 14	ovmpo	$$⊢\left(X\in K\wedge F\in B\right)\to X\underset{\dot{}}{\bullet }F=\left(D\times \left\{X\right\}\right){\underset{\dot{}}{·}}_{f}F$$
16	7 8 15	syl2anc	$$⊢\phi \to X\underset{\dot{}}{\bullet }F=\left(D\times \left\{X\right\}\right){\underset{\dot{}}{·}}_{f}F$$