# Metamath Proof Explorer

## 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({{ℕ}_{0}}^{{I}}\right)|{{h}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\right\}×\left\{{x}\right\}\right){{\cdot }_{{R}}}_{f}{f}\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\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)⟩\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({{ℕ}_{0}}^{{I}}\right)|{{h}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\right\}×\left\{{x}\right\}\right){{\cdot }_{{R}}}_{f}{f}\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\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)⟩\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({{ℕ}_{0}}^{{I}}\right)|{{h}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\right\}×\left\{{x}\right\}\right){{\cdot }_{{R}}}_{f}{f}\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\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)⟩\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({{ℕ}_{0}}^{{I}}\right)|{{h}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\right\}×\left\{{x}\right\}\right){{\cdot }_{{R}}}_{f}{f}\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\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)⟩\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({{ℕ}_{0}}^{{I}}\right)|{{h}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\right\}×\left\{{x}\right\}\right){{\cdot }_{{R}}}_{f}{f}\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\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)⟩\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({{ℕ}_{0}}^{{I}}\right)|{{h}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\right\}×\left\{{x}\right\}\right){{\cdot }_{{R}}}_{f}{f}\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\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)⟩\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({{ℕ}_{0}}^{{I}}\right)|{{h}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\right\}×\left\{{x}\right\}\right){{\cdot }_{{R}}}_{f}{f}\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\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)⟩\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({{ℕ}_{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\}$
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({{ℕ}_{0}}^{{I}}\right)|{{h}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\right\}}$
18 eqid ${⊢}{+}_{{S}}={+}_{{S}}$
19 1 16 12 18 psrplusg ${⊢}{+}_{{S}}={{\circ }_{f}{+}_{{R}}↾}_{\left({\mathrm{Base}}_{{S}}×{\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({{ℕ}_{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}{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({{ℕ}_{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 {\mathrm{Base}}_{{S}}⟼\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)$
23 eqidd ${⊢}{\phi }\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)$
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({{ℕ}_{0}}^{{I}}\right)|{{h}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\right\}×\left\{{x}\right\}\right){{\cdot }_{{R}}}_{f}{f}\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\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)⟩\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({{ℕ}_{0}}^{{I}}\right)|{{h}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\right\}×\left\{{x}\right\}\right){{\cdot }_{{R}}}_{f}{f}\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\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)⟩\right\}\right)$
26 10 25 eqtr4d ${⊢}{\phi }\to {R}=\mathrm{Scalar}\left({S}\right)$