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	$$⊢\underset{\dot{}}{+}={+}_R$$
	psrplusg.p	$$⊢\underset{\dot{}}{✚}={+}_S$$
Assertion	psrplusg	$$⊢\underset{\dot{}}{✚}={{\circ }_f\underset{\dot{}}{+}\upharpoonright }_{\left(B\times B\right)}$$

Proof

Step	Hyp	Ref	Expression
1		psrplusg.s	$$⊢S=I\mathrm{mPwSer}R$$
2		psrplusg.b	$$⊢B={\mathrm{Base}}_S$$
3		psrplusg.a	$$⊢\underset{\dot{}}{+}={+}_R$$
4		psrplusg.p	$$⊢\underset{\dot{}}{✚}={+}_S$$
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({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\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({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}}$$
11		eqid	$$⊢{{\circ }_f\underset{\dot{}}{+}\upharpoonright }_{\left(B\times B\right)}={{\circ }_f\underset{\dot{}}{+}\upharpoonright }_{\left(B\times B\right)}$$
12		eqid	$$⊢\left(f\in B,g\in B⟼\left(k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼\underset{x\in \left\{y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\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({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼\underset{x\in \left\{y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\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({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\times \left\{x\right\}\right){{\cdot }_R}_{f}f\right)=\left(x\in {\mathrm{Base}}_R,f\in B⟼\left(\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\times \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({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\times \left\{\mathrm{TopOpen}\left(R\right)\right\}\right)={\prod }_{𝑡}\left(\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\times \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	$$⊢\left(I\in \mathrm{V}\wedge R\in \mathrm{V}\right)\to S=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_f\underset{\dot{}}{+}\upharpoonright }_{\left(B\times B\right)}⟩,⟨{\cdot }_{\mathrm{ndx}},\left(f\in B,g\in B⟼\left(k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼\underset{x\in \left\{y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\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)⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),R⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in {\mathrm{Base}}_R,f\in B⟼\left(\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\times \left\{x\right\}\right){{\cdot }_R}_{f}f\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),{\prod }_{𝑡}\left(\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\times \left\{\mathrm{TopOpen}\left(R\right)\right\}\right)⟩\right\}$$
17	16	fveq2d	$$⊢\left(I\in \mathrm{V}\wedge R\in \mathrm{V}\right)\to {+}_S={+}_{\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_f\underset{\dot{}}{+}\upharpoonright }_{\left(B\times B\right)}⟩,⟨{\cdot }_{\mathrm{ndx}},\left(f\in B,g\in B⟼\left(k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼\underset{x\in \left\{y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\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)⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),R⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in {\mathrm{Base}}_R,f\in B⟼\left(\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\times \left\{x\right\}\right){{\cdot }_R}_{f}f\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),{\prod }_{𝑡}\left(\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\times \left\{\mathrm{TopOpen}\left(R\right)\right\}\right)⟩\right\}\right)}$$
18	2	fvexi	$$⊢B\in \mathrm{V}$$
19	18 18	xpex	$$⊢B\times B\in \mathrm{V}$$
20		ofexg	$$⊢B\times B\in \mathrm{V}\to {{\circ }_f\underset{\dot{}}{+}\upharpoonright }_{\left(B\times B\right)}\in \mathrm{V}$$
21		psrvalstr	$$⊢\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_f\underset{\dot{}}{+}\upharpoonright }_{\left(B\times B\right)}⟩,⟨{\cdot }_{\mathrm{ndx}},\left(f\in B,g\in B⟼\left(k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼\underset{x\in \left\{y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\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)⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),R⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in {\mathrm{Base}}_R,f\in B⟼\left(\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\times \left\{x\right\}\right){{\cdot }_R}_{f}f\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),{\prod }_{𝑡}\left(\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\times \left\{\mathrm{TopOpen}\left(R\right)\right\}\right)⟩\right\}\right)\mathrm{Struct}⟨1,9⟩$$
22		plusgid	$$⊢{+}_{𝑔}=\mathrm{Slot}{+}_{\mathrm{ndx}}$$
23		snsstp2	$$⊢\left\{⟨{+}_{\mathrm{ndx}},{{\circ }_f\underset{\dot{}}{+}\upharpoonright }_{\left(B\times B\right)}⟩\right\}\subseteq \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_f\underset{\dot{}}{+}\upharpoonright }_{\left(B\times B\right)}⟩,⟨{\cdot }_{\mathrm{ndx}},\left(f\in B,g\in B⟼\left(k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼\underset{x\in \left\{y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\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)⟩\right\}$$
24		ssun1	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_f\underset{\dot{}}{+}\upharpoonright }_{\left(B\times B\right)}⟩,⟨{\cdot }_{\mathrm{ndx}},\left(f\in B,g\in B⟼\left(k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼\underset{x\in \left\{y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\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)⟩\right\}\subseteq \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_f\underset{\dot{}}{+}\upharpoonright }_{\left(B\times B\right)}⟩,⟨{\cdot }_{\mathrm{ndx}},\left(f\in B,g\in B⟼\left(k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼\underset{x\in \left\{y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\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)⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),R⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in {\mathrm{Base}}_R,f\in B⟼\left(\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\times \left\{x\right\}\right){{\cdot }_R}_{f}f\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),{\prod }_{𝑡}\left(\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\times \left\{\mathrm{TopOpen}\left(R\right)\right\}\right)⟩\right\}$$
25	23 24	sstri	$$⊢\left\{⟨{+}_{\mathrm{ndx}},{{\circ }_f\underset{\dot{}}{+}\upharpoonright }_{\left(B\times B\right)}⟩\right\}\subseteq \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_f\underset{\dot{}}{+}\upharpoonright }_{\left(B\times B\right)}⟩,⟨{\cdot }_{\mathrm{ndx}},\left(f\in B,g\in B⟼\left(k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼\underset{x\in \left\{y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\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)⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),R⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in {\mathrm{Base}}_R,f\in B⟼\left(\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\times \left\{x\right\}\right){{\cdot }_R}_{f}f\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),{\prod }_{𝑡}\left(\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\times \left\{\mathrm{TopOpen}\left(R\right)\right\}\right)⟩\right\}$$
26	21 22 25	strfv	$$⊢{{\circ }_f\underset{\dot{}}{+}\upharpoonright }_{\left(B\times B\right)}\in \mathrm{V}\to {{\circ }_f\underset{\dot{}}{+}\upharpoonright }_{\left(B\times B\right)}={+}_{\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_f\underset{\dot{}}{+}\upharpoonright }_{\left(B\times B\right)}⟩,⟨{\cdot }_{\mathrm{ndx}},\left(f\in B,g\in B⟼\left(k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼\underset{x\in \left\{y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\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)⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),R⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in {\mathrm{Base}}_R,f\in B⟼\left(\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\times \left\{x\right\}\right){{\cdot }_R}_{f}f\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),{\prod }_{𝑡}\left(\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\times \left\{\mathrm{TopOpen}\left(R\right)\right\}\right)⟩\right\}\right)}$$
27	19 20 26	mp2b	$$⊢{{\circ }_f\underset{\dot{}}{+}\upharpoonright }_{\left(B\times B\right)}={+}_{\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_f\underset{\dot{}}{+}\upharpoonright }_{\left(B\times B\right)}⟩,⟨{\cdot }_{\mathrm{ndx}},\left(f\in B,g\in B⟼\left(k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼\underset{x\in \left\{y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\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)⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),R⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in {\mathrm{Base}}_R,f\in B⟼\left(\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\times \left\{x\right\}\right){{\cdot }_R}_{f}f\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),{\prod }_{𝑡}\left(\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\times \left\{\mathrm{TopOpen}\left(R\right)\right\}\right)⟩\right\}\right)}$$
28	17 4 27	3eqtr4g	$$⊢\left(I\in \mathrm{V}\wedge R\in \mathrm{V}\right)\to \underset{\dot{}}{✚}={{\circ }_f\underset{\dot{}}{+}\upharpoonright }_{\left(B\times B\right)}$$
29		reldmpsr	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{mPwSer}$$
30	29	ovprc	$$⊢\neg \left(I\in \mathrm{V}\wedge R\in \mathrm{V}\right)\to I\mathrm{mPwSer}R=\varnothing$$
31	1 30	syl5eq	$$⊢\neg \left(I\in \mathrm{V}\wedge R\in \mathrm{V}\right)\to S=\varnothing$$
32	31	fveq2d	$$⊢\neg \left(I\in \mathrm{V}\wedge R\in \mathrm{V}\right)\to {+}_S={+}_{\varnothing }$$
33	22	str0	$$⊢\varnothing ={+}_{\varnothing }$$
34	32 4 33	3eqtr4g	$$⊢\neg \left(I\in \mathrm{V}\wedge R\in \mathrm{V}\right)\to \underset{\dot{}}{✚}=\varnothing$$
35	31	fveq2d	$$⊢\neg \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	$$⊢\neg \left(I\in \mathrm{V}\wedge R\in \mathrm{V}\right)\to B=\varnothing$$
38	37	xpeq2d	$$⊢\neg \left(I\in \mathrm{V}\wedge R\in \mathrm{V}\right)\to B\times B=B\times \varnothing$$
39		xp0	$$⊢B\times \varnothing =\varnothing$$
40	38 39	eqtrdi	$$⊢\neg \left(I\in \mathrm{V}\wedge R\in \mathrm{V}\right)\to B\times B=\varnothing$$
41	40	reseq2d	$$⊢\neg \left(I\in \mathrm{V}\wedge R\in \mathrm{V}\right)\to {{\circ }_f\underset{\dot{}}{+}\upharpoonright }_{\left(B\times B\right)}={{\circ }_f\underset{\dot{}}{+}\upharpoonright }_{\varnothing }$$
42		res0	$$⊢{{\circ }_f\underset{\dot{}}{+}\upharpoonright }_{\varnothing }=\varnothing$$
43	41 42	eqtrdi	$$⊢\neg \left(I\in \mathrm{V}\wedge R\in \mathrm{V}\right)\to {{\circ }_f\underset{\dot{}}{+}\upharpoonright }_{\left(B\times B\right)}=\varnothing$$
44	34 43	eqtr4d	$$⊢\neg \left(I\in \mathrm{V}\wedge R\in \mathrm{V}\right)\to \underset{\dot{}}{✚}={{\circ }_f\underset{\dot{}}{+}\upharpoonright }_{\left(B\times B\right)}$$
45	28 44	pm2.61i	$$⊢\underset{\dot{}}{✚}={{\circ }_f\underset{\dot{}}{+}\upharpoonright }_{\left(B\times B\right)}$$