# Metamath Proof Explorer

## Theorem coe1subfv

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

Ref Expression
Hypotheses coe1sub.y ${⊢}{Y}={\mathrm{Poly}}_{1}\left({R}\right)$
coe1sub.b ${⊢}{B}={\mathrm{Base}}_{{Y}}$
coe1sub.p
coe1sub.q ${⊢}{N}={-}_{{R}}$
Assertion coe1subfv

### Proof

Step Hyp Ref Expression
1 coe1sub.y ${⊢}{Y}={\mathrm{Poly}}_{1}\left({R}\right)$
2 coe1sub.b ${⊢}{B}={\mathrm{Base}}_{{Y}}$
3 coe1sub.p
4 coe1sub.q ${⊢}{N}={-}_{{R}}$
5 simpl1 ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {F}\in {B}\wedge {G}\in {B}\right)\wedge {X}\in {ℕ}_{0}\right)\to {R}\in \mathrm{Ring}$
6 1 ply1ring ${⊢}{R}\in \mathrm{Ring}\to {Y}\in \mathrm{Ring}$
7 ringgrp ${⊢}{Y}\in \mathrm{Ring}\to {Y}\in \mathrm{Grp}$
8 6 7 syl ${⊢}{R}\in \mathrm{Ring}\to {Y}\in \mathrm{Grp}$
9 2 3 grpsubcl
10 8 9 syl3an1
12 simpl3 ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {F}\in {B}\wedge {G}\in {B}\right)\wedge {X}\in {ℕ}_{0}\right)\to {G}\in {B}$
13 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}$
14 eqid ${⊢}{+}_{{Y}}={+}_{{Y}}$
15 eqid ${⊢}{+}_{{R}}={+}_{{R}}$
16 1 2 14 15 coe1addfv
17 5 11 12 13 16 syl31anc
18 8 3ad2ant1 ${⊢}\left({R}\in \mathrm{Ring}\wedge {F}\in {B}\wedge {G}\in {B}\right)\to {Y}\in \mathrm{Grp}$
19 18 adantr ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {F}\in {B}\wedge {G}\in {B}\right)\wedge {X}\in {ℕ}_{0}\right)\to {Y}\in \mathrm{Grp}$
20 simpl2 ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {F}\in {B}\wedge {G}\in {B}\right)\wedge {X}\in {ℕ}_{0}\right)\to {F}\in {B}$
21 2 14 3 grpnpcan
22 19 20 12 21 syl3anc
23 22 fveq2d
24 23 fveq1d
25 17 24 eqtr3d
26 ringgrp ${⊢}{R}\in \mathrm{Ring}\to {R}\in \mathrm{Grp}$
27 26 3ad2ant1 ${⊢}\left({R}\in \mathrm{Ring}\wedge {F}\in {B}\wedge {G}\in {B}\right)\to {R}\in \mathrm{Grp}$
28 27 adantr ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {F}\in {B}\wedge {G}\in {B}\right)\wedge {X}\in {ℕ}_{0}\right)\to {R}\in \mathrm{Grp}$
29 eqid ${⊢}{\mathrm{coe}}_{1}\left({F}\right)={\mathrm{coe}}_{1}\left({F}\right)$
30 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
31 29 2 1 30 coe1f ${⊢}{F}\in {B}\to {\mathrm{coe}}_{1}\left({F}\right):{ℕ}_{0}⟶{\mathrm{Base}}_{{R}}$
32 31 3ad2ant2 ${⊢}\left({R}\in \mathrm{Ring}\wedge {F}\in {B}\wedge {G}\in {B}\right)\to {\mathrm{coe}}_{1}\left({F}\right):{ℕ}_{0}⟶{\mathrm{Base}}_{{R}}$
33 32 ffvelrnda ${⊢}\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)\left({X}\right)\in {\mathrm{Base}}_{{R}}$
34 eqid ${⊢}{\mathrm{coe}}_{1}\left({G}\right)={\mathrm{coe}}_{1}\left({G}\right)$
35 34 2 1 30 coe1f ${⊢}{G}\in {B}\to {\mathrm{coe}}_{1}\left({G}\right):{ℕ}_{0}⟶{\mathrm{Base}}_{{R}}$
36 35 3ad2ant3 ${⊢}\left({R}\in \mathrm{Ring}\wedge {F}\in {B}\wedge {G}\in {B}\right)\to {\mathrm{coe}}_{1}\left({G}\right):{ℕ}_{0}⟶{\mathrm{Base}}_{{R}}$
37 36 ffvelrnda ${⊢}\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)\left({X}\right)\in {\mathrm{Base}}_{{R}}$
38 eqid
39 38 2 1 30 coe1f
40 10 39 syl
41 40 ffvelrnda