Metamath Proof Explorer


Theorem coe1tmfv2

Description: Zero 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𝑁 )
coe1tmfv2.r ( 𝜑𝑅 ∈ Ring )
coe1tmfv2.c ( 𝜑𝐶𝐾 )
coe1tmfv2.d ( 𝜑𝐷 ∈ ℕ0 )
coe1tmfv2.f ( 𝜑𝐹 ∈ ℕ0 )
coe1tmfv2.q ( 𝜑𝐷𝐹 )
Assertion coe1tmfv2 ( 𝜑 → ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ 𝐹 ) = 0 )

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 coe1tmfv2.r ( 𝜑𝑅 ∈ Ring )
9 coe1tmfv2.c ( 𝜑𝐶𝐾 )
10 coe1tmfv2.d ( 𝜑𝐷 ∈ ℕ0 )
11 coe1tmfv2.f ( 𝜑𝐹 ∈ ℕ0 )
12 coe1tmfv2.q ( 𝜑𝐷𝐹 )
13 1 2 3 4 5 6 7 coe1tm ( ( 𝑅 ∈ Ring ∧ 𝐶𝐾𝐷 ∈ ℕ0 ) → ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) = ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 𝐷 , 𝐶 , 0 ) ) )
14 8 9 10 13 syl3anc ( 𝜑 → ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) = ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 𝐷 , 𝐶 , 0 ) ) )
15 14 fveq1d ( 𝜑 → ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ 𝐹 ) = ( ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 𝐷 , 𝐶 , 0 ) ) ‘ 𝐹 ) )
16 eqid ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 𝐷 , 𝐶 , 0 ) ) = ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 𝐷 , 𝐶 , 0 ) )
17 eqeq1 ( 𝑥 = 𝐹 → ( 𝑥 = 𝐷𝐹 = 𝐷 ) )
18 17 ifbid ( 𝑥 = 𝐹 → if ( 𝑥 = 𝐷 , 𝐶 , 0 ) = if ( 𝐹 = 𝐷 , 𝐶 , 0 ) )
19 2 1 ring0cl ( 𝑅 ∈ Ring → 0𝐾 )
20 8 19 syl ( 𝜑0𝐾 )
21 9 20 ifcld ( 𝜑 → if ( 𝐹 = 𝐷 , 𝐶 , 0 ) ∈ 𝐾 )
22 16 18 11 21 fvmptd3 ( 𝜑 → ( ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 𝐷 , 𝐶 , 0 ) ) ‘ 𝐹 ) = if ( 𝐹 = 𝐷 , 𝐶 , 0 ) )
23 12 necomd ( 𝜑𝐹𝐷 )
24 23 neneqd ( 𝜑 → ¬ 𝐹 = 𝐷 )
25 24 iffalsed ( 𝜑 → if ( 𝐹 = 𝐷 , 𝐶 , 0 ) = 0 )
26 15 22 25 3eqtrd ( 𝜑 → ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ 𝐹 ) = 0 )