mplvscaval

Description: The scalar multiplication operation on multivariate polynomials. (Contributed by Mario Carneiro, 9-Jan-2015)

	Ref	Expression
Hypotheses	mplvsca.p	$⊢ P = I mPoly R$
	mplvsca.n	$⊢ \underset{˙}{∙} = \cdot_{P}$
	mplvsca.k	$⊢ K = {Base}_{R}$
	mplvsca.b	$⊢ B = {Base}_{P}$
	mplvsca.m	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	mplvsca.d	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
	mplvsca.x	$⊢ φ \to X \in K$
	mplvsca.f	$⊢ φ \to F \in B$
	mplvscaval.y	$⊢ φ \to Y \in D$
Assertion	mplvscaval	$⊢ φ \to (X \underset{˙}{∙} F) (Y) = X \underset{˙}{\cdot} F (Y)$

Step	Hyp	Ref	Expression
1		mplvsca.p	$⊢ P = I mPoly R$
2		mplvsca.n	$⊢ \underset{˙}{∙} = \cdot_{P}$
3		mplvsca.k	$⊢ K = {Base}_{R}$
4		mplvsca.b	$⊢ B = {Base}_{P}$
5		mplvsca.m	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
6		mplvsca.d	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
7		mplvsca.x	$⊢ φ \to X \in K$
8		mplvsca.f	$⊢ φ \to F \in B$
9		mplvscaval.y	$⊢ φ \to Y \in D$
10	1 2 3 4 5 6 7 8	mplvsca	$⊢ φ \to X \underset{˙}{∙} F = (D \times \{X\}) {\underset{˙}{\cdot}}_{f} F$
11	10	fveq1d	$⊢ φ \to (X \underset{˙}{∙} F) (Y) = ((D \times \{X\}) {\underset{˙}{\cdot}}_{f} F) (Y)$
12		ovex	$⊢ {ℕ_{0}}^{I} \in V$
13	6 12	rabex2	$⊢ D \in V$
14	13	a1i	$⊢ φ \to D \in V$
15		eqid	$⊢ {Base}_{R} = {Base}_{R}$
16	1 15 4 6 8	mplelf	$⊢ φ \to F : D ⟶ {Base}_{R}$
17	16	ffnd	$⊢ φ \to F Fn D$
18		eqidd	$⊢ (φ \land Y \in D) \to F (Y) = F (Y)$
19	14 7 17 18	ofc1	$⊢ (φ \land Y \in D) \to ((D \times \{X\}) {\underset{˙}{\cdot}}_{f} F) (Y) = X \underset{˙}{\cdot} F (Y)$
20	9 19	mpdan	$⊢ φ \to ((D \times \{X\}) {\underset{˙}{\cdot}}_{f} F) (Y) = X \underset{˙}{\cdot} F (Y)$
21	11 20	eqtrd	$⊢ φ \to (X \underset{˙}{∙} F) (Y) = X \underset{˙}{\cdot} F (Y)$

Metamath Proof Explorer