This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mplvsca

Description: The scalar multiplication operation on multivariate polynomials. (Contributed by Mario Carneiro, 9-Jan-2015) (Revised by Mario Carneiro, 2-Oct-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$
	Assertion	mplvsca	$⊢ φ \to X \underset{˙}{∙} F = (D \times \{X\}) {\underset{˙}{\cdot}}_{f} F$

Proof

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		eqid	$⊢ I mPwSer R = I mPwSer R$
10	1 9 2	mplvsca2	$⊢ \underset{˙}{∙} = \cdot_{(I mPwSer R)}$
11		eqid	$⊢ {Base}_{(I mPwSer R)} = {Base}_{(I mPwSer R)}$
12	1 9 4 11	mplbasss	$⊢ B \subseteq {Base}_{(I mPwSer R)}$
13	12 8	sselid	$⊢ φ \to F \in {Base}_{(I mPwSer R)}$
14	9 10 3 11 5 6 7 13	psrvsca	$⊢ φ \to X \underset{˙}{∙} F = (D \times \{X\}) {\underset{˙}{\cdot}}_{f} F$