Theorem coe1tmfv1

Description: Nonzero coefficient of a polynomial term. (Contributed by Stefan O'Rear, 27-Mar-2015)

	Ref	Expression
Hypotheses	coe1tm.z	⊢ 0 = ( 0g ‘ 𝑅 )
	coe1tm.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	coe1tm.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	coe1tm.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
	coe1tm.m	⊢ · = ( ·𝑠 ‘ 𝑃 )
	coe1tm.n	⊢ 𝑁 = ( mulGrp ‘ 𝑃 )
	coe1tm.e	⊢ ↑ = ( .g ‘ 𝑁 )
Assertion	coe1tmfv1	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ 𝐷 ) = 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		coe1tm.z	⊢ 0 = ( 0g ‘ 𝑅 )
2		coe1tm.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
3		coe1tm.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
4		coe1tm.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
5		coe1tm.m	⊢ · = ( ·𝑠 ‘ 𝑃 )
6		coe1tm.n	⊢ 𝑁 = ( mulGrp ‘ 𝑃 )
7		coe1tm.e	⊢ ↑ = ( .g ‘ 𝑁 )
8	1 2 3 4 5 6 7	coe1tm	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0 ) → ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) = ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 𝐷 , 𝐶 , 0 ) ) )
9	8	fveq1d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ 𝐷 ) = ( ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 𝐷 , 𝐶 , 0 ) ) ‘ 𝐷 ) )
10		eqid	⊢ ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 𝐷 , 𝐶 , 0 ) ) = ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 𝐷 , 𝐶 , 0 ) )
11		iftrue	⊢ ( 𝑥 = 𝐷 → if ( 𝑥 = 𝐷 , 𝐶 , 0 ) = 𝐶 )
12		simp3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0 ) → 𝐷 ∈ ℕ0 )
13		simp2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0 ) → 𝐶 ∈ 𝐾 )
14	10 11 12 13	fvmptd3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0 ) → ( ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 𝐷 , 𝐶 , 0 ) ) ‘ 𝐷 ) = 𝐶 )
15	9 14	eqtrd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ 𝐷 ) = 𝐶 )