# Metamath Proof Explorer

## Theorem coe1z

Description: The coefficient vector of 0. (Contributed by Stefan O'Rear, 23-Mar-2015)

Ref Expression
Hypotheses coe1z.p $⊢ P = Poly 1 ⁡ R$
coe1z.z
coe1z.y $⊢ Y = 0 R$
Assertion coe1z

### Proof

Step Hyp Ref Expression
1 coe1z.p $⊢ P = Poly 1 ⁡ R$
2 coe1z.z
3 coe1z.y $⊢ Y = 0 R$
4 fconst6g $⊢ a ∈ ℕ 0 → 1 𝑜 × a : 1 𝑜 ⟶ ℕ 0$
5 4 adantl $⊢ R ∈ Ring ∧ a ∈ ℕ 0 → 1 𝑜 × a : 1 𝑜 ⟶ ℕ 0$
6 nn0ex $⊢ ℕ 0 ∈ V$
7 1oex $⊢ 1 𝑜 ∈ V$
8 6 7 elmap $⊢ 1 𝑜 × a ∈ ℕ 0 1 𝑜 ↔ 1 𝑜 × a : 1 𝑜 ⟶ ℕ 0$
9 5 8 sylibr $⊢ R ∈ Ring ∧ a ∈ ℕ 0 → 1 𝑜 × a ∈ ℕ 0 1 𝑜$
10 eqidd $⊢ R ∈ Ring → a ∈ ℕ 0 ⟼ 1 𝑜 × a = a ∈ ℕ 0 ⟼ 1 𝑜 × a$
11 eqid $⊢ 1 𝑜 mPoly R = 1 𝑜 mPoly R$
12 psr1baslem $⊢ ℕ 0 1 𝑜 = c ∈ ℕ 0 1 𝑜 | c -1 ℕ ∈ Fin$
13 11 1 2 ply1mpl0
14 1on $⊢ 1 𝑜 ∈ On$
15 14 a1i $⊢ R ∈ Ring → 1 𝑜 ∈ On$
16 ringgrp $⊢ R ∈ Ring → R ∈ Grp$
17 11 12 3 13 15 16 mpl0
18 fconstmpt $⊢ ℕ 0 1 𝑜 × Y = b ∈ ℕ 0 1 𝑜 ⟼ Y$
19 17 18 eqtrdi
20 eqidd $⊢ b = 1 𝑜 × a → Y = Y$
21 9 10 19 20 fmptco
22 1 ply1ring $⊢ R ∈ Ring → P ∈ Ring$
23 eqid $⊢ Base P = Base P$
24 23 2 ring0cl
25 eqid
26 eqid $⊢ a ∈ ℕ 0 ⟼ 1 𝑜 × a = a ∈ ℕ 0 ⟼ 1 𝑜 × a$
27 25 23 1 26 coe1fval2
28 22 24 27 3syl
29 fconstmpt $⊢ ℕ 0 × Y = a ∈ ℕ 0 ⟼ Y$
30 29 a1i $⊢ R ∈ Ring → ℕ 0 × Y = a ∈ ℕ 0 ⟼ Y$
31 21 28 30 3eqtr4d