# Metamath Proof Explorer

## Theorem psrplusg

Description: The addition operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014) (Revised by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses psrplusg.s ${⊢}{S}={I}\mathrm{mPwSer}{R}$
psrplusg.b ${⊢}{B}={\mathrm{Base}}_{{S}}$
psrplusg.a
psrplusg.p
Assertion psrplusg

### Proof

Step Hyp Ref Expression
1 psrplusg.s ${⊢}{S}={I}\mathrm{mPwSer}{R}$
2 psrplusg.b ${⊢}{B}={\mathrm{Base}}_{{S}}$
3 psrplusg.a
4 psrplusg.p
5 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
6 eqid ${⊢}{\cdot }_{{R}}={\cdot }_{{R}}$
7 eqid ${⊢}\mathrm{TopOpen}\left({R}\right)=\mathrm{TopOpen}\left({R}\right)$
8 eqid ${⊢}\left\{{h}\in \left({{ℕ}_{0}}^{{I}}\right)|{{h}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\right\}=\left\{{h}\in \left({{ℕ}_{0}}^{{I}}\right)|{{h}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\right\}$
9 simpl ${⊢}\left({I}\in \mathrm{V}\wedge {R}\in \mathrm{V}\right)\to {I}\in \mathrm{V}$
10 1 5 8 2 9 psrbas ${⊢}\left({I}\in \mathrm{V}\wedge {R}\in \mathrm{V}\right)\to {B}={{\mathrm{Base}}_{{R}}}^{\left\{{h}\in \left({{ℕ}_{0}}^{{I}}\right)|{{h}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\right\}}$
11 eqid
12 eqid ${⊢}\left({f}\in {B},{g}\in {B}⟼\left({k}\in \left\{{h}\in \left({{ℕ}_{0}}^{{I}}\right)|{{h}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\right\}⟼\underset{{x}\in \left\{{y}\in \left\{{h}\in \left({{ℕ}_{0}}^{{I}}\right)|{{h}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\right\}|{y}{\le }_{f}{k}\right\}}{{\sum }_{{R}}}\left({f}\left({x}\right){\cdot }_{{R}}{g}\left({k}{-}_{f}{x}\right)\right)\right)\right)=\left({f}\in {B},{g}\in {B}⟼\left({k}\in \left\{{h}\in \left({{ℕ}_{0}}^{{I}}\right)|{{h}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\right\}⟼\underset{{x}\in \left\{{y}\in \left\{{h}\in \left({{ℕ}_{0}}^{{I}}\right)|{{h}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\right\}|{y}{\le }_{f}{k}\right\}}{{\sum }_{{R}}}\left({f}\left({x}\right){\cdot }_{{R}}{g}\left({k}{-}_{f}{x}\right)\right)\right)\right)$
13 eqid ${⊢}\left({x}\in {\mathrm{Base}}_{{R}},{f}\in {B}⟼\left(\left\{{h}\in \left({{ℕ}_{0}}^{{I}}\right)|{{h}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\right\}×\left\{{x}\right\}\right){{\cdot }_{{R}}}_{f}{f}\right)=\left({x}\in {\mathrm{Base}}_{{R}},{f}\in {B}⟼\left(\left\{{h}\in \left({{ℕ}_{0}}^{{I}}\right)|{{h}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\right\}×\left\{{x}\right\}\right){{\cdot }_{{R}}}_{f}{f}\right)$
14 eqidd ${⊢}\left({I}\in \mathrm{V}\wedge {R}\in \mathrm{V}\right)\to {\prod }_{𝑡}\left(\left\{{h}\in \left({{ℕ}_{0}}^{{I}}\right)|{{h}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\right\}×\left\{\mathrm{TopOpen}\left({R}\right)\right\}\right)={\prod }_{𝑡}\left(\left\{{h}\in \left({{ℕ}_{0}}^{{I}}\right)|{{h}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\right\}×\left\{\mathrm{TopOpen}\left({R}\right)\right\}\right)$
15 simpr ${⊢}\left({I}\in \mathrm{V}\wedge {R}\in \mathrm{V}\right)\to {R}\in \mathrm{V}$
16 1 5 3 6 7 8 10 11 12 13 14 9 15 psrval
17 16 fveq2d
18 2 fvexi ${⊢}{B}\in \mathrm{V}$
19 18 18 xpex ${⊢}{B}×{B}\in \mathrm{V}$
20 ofexg
21 psrvalstr
22 plusgid ${⊢}{+}_{𝑔}=\mathrm{Slot}{+}_{\mathrm{ndx}}$
23 snsstp2
24 ssun1
25 23 24 sstri
26 21 22 25 strfv
27 19 20 26 mp2b
28 17 4 27 3eqtr4g
29 reldmpsr ${⊢}\mathrm{Rel}\mathrm{dom}\mathrm{mPwSer}$
30 29 ovprc ${⊢}¬\left({I}\in \mathrm{V}\wedge {R}\in \mathrm{V}\right)\to {I}\mathrm{mPwSer}{R}=\varnothing$
31 1 30 syl5eq ${⊢}¬\left({I}\in \mathrm{V}\wedge {R}\in \mathrm{V}\right)\to {S}=\varnothing$
32 31 fveq2d ${⊢}¬\left({I}\in \mathrm{V}\wedge {R}\in \mathrm{V}\right)\to {+}_{{S}}={+}_{\varnothing }$
33 22 str0 ${⊢}\varnothing ={+}_{\varnothing }$
34 32 4 33 3eqtr4g
35 31 fveq2d ${⊢}¬\left({I}\in \mathrm{V}\wedge {R}\in \mathrm{V}\right)\to {\mathrm{Base}}_{{S}}={\mathrm{Base}}_{\varnothing }$
36 base0 ${⊢}\varnothing ={\mathrm{Base}}_{\varnothing }$
37 35 2 36 3eqtr4g ${⊢}¬\left({I}\in \mathrm{V}\wedge {R}\in \mathrm{V}\right)\to {B}=\varnothing$
38 37 xpeq2d ${⊢}¬\left({I}\in \mathrm{V}\wedge {R}\in \mathrm{V}\right)\to {B}×{B}={B}×\varnothing$
39 xp0 ${⊢}{B}×\varnothing =\varnothing$
40 38 39 syl6eq ${⊢}¬\left({I}\in \mathrm{V}\wedge {R}\in \mathrm{V}\right)\to {B}×{B}=\varnothing$
41 40 reseq2d
42 res0
43 41 42 syl6eq
44 34 43 eqtr4d
45 28 44 pm2.61i