mplascl

Description: Value of the scalar injection into the polynomial algebra. (Contributed by Stefan O'Rear, 9-Mar-2015)

	Ref	Expression
Hypotheses	mplascl.p	$⊢ P = I mPoly R$
	mplascl.d	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
	mplascl.z	$⊢ \underset{˙}{0} = 0_{R}$
	mplascl.b	$⊢ B = {Base}_{R}$
	mplascl.a	$⊢ A = algSc (P)$
	mplascl.i	$⊢ φ \to I \in W$
	mplascl.r	$⊢ φ \to R \in Ring$
	mplascl.x	$⊢ φ \to X \in B$
Assertion	mplascl	$⊢ φ \to A (X) = (y \in D ⟼ if (y = I \times \{0\}, X, \underset{˙}{0}))$

Step	Hyp	Ref	Expression
1		mplascl.p	$⊢ P = I mPoly R$
2		mplascl.d	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
3		mplascl.z	$⊢ \underset{˙}{0} = 0_{R}$
4		mplascl.b	$⊢ B = {Base}_{R}$
5		mplascl.a	$⊢ A = algSc (P)$
6		mplascl.i	$⊢ φ \to I \in W$
7		mplascl.r	$⊢ φ \to R \in Ring$
8		mplascl.x	$⊢ φ \to X \in B$
9	1 6 7	mplsca	$⊢ φ \to R = Scalar (P)$
10	9	fveq2d	$⊢ φ \to {Base}_{R} = {Base}_{Scalar (P)}$
11	4 10	eqtrid	$⊢ φ \to B = {Base}_{Scalar (P)}$
12	8 11	eleqtrd	$⊢ φ \to X \in {Base}_{Scalar (P)}$
13		eqid	$⊢ Scalar (P) = Scalar (P)$
14		eqid	$⊢ {Base}_{Scalar (P)} = {Base}_{Scalar (P)}$
15		eqid	$⊢ \cdot_{P} = \cdot_{P}$
16		eqid	$⊢ 1_{P} = 1_{P}$
17	5 13 14 15 16	asclval	$⊢ X \in {Base}_{Scalar (P)} \to A (X) = X \cdot_{P} 1_{P}$
18	12 17	syl	$⊢ φ \to A (X) = X \cdot_{P} 1_{P}$
19		eqid	$⊢ 1_{R} = 1_{R}$
20	1 2 3 19 16 6 7	mpl1	$⊢ φ \to 1_{P} = (y \in D ⟼ if (y = I \times \{0\}, 1_{R}, \underset{˙}{0}))$
21	20	oveq2d	$⊢ φ \to X \cdot_{P} 1_{P} = X \cdot_{P} (y \in D ⟼ if (y = I \times \{0\}, 1_{R}, \underset{˙}{0}))$
22	2	psrbag0	$⊢ I \in W \to I \times \{0\} \in D$
23	6 22	syl	$⊢ φ \to I \times \{0\} \in D$
24	1 15 2 19 3 4 6 7 23 8	mplmon2	$⊢ φ \to X \cdot_{P} (y \in D ⟼ if (y = I \times \{0\}, 1_{R}, \underset{˙}{0})) = (y \in D ⟼ if (y = I \times \{0\}, X, \underset{˙}{0}))$
25	18 21 24	3eqtrd	$⊢ φ \to A (X) = (y \in D ⟼ if (y = I \times \{0\}, X, \underset{˙}{0}))$

Metamath Proof Explorer