# Metamath Proof Explorer

## Theorem ply1plusg

Description: Value of addition in a univariate polynomial ring. (Contributed by Stefan O'Rear, 21-Mar-2015) (Revised by Mario Carneiro, 4-Jul-2015)

Ref Expression
Hypotheses ply1plusg.y ${⊢}{Y}={\mathrm{Poly}}_{1}\left({R}\right)$
ply1plusg.s ${⊢}{S}={1}_{𝑜}\mathrm{mPoly}{R}$
ply1plusg.p
Assertion ply1plusg

### Proof

Step Hyp Ref Expression
1 ply1plusg.y ${⊢}{Y}={\mathrm{Poly}}_{1}\left({R}\right)$
2 ply1plusg.s ${⊢}{S}={1}_{𝑜}\mathrm{mPoly}{R}$
3 ply1plusg.p
4 eqid ${⊢}{1}_{𝑜}\mathrm{mPwSer}{R}={1}_{𝑜}\mathrm{mPwSer}{R}$
5 eqid ${⊢}{+}_{{S}}={+}_{{S}}$
6 2 4 5 mplplusg ${⊢}{+}_{{S}}={+}_{\left({1}_{𝑜}\mathrm{mPwSer}{R}\right)}$
7 eqid ${⊢}{\mathrm{PwSer}}_{1}\left({R}\right)={\mathrm{PwSer}}_{1}\left({R}\right)$
8 eqid ${⊢}{+}_{{\mathrm{PwSer}}_{1}\left({R}\right)}={+}_{{\mathrm{PwSer}}_{1}\left({R}\right)}$
9 7 4 8 psr1plusg ${⊢}{+}_{{\mathrm{PwSer}}_{1}\left({R}\right)}={+}_{\left({1}_{𝑜}\mathrm{mPwSer}{R}\right)}$
10 fvex ${⊢}{\mathrm{Base}}_{\left({1}_{𝑜}\mathrm{mPoly}{R}\right)}\in \mathrm{V}$
11 1 7 ply1val ${⊢}{Y}={\mathrm{PwSer}}_{1}\left({R}\right){↾}_{𝑠}{\mathrm{Base}}_{\left({1}_{𝑜}\mathrm{mPoly}{R}\right)}$
12 11 8 ressplusg ${⊢}{\mathrm{Base}}_{\left({1}_{𝑜}\mathrm{mPoly}{R}\right)}\in \mathrm{V}\to {+}_{{\mathrm{PwSer}}_{1}\left({R}\right)}={+}_{{Y}}$
13 10 12 ax-mp ${⊢}{+}_{{\mathrm{PwSer}}_{1}\left({R}\right)}={+}_{{Y}}$
14 6 9 13 3eqtr2i ${⊢}{+}_{{S}}={+}_{{Y}}$
15 3 14 eqtr4i