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

Metamath Proof Explorer

Theorem coe1id

Description: Coefficient vector of the unit polynomial. (Contributed by AV, 9-Aug-2019)

Ref Expression
Hypotheses coe1id.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
coe1id.i ⊢ 𝐼 = ( 1r ‘ 𝑃 )
coe1id.0 ⊢ 0 = ( 0g ‘ 𝑅 )
coe1id.1 ⊢ 1 = ( 1r ‘ 𝑅 )
Assertion coe1id ( 𝑅 ∈ Ring → ( coe1 ‘ 𝐼 ) = ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 0 , 1 , 0 ) ) )

Proof

Step Hyp Ref Expression
1 coe1id.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 coe1id.i ⊢ 𝐼 = ( 1r ‘ 𝑃 )
3 coe1id.0 ⊢ 0 = ( 0g ‘ 𝑅 )
4 coe1id.1 ⊢ 1 = ( 1r ‘ 𝑅 )
5 eqid ⊢ ( algSc ‘ 𝑃 ) = ( algSc ‘ 𝑃 )
6 1 5 4 2 ply1scl1 ⊢ ( 𝑅 ∈ Ring → ( ( algSc ‘ 𝑃 ) ‘ 1 ) = 𝐼 )
7 6 eqcomd ⊢ ( 𝑅 ∈ Ring → 𝐼 = ( ( algSc ‘ 𝑃 ) ‘ 1 ) )
8 7 fveq2d ⊢ ( 𝑅 ∈ Ring → ( coe1 ‘ 𝐼 ) = ( coe1 ‘ ( ( algSc ‘ 𝑃 ) ‘ 1 ) ) )
9 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
10 9 4 ringidcl ⊢ ( 𝑅 ∈ Ring → 1 ∈ ( Base ‘ 𝑅 ) )
11 1 5 9 3 coe1scl ⊢ ( ( 𝑅 ∈ Ring ∧ 1 ∈ ( Base ‘ 𝑅 ) ) → ( coe1 ‘ ( ( algSc ‘ 𝑃 ) ‘ 1 ) ) = ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 0 , 1 , 0 ) ) )
12 10 11 mpdan ⊢ ( 𝑅 ∈ Ring → ( coe1 ‘ ( ( algSc ‘ 𝑃 ) ‘ 1 ) ) = ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 0 , 1 , 0 ) ) )
13 8 12 eqtrd ⊢ ( 𝑅 ∈ Ring → ( coe1 ‘ 𝐼 ) = ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 0 , 1 , 0 ) ) )