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

Metamath Proof Explorer

Theorem coe1ae0

Description: The coefficient vector of a univariate polynomial is 0 almost everywhere. (Contributed by AV, 19-Oct-2019)

		Ref	Expression
	Hypotheses	coe1ae0.a	⊢ 𝐴 = ( coe₁ ‘ 𝐹 )
		coe1ae0.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
		coe1ae0.p	⊢ 𝑃 = ( Poly₁ ‘ 𝑅 )
		coe1ae0.z	⊢ 0 = ( 0_g ‘ 𝑅 )
	Assertion	coe1ae0	⊢ ( 𝐹 ∈ 𝐵 → ∃ 𝑠 ∈ ℕ₀ ∀ 𝑛 ∈ ℕ₀ ( 𝑠 < 𝑛 → ( 𝐴 ‘ 𝑛 ) = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		coe1ae0.a	⊢ 𝐴 = ( coe₁ ‘ 𝐹 )
2		coe1ae0.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
3		coe1ae0.p	⊢ 𝑃 = ( Poly₁ ‘ 𝑅 )
4		coe1ae0.z	⊢ 0 = ( 0_g ‘ 𝑅 )
5		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
6	1 2 3 4 5	coe1fsupp	⊢ ( 𝐹 ∈ 𝐵 → 𝐴 ∈ { 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∣ 𝑎 finSupp 0 } )
7		breq1	⊢ ( 𝑎 = 𝐴 → ( 𝑎 finSupp 0 ↔ 𝐴 finSupp 0 ) )
8	7	elrab	⊢ ( 𝐴 ∈ { 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∣ 𝑎 finSupp 0 } ↔ ( 𝐴 ∈ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∧ 𝐴 finSupp 0 ) )
9	4	fvexi	⊢ 0 ∈ V
10	9	a1i	⊢ ( 𝐹 ∈ 𝐵 → 0 ∈ V )
11		fsuppmapnn0ub	⊢ ( ( 𝐴 ∈ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∧ 0 ∈ V ) → ( 𝐴 finSupp 0 → ∃ 𝑠 ∈ ℕ₀ ∀ 𝑛 ∈ ℕ₀ ( 𝑠 < 𝑛 → ( 𝐴 ‘ 𝑛 ) = 0 ) ) )
12	10 11	sylan2	⊢ ( ( 𝐴 ∈ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∧ 𝐹 ∈ 𝐵 ) → ( 𝐴 finSupp 0 → ∃ 𝑠 ∈ ℕ₀ ∀ 𝑛 ∈ ℕ₀ ( 𝑠 < 𝑛 → ( 𝐴 ‘ 𝑛 ) = 0 ) ) )
13	12	impancom	⊢ ( ( 𝐴 ∈ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∧ 𝐴 finSupp 0 ) → ( 𝐹 ∈ 𝐵 → ∃ 𝑠 ∈ ℕ₀ ∀ 𝑛 ∈ ℕ₀ ( 𝑠 < 𝑛 → ( 𝐴 ‘ 𝑛 ) = 0 ) ) )
14	8 13	sylbi	⊢ ( 𝐴 ∈ { 𝑎 ∈ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∣ 𝑎 finSupp 0 } → ( 𝐹 ∈ 𝐵 → ∃ 𝑠 ∈ ℕ₀ ∀ 𝑛 ∈ ℕ₀ ( 𝑠 < 𝑛 → ( 𝐴 ‘ 𝑛 ) = 0 ) ) )
15	6 14	mpcom	⊢ ( 𝐹 ∈ 𝐵 → ∃ 𝑠 ∈ ℕ₀ ∀ 𝑛 ∈ ℕ₀ ( 𝑠 < 𝑛 → ( 𝐴 ‘ 𝑛 ) = 0 ) )