Theorem psrvscaval

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$$
	psrvscaval.y	$$⊢\phi \to Y\in D$$
Assertion	psrvscaval	$$⊢\phi \to \left(X\underset{\dot{}}{\bullet }F\right)\left(Y\right)=X\underset{\dot{}}{·}F\left(Y\right)$$

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		psrvscaval.y	$$⊢\phi \to Y\in D$$
10	1 2 3 4 5 6 7 8	psrvsca	$$⊢\phi \to X\underset{\dot{}}{\bullet }F=\left(D\times \left\{X\right\}\right){\underset{\dot{}}{·}}_{f}F$$
11	10	fveq1d	$$⊢\phi \to \left(X\underset{\dot{}}{\bullet }F\right)\left(Y\right)=\left(\left(D\times \left\{X\right\}\right){\underset{\dot{}}{·}}_{f}F\right)\left(Y\right)$$
12		ovex	$$⊢{{\mathbb{N}}_0}^I\in \mathrm{V}$$
13	6 12	rabex2	$$⊢D\in \mathrm{V}$$
14	13	a1i	$$⊢\phi \to D\in \mathrm{V}$$
15	1 3 6 4 8	psrelbas	$$⊢\phi \to F:D⟶K$$
16	15	ffnd	$$⊢\phi \to FFnD$$
17		eqidd	$$⊢\left(\phi \wedge Y\in D\right)\to F\left(Y\right)=F\left(Y\right)$$
18	14 7 16 17	ofc1	$$⊢\left(\phi \wedge Y\in D\right)\to \left(\left(D\times \left\{X\right\}\right){\underset{\dot{}}{·}}_{f}F\right)\left(Y\right)=X\underset{\dot{}}{·}F\left(Y\right)$$
19	9 18	mpdan	$$⊢\phi \to \left(\left(D\times \left\{X\right\}\right){\underset{\dot{}}{·}}_{f}F\right)\left(Y\right)=X\underset{\dot{}}{·}F\left(Y\right)$$
20	11 19	eqtrd	$$⊢\phi \to \left(X\underset{\dot{}}{\bullet }F\right)\left(Y\right)=X\underset{\dot{}}{·}F\left(Y\right)$$