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

Metamath Proof Explorer

Theorem coe0

Description: The coefficients of the zero polynomial are zero. (Contributed by Mario Carneiro, 22-Jul-2014)

Ref Expression
Assertion coe0 ( coeff ‘ 0𝑝 ) = ( ℕ0 × { 0 } )

Proof

Step Hyp Ref Expression
1 0cnd ⊢ ( ⊤ → 0 ∈ ℂ )
2 ssid ⊢ ℂ ⊆ ℂ
3 ply0 ⊢ ( ℂ ⊆ ℂ → 0𝑝 ∈ ( Poly ‘ ℂ ) )
4 2 3 ax-mp ⊢ 0𝑝 ∈ ( Poly ‘ ℂ )
5 coemulc ⊢ ( ( 0 ∈ ℂ ∧ 0𝑝 ∈ ( Poly ‘ ℂ ) ) → ( coeff ‘ ( ( ℂ × { 0 } ) ∘f · 0𝑝 ) ) = ( ( ℕ0 × { 0 } ) ∘f · ( coeff ‘ 0𝑝 ) ) )
6 1 4 5 sylancl ⊢ ( ⊤ → ( coeff ‘ ( ( ℂ × { 0 } ) ∘f · 0𝑝 ) ) = ( ( ℕ0 × { 0 } ) ∘f · ( coeff ‘ 0𝑝 ) ) )
7 cnex ⊢ ℂ ∈ V
8 7 a1i ⊢ ( ⊤ → ℂ ∈ V )
9 plyf ⊢ ( 0𝑝 ∈ ( Poly ‘ ℂ ) → 0𝑝 : ℂ ⟶ ℂ )
10 4 9 mp1i ⊢ ( ⊤ → 0𝑝 : ℂ ⟶ ℂ )
11 mul02 ⊢ ( 𝑥 ∈ ℂ → ( 0 · 𝑥 ) = 0 )
12 11 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( 0 · 𝑥 ) = 0 )
13 8 10 1 1 12 caofid2 ⊢ ( ⊤ → ( ( ℂ × { 0 } ) ∘f · 0𝑝 ) = ( ℂ × { 0 } ) )
14 df-0p ⊢ 0𝑝 = ( ℂ × { 0 } )
15 13 14 eqtr4di ⊢ ( ⊤ → ( ( ℂ × { 0 } ) ∘f · 0𝑝 ) = 0𝑝 )
16 15 fveq2d ⊢ ( ⊤ → ( coeff ‘ ( ( ℂ × { 0 } ) ∘f · 0𝑝 ) ) = ( coeff ‘ 0𝑝 ) )
17 nn0ex ⊢ ℕ0 ∈ V
18 17 a1i ⊢ ( ⊤ → ℕ0 ∈ V )
19 eqid ⊢ ( coeff ‘ 0𝑝 ) = ( coeff ‘ 0𝑝 )
20 19 coef3 ⊢ ( 0𝑝 ∈ ( Poly ‘ ℂ ) → ( coeff ‘ 0𝑝 ) : ℕ0 ⟶ ℂ )
21 4 20 mp1i ⊢ ( ⊤ → ( coeff ‘ 0𝑝 ) : ℕ0 ⟶ ℂ )
22 18 21 1 1 12 caofid2 ⊢ ( ⊤ → ( ( ℕ0 × { 0 } ) ∘f · ( coeff ‘ 0𝑝 ) ) = ( ℕ0 × { 0 } ) )
23 6 16 22 3eqtr3d ⊢ ( ⊤ → ( coeff ‘ 0𝑝 ) = ( ℕ0 × { 0 } ) )
24 23 mptru ⊢ ( coeff ‘ 0𝑝 ) = ( ℕ0 × { 0 } )