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

Metamath Proof Explorer

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 ) ) )