mpl1

Description: The identity element of the ring of polynomials. (Contributed by Mario Carneiro, 10-Jan-2015)

	Ref	Expression
Hypotheses	mpl1.p	$⊢ P = I mPoly R$
	mpl1.d	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
	mpl1.z	$⊢ \underset{˙}{0} = 0_{R}$
	mpl1.o	$⊢ \underset{˙}{1} = 1_{R}$
	mpl1.u	$⊢ U = 1_{P}$
	mpl1.i	$⊢ φ \to I \in W$
	mpl1.r	$⊢ φ \to R \in Ring$
Assertion	mpl1	$⊢ φ \to U = (x \in D ⟼ if (x = I \times \{0\}, \underset{˙}{1}, \underset{˙}{0}))$

Step	Hyp	Ref	Expression
1		mpl1.p	$⊢ P = I mPoly R$
2		mpl1.d	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
3		mpl1.z	$⊢ \underset{˙}{0} = 0_{R}$
4		mpl1.o	$⊢ \underset{˙}{1} = 1_{R}$
5		mpl1.u	$⊢ U = 1_{P}$
6		mpl1.i	$⊢ φ \to I \in W$
7		mpl1.r	$⊢ φ \to R \in Ring$
8		eqid	$⊢ I mPwSer R = I mPwSer R$
9		eqid	$⊢ {Base}_{P} = {Base}_{P}$
10	8 1 9 6 7	mplsubrg	$⊢ φ \to {Base}_{P} \in SubRing (I mPwSer R)$
11	1 8 9	mplval2	$⊢ P = (I mPwSer R) ↾_{𝑠} {Base}_{P}$
12		eqid	$⊢ 1_{(I mPwSer R)} = 1_{(I mPwSer R)}$
13	11 12	subrg1	$⊢ {Base}_{P} \in SubRing (I mPwSer R) \to 1_{(I mPwSer R)} = 1_{P}$
14	10 13	syl	$⊢ φ \to 1_{(I mPwSer R)} = 1_{P}$
15	8 6 7 2 3 4 12	psr1	$⊢ φ \to 1_{(I mPwSer R)} = (x \in D ⟼ if (x = I \times \{0\}, \underset{˙}{1}, \underset{˙}{0}))$
16	14 15	eqtr3d	$⊢ φ \to 1_{P} = (x \in D ⟼ if (x = I \times \{0\}, \underset{˙}{1}, \underset{˙}{0}))$
17	5 16	eqtrid	$⊢ φ \to U = (x \in D ⟼ if (x = I \times \{0\}, \underset{˙}{1}, \underset{˙}{0}))$

Metamath Proof Explorer