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

Metamath Proof Explorer

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 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ 𝐷 ) = 𝐶 )