Theorem mpl1

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

	Ref	Expression
Hypotheses	mpl1.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
	mpl1.d	⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
	mpl1.z	⊢ 0 = ( 0g ‘ 𝑅 )
	mpl1.o	⊢ 1 = ( 1r ‘ 𝑅 )
	mpl1.u	⊢ 𝑈 = ( 1r ‘ 𝑃 )
	mpl1.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
	mpl1.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
Assertion	mpl1	⊢ ( 𝜑 → 𝑈 = ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = ( 𝐼 × { 0 } ) , 1 , 0 ) ) )

Proof

Step	Hyp	Ref	Expression
1		mpl1.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2		mpl1.d	⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
3		mpl1.z	⊢ 0 = ( 0g ‘ 𝑅 )
4		mpl1.o	⊢ 1 = ( 1r ‘ 𝑅 )
5		mpl1.u	⊢ 𝑈 = ( 1r ‘ 𝑃 )
6		mpl1.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
7		mpl1.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
8		eqid	⊢ ( 𝐼 mPwSer 𝑅 ) = ( 𝐼 mPwSer 𝑅 )
9		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
10	8 1 9 6 7	mplsubrg	⊢ ( 𝜑 → ( Base ‘ 𝑃 ) ∈ ( SubRing ‘ ( 𝐼 mPwSer 𝑅 ) ) )
11	1 8 9	mplval2	⊢ 𝑃 = ( ( 𝐼 mPwSer 𝑅 ) ↾s ( Base ‘ 𝑃 ) )
12		eqid	⊢ ( 1r ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( 1r ‘ ( 𝐼 mPwSer 𝑅 ) )
13	11 12	subrg1	⊢ ( ( Base ‘ 𝑃 ) ∈ ( SubRing ‘ ( 𝐼 mPwSer 𝑅 ) ) → ( 1r ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( 1r ‘ 𝑃 ) )
14	10 13	syl	⊢ ( 𝜑 → ( 1r ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( 1r ‘ 𝑃 ) )
15	8 6 7 2 3 4 12	psr1	⊢ ( 𝜑 → ( 1r ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = ( 𝐼 × { 0 } ) , 1 , 0 ) ) )
16	14 15	eqtr3d	⊢ ( 𝜑 → ( 1r ‘ 𝑃 ) = ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = ( 𝐼 × { 0 } ) , 1 , 0 ) ) )
17	5 16	eqtrid	⊢ ( 𝜑 → 𝑈 = ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = ( 𝐼 × { 0 } ) , 1 , 0 ) ) )