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 mPwSer R$
	psrvsca.n	$⊢ \underset{˙}{∙} = \cdot_{S}$
	psrvsca.k	$⊢ K = {Base}_{R}$
	psrvsca.b	$⊢ B = {Base}_{S}$
	psrvsca.m	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	psrvsca.d	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
	psrvsca.x	$⊢ φ \to X \in K$
	psrvsca.y	$⊢ φ \to F \in B$
Assertion	psrvsca	$⊢ φ \to X \underset{˙}{∙} F = (D \times \{X\}) {\underset{˙}{\cdot}}_{f} F$

Step	Hyp	Ref	Expression
1		psrvsca.s	$⊢ S = I mPwSer R$
2		psrvsca.n	$⊢ \underset{˙}{∙} = \cdot_{S}$
3		psrvsca.k	$⊢ K = {Base}_{R}$
4		psrvsca.b	$⊢ B = {Base}_{S}$
5		psrvsca.m	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
6		psrvsca.d	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
7		psrvsca.x	$⊢ φ \to X \in K$
8		psrvsca.y	$⊢ φ \to F \in B$
9		sneq	$⊢ x = X \to \{x\} = \{X\}$
10	9	xpeq2d	$⊢ x = X \to D \times \{x\} = D \times \{X\}$
11	10	oveq1d	$⊢ x = X \to (D \times \{x\}) {\underset{˙}{\cdot}}_{f} f = (D \times \{X\}) {\underset{˙}{\cdot}}_{f} f$
12		oveq2	$⊢ f = F \to (D \times \{X\}) {\underset{˙}{\cdot}}_{f} f = (D \times \{X\}) {\underset{˙}{\cdot}}_{f} F$
13	1 2 3 4 5 6	psrvscafval	$⊢ \underset{˙}{∙} = (x \in K, f \in B ⟼ (D \times \{x\}) {\underset{˙}{\cdot}}_{f} f)$
14		ovex	$⊢ (D \times \{X\}) {\underset{˙}{\cdot}}_{f} F \in V$
15	11 12 13 14	ovmpo	$⊢ (X \in K \land F \in B) \to X \underset{˙}{∙} F = (D \times \{X\}) {\underset{˙}{\cdot}}_{f} F$
16	7 8 15	syl2anc	$⊢ φ \to X \underset{˙}{∙} F = (D \times \{X\}) {\underset{˙}{\cdot}}_{f} F$

Metamath Proof Explorer