Theorem psrsca

Description: The scalar field of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014)

	Ref	Expression
Hypotheses	psrsca.s	$$⊢S=I\mathrm{mPwSer}R$$
	psrsca.i	$$⊢\phi \to I\in V$$
	psrsca.r	$$⊢\phi \to R\in W$$
Assertion	psrsca	$$⊢\phi \to R=\mathrm{Scalar}\left(S\right)$$

Proof

Step	Hyp	Ref	Expression
1		psrsca.s	$$⊢S=I\mathrm{mPwSer}R$$
2		psrsca.i	$$⊢\phi \to I\in V$$
3		psrsca.r	$$⊢\phi \to R\in W$$
4		psrvalstr	$$⊢\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{\mathrm{Base}}_S⟩,⟨{+}_{\mathrm{ndx}},{+}_S⟩,⟨{\cdot }_{\mathrm{ndx}},{\cdot }_S⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),R⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in {\mathrm{Base}}_R,f\in {\mathrm{Base}}_S⟼\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⟩$$
5		scaid	$$⊢\mathrm{Scalar}=\mathrm{Slot}\mathrm{Scalar}\left(\mathrm{ndx}\right)$$
6		snsstp1	$$⊢\left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),R⟩\right\}\subseteq \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),R⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in {\mathrm{Base}}_R,f\in {\mathrm{Base}}_S⟼\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\}$$
7		ssun2	$$⊢\left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),R⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in {\mathrm{Base}}_R,f\in {\mathrm{Base}}_S⟼\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\}\subseteq \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{\mathrm{Base}}_S⟩,⟨{+}_{\mathrm{ndx}},{+}_S⟩,⟨{\cdot }_{\mathrm{ndx}},{\cdot }_S⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),R⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in {\mathrm{Base}}_R,f\in {\mathrm{Base}}_S⟼\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\}$$
8	6 7	sstri	$$⊢\left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),R⟩\right\}\subseteq \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{\mathrm{Base}}_S⟩,⟨{+}_{\mathrm{ndx}},{+}_S⟩,⟨{\cdot }_{\mathrm{ndx}},{\cdot }_S⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),R⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in {\mathrm{Base}}_R,f\in {\mathrm{Base}}_S⟼\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\}$$
9	4 5 8	strfv	$$⊢R\in W\to R=\mathrm{Scalar}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{\mathrm{Base}}_S⟩,⟨{+}_{\mathrm{ndx}},{+}_S⟩,⟨{\cdot }_{\mathrm{ndx}},{\cdot }_S⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),R⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in {\mathrm{Base}}_R,f\in {\mathrm{Base}}_S⟼\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)$$
10	3 9	syl	$$⊢\phi \to R=\mathrm{Scalar}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{\mathrm{Base}}_S⟩,⟨{+}_{\mathrm{ndx}},{+}_S⟩,⟨{\cdot }_{\mathrm{ndx}},{\cdot }_S⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),R⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in {\mathrm{Base}}_R,f\in {\mathrm{Base}}_S⟼\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)$$
11		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
12		eqid	$$⊢{+}_R={+}_R$$
13		eqid	$$⊢{\cdot }_R={\cdot }_R$$
14		eqid	$$⊢\mathrm{TopOpen}\left(R\right)=\mathrm{TopOpen}\left(R\right)$$
15		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\}$$
16		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
17	1 11 15 16 2	psrbas	$$⊢\phi \to {\mathrm{Base}}_S={{\mathrm{Base}}_R}^{\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}}$$
18		eqid	$$⊢{+}_S={+}_S$$
19	1 16 12 18	psrplusg	$$⊢{+}_S={{\circ }_f{+}_R\upharpoonright }_{\left({\mathrm{Base}}_S\times {\mathrm{Base}}_S\right)}$$
20		eqid	$$⊢{\cdot }_S={\cdot }_S$$
21	1 16 13 20 15	psrmulr	$$⊢{\cdot }_S=\left(f\in {\mathrm{Base}}_S,z\in {\mathrm{Base}}_S⟼\left(w\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}w\right\}}{{\sum }_R}\left(f\left(x\right){\cdot }_{R}z\left(w{-}_{f}x\right)\right)\right)\right)$$
22		eqid	$$⊢\left(x\in {\mathrm{Base}}_R,f\in {\mathrm{Base}}_S⟼\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 {\mathrm{Base}}_S⟼\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)$$
23		eqidd	$$⊢\phi \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)$$
24	1 11 12 13 14 15 17 19 21 22 23 2 3	psrval	$$⊢\phi \to S=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{\mathrm{Base}}_S⟩,⟨{+}_{\mathrm{ndx}},{+}_S⟩,⟨{\cdot }_{\mathrm{ndx}},{\cdot }_S⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),R⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in {\mathrm{Base}}_R,f\in {\mathrm{Base}}_S⟼\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	24	fveq2d	$$⊢\phi \to \mathrm{Scalar}\left(S\right)=\mathrm{Scalar}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{\mathrm{Base}}_S⟩,⟨{+}_{\mathrm{ndx}},{+}_S⟩,⟨{\cdot }_{\mathrm{ndx}},{\cdot }_S⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),R⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in {\mathrm{Base}}_R,f\in {\mathrm{Base}}_S⟼\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)$$
26	10 25	eqtr4d	$$⊢\phi \to R=\mathrm{Scalar}\left(S\right)$$