# Metamath Proof Explorer

Description: A particular coefficient of an addition. (Contributed by Stefan O'Rear, 23-Mar-2015)

Ref Expression
Hypotheses coe1add.y ${⊢}{Y}={\mathrm{Poly}}_{1}\left({R}\right)$
coe1add.b ${⊢}{B}={\mathrm{Base}}_{{Y}}$

### Proof

Step Hyp Ref Expression
1 coe1add.y ${⊢}{Y}={\mathrm{Poly}}_{1}\left({R}\right)$
2 coe1add.b ${⊢}{B}={\mathrm{Base}}_{{Y}}$
5 1 2 3 4 coe1add
7 6 fveq1d
8 eqid ${⊢}{\mathrm{coe}}_{1}\left({F}\right)={\mathrm{coe}}_{1}\left({F}\right)$
9 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
10 8 2 1 9 coe1f ${⊢}{F}\in {B}\to {\mathrm{coe}}_{1}\left({F}\right):{ℕ}_{0}⟶{\mathrm{Base}}_{{R}}$
11 10 ffnd ${⊢}{F}\in {B}\to {\mathrm{coe}}_{1}\left({F}\right)Fn{ℕ}_{0}$
12 11 3ad2ant2 ${⊢}\left({R}\in \mathrm{Ring}\wedge {F}\in {B}\wedge {G}\in {B}\right)\to {\mathrm{coe}}_{1}\left({F}\right)Fn{ℕ}_{0}$
13 12 adantr ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {F}\in {B}\wedge {G}\in {B}\right)\wedge {X}\in {ℕ}_{0}\right)\to {\mathrm{coe}}_{1}\left({F}\right)Fn{ℕ}_{0}$
14 eqid ${⊢}{\mathrm{coe}}_{1}\left({G}\right)={\mathrm{coe}}_{1}\left({G}\right)$
15 14 2 1 9 coe1f ${⊢}{G}\in {B}\to {\mathrm{coe}}_{1}\left({G}\right):{ℕ}_{0}⟶{\mathrm{Base}}_{{R}}$
16 15 ffnd ${⊢}{G}\in {B}\to {\mathrm{coe}}_{1}\left({G}\right)Fn{ℕ}_{0}$
17 16 3ad2ant3 ${⊢}\left({R}\in \mathrm{Ring}\wedge {F}\in {B}\wedge {G}\in {B}\right)\to {\mathrm{coe}}_{1}\left({G}\right)Fn{ℕ}_{0}$
18 17 adantr ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {F}\in {B}\wedge {G}\in {B}\right)\wedge {X}\in {ℕ}_{0}\right)\to {\mathrm{coe}}_{1}\left({G}\right)Fn{ℕ}_{0}$
19 nn0ex ${⊢}{ℕ}_{0}\in \mathrm{V}$
20 19 a1i ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {F}\in {B}\wedge {G}\in {B}\right)\wedge {X}\in {ℕ}_{0}\right)\to {ℕ}_{0}\in \mathrm{V}$
21 simpr ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {F}\in {B}\wedge {G}\in {B}\right)\wedge {X}\in {ℕ}_{0}\right)\to {X}\in {ℕ}_{0}$
22 fnfvof
23 13 18 20 21 22 syl22anc
24 7 23 eqtrd