coe1tmfv2

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

	Ref	Expression
Hypotheses	coe1tm.z	⊢ 0 = ( 0_g ‘ 𝑅 )
	coe1tm.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	coe1tm.p	⊢ 𝑃 = ( Poly₁ ‘ 𝑅 )
	coe1tm.x	⊢ 𝑋 = ( var₁ ‘ 𝑅 )
	coe1tm.m	⊢ · = ( ·_𝑠 ‘ 𝑃 )
	coe1tm.n	⊢ 𝑁 = ( mulGrp ‘ 𝑃 )
	coe1tm.e	⊢ ↑ = ( ._g ‘ 𝑁 )
	coe1tmfv2.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	coe1tmfv2.c	⊢ ( 𝜑 → 𝐶 ∈ 𝐾 )
	coe1tmfv2.d	⊢ ( 𝜑 → 𝐷 ∈ ℕ₀ )
	coe1tmfv2.f	⊢ ( 𝜑 → 𝐹 ∈ ℕ₀ )
	coe1tmfv2.q	⊢ ( 𝜑 → 𝐷 ≠ 𝐹 )
Assertion	coe1tmfv2	⊢ ( 𝜑 → ( ( coe₁ ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ 𝐹 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		coe1tm.z	⊢ 0 = ( 0_g ‘ 𝑅 )
2		coe1tm.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
3		coe1tm.p	⊢ 𝑃 = ( Poly₁ ‘ 𝑅 )
4		coe1tm.x	⊢ 𝑋 = ( var₁ ‘ 𝑅 )
5		coe1tm.m	⊢ · = ( ·_𝑠 ‘ 𝑃 )
6		coe1tm.n	⊢ 𝑁 = ( mulGrp ‘ 𝑃 )
7		coe1tm.e	⊢ ↑ = ( ._g ‘ 𝑁 )
8		coe1tmfv2.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
9		coe1tmfv2.c	⊢ ( 𝜑 → 𝐶 ∈ 𝐾 )
10		coe1tmfv2.d	⊢ ( 𝜑 → 𝐷 ∈ ℕ₀ )
11		coe1tmfv2.f	⊢ ( 𝜑 → 𝐹 ∈ ℕ₀ )
12		coe1tmfv2.q	⊢ ( 𝜑 → 𝐷 ≠ 𝐹 )
13	1 2 3 4 5 6 7	coe1tm	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀ ) → ( coe₁ ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) = ( 𝑥 ∈ ℕ₀ ↦ if ( 𝑥 = 𝐷 , 𝐶 , 0 ) ) )
14	8 9 10 13	syl3anc	⊢ ( 𝜑 → ( coe₁ ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) = ( 𝑥 ∈ ℕ₀ ↦ if ( 𝑥 = 𝐷 , 𝐶 , 0 ) ) )
15	14	fveq1d	⊢ ( 𝜑 → ( ( coe₁ ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ 𝐹 ) = ( ( 𝑥 ∈ ℕ₀ ↦ if ( 𝑥 = 𝐷 , 𝐶 , 0 ) ) ‘ 𝐹 ) )
16		eqid	⊢ ( 𝑥 ∈ ℕ₀ ↦ if ( 𝑥 = 𝐷 , 𝐶 , 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	⊢ ( 𝜑 → ( ( 𝑥 ∈ ℕ₀ ↦ if ( 𝑥 = 𝐷 , 𝐶 , 0 ) ) ‘ 𝐹 ) = if ( 𝐹 = 𝐷 , 𝐶 , 0 ) )
23	12	necomd	⊢ ( 𝜑 → 𝐹 ≠ 𝐷 )
24	23	neneqd	⊢ ( 𝜑 → ¬ 𝐹 = 𝐷 )
25	24	iffalsed	⊢ ( 𝜑 → if ( 𝐹 = 𝐷 , 𝐶 , 0 ) = 0 )
26	15 22 25	3eqtrd	⊢ ( 𝜑 → ( ( coe₁ ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ‘ 𝐹 ) = 0 )

Metamath Proof Explorer

Theorem coe1tmfv2

Proof