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