Metamath Proof Explorer

Theorem psrbas

Description: The base set of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014) (Revised by Mario Carneiro, 2-Oct-2015) (Proof shortened by AV, 8-Jul-2019)

Ref Expression
Hypotheses psrbas.s ${⊢}{S}={I}\mathrm{mPwSer}{R}$
psrbas.k ${⊢}{K}={\mathrm{Base}}_{{R}}$
psrbas.d ${⊢}{D}=\left\{{f}\in \left({{ℕ}_{0}}^{{I}}\right)|{{f}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\right\}$
psrbas.b ${⊢}{B}={\mathrm{Base}}_{{S}}$
psrbas.i ${⊢}{\phi }\to {I}\in {V}$
Assertion psrbas ${⊢}{\phi }\to {B}={{K}}^{{D}}$

Proof

Step Hyp Ref Expression
1 psrbas.s ${⊢}{S}={I}\mathrm{mPwSer}{R}$
2 psrbas.k ${⊢}{K}={\mathrm{Base}}_{{R}}$
3 psrbas.d ${⊢}{D}=\left\{{f}\in \left({{ℕ}_{0}}^{{I}}\right)|{{f}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\right\}$
4 psrbas.b ${⊢}{B}={\mathrm{Base}}_{{S}}$
5 psrbas.i ${⊢}{\phi }\to {I}\in {V}$
6 eqid ${⊢}{+}_{{R}}={+}_{{R}}$
7 eqid ${⊢}{\cdot }_{{R}}={\cdot }_{{R}}$
8 eqid ${⊢}\mathrm{TopOpen}\left({R}\right)=\mathrm{TopOpen}\left({R}\right)$
9 eqidd ${⊢}\left({\phi }\wedge {R}\in \mathrm{V}\right)\to {{K}}^{{D}}={{K}}^{{D}}$
10 eqid ${⊢}{{\circ }_{f}{+}_{{R}}↾}_{\left(\left({{K}}^{{D}}\right)×\left({{K}}^{{D}}\right)\right)}={{\circ }_{f}{+}_{{R}}↾}_{\left(\left({{K}}^{{D}}\right)×\left({{K}}^{{D}}\right)\right)}$
11 eqid ${⊢}\left({g}\in \left({{K}}^{{D}}\right),{h}\in \left({{K}}^{{D}}\right)⟼\left({k}\in {D}⟼\underset{{x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}}{{\sum }_{{R}}}\left({g}\left({x}\right){\cdot }_{{R}}{h}\left({k}{-}_{f}{x}\right)\right)\right)\right)=\left({g}\in \left({{K}}^{{D}}\right),{h}\in \left({{K}}^{{D}}\right)⟼\left({k}\in {D}⟼\underset{{x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}}{{\sum }_{{R}}}\left({g}\left({x}\right){\cdot }_{{R}}{h}\left({k}{-}_{f}{x}\right)\right)\right)\right)$
12 eqid ${⊢}\left({x}\in {K},{g}\in \left({{K}}^{{D}}\right)⟼\left({D}×\left\{{x}\right\}\right){{\cdot }_{{R}}}_{f}{g}\right)=\left({x}\in {K},{g}\in \left({{K}}^{{D}}\right)⟼\left({D}×\left\{{x}\right\}\right){{\cdot }_{{R}}}_{f}{g}\right)$
13 eqidd ${⊢}\left({\phi }\wedge {R}\in \mathrm{V}\right)\to {\prod }_{𝑡}\left({D}×\left\{\mathrm{TopOpen}\left({R}\right)\right\}\right)={\prod }_{𝑡}\left({D}×\left\{\mathrm{TopOpen}\left({R}\right)\right\}\right)$
14 5 adantr ${⊢}\left({\phi }\wedge {R}\in \mathrm{V}\right)\to {I}\in {V}$
15 simpr ${⊢}\left({\phi }\wedge {R}\in \mathrm{V}\right)\to {R}\in \mathrm{V}$
16 1 2 6 7 8 3 9 10 11 12 13 14 15 psrval ${⊢}\left({\phi }\wedge {R}\in \mathrm{V}\right)\to {S}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{{K}}^{{D}}⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_{f}{+}_{{R}}↾}_{\left(\left({{K}}^{{D}}\right)×\left({{K}}^{{D}}\right)\right)}⟩,⟨{\cdot }_{\mathrm{ndx}},\left({g}\in \left({{K}}^{{D}}\right),{h}\in \left({{K}}^{{D}}\right)⟼\left({k}\in {D}⟼\underset{{x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}}{{\sum }_{{R}}}\left({g}\left({x}\right){\cdot }_{{R}}{h}\left({k}{-}_{f}{x}\right)\right)\right)\right)⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{R}⟩,⟨{\cdot }_{\mathrm{ndx}},\left({x}\in {K},{g}\in \left({{K}}^{{D}}\right)⟼\left({D}×\left\{{x}\right\}\right){{\cdot }_{{R}}}_{f}{g}\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),{\prod }_{𝑡}\left({D}×\left\{\mathrm{TopOpen}\left({R}\right)\right\}\right)⟩\right\}$
17 16 fveq2d ${⊢}\left({\phi }\wedge {R}\in \mathrm{V}\right)\to {\mathrm{Base}}_{{S}}={\mathrm{Base}}_{\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{{K}}^{{D}}⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_{f}{+}_{{R}}↾}_{\left(\left({{K}}^{{D}}\right)×\left({{K}}^{{D}}\right)\right)}⟩,⟨{\cdot }_{\mathrm{ndx}},\left({g}\in \left({{K}}^{{D}}\right),{h}\in \left({{K}}^{{D}}\right)⟼\left({k}\in {D}⟼\underset{{x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}}{{\sum }_{{R}}}\left({g}\left({x}\right){\cdot }_{{R}}{h}\left({k}{-}_{f}{x}\right)\right)\right)\right)⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{R}⟩,⟨{\cdot }_{\mathrm{ndx}},\left({x}\in {K},{g}\in \left({{K}}^{{D}}\right)⟼\left({D}×\left\{{x}\right\}\right){{\cdot }_{{R}}}_{f}{g}\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),{\prod }_{𝑡}\left({D}×\left\{\mathrm{TopOpen}\left({R}\right)\right\}\right)⟩\right\}\right)}$
18 ovex ${⊢}{{K}}^{{D}}\in \mathrm{V}$
19 psrvalstr ${⊢}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{{K}}^{{D}}⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_{f}{+}_{{R}}↾}_{\left(\left({{K}}^{{D}}\right)×\left({{K}}^{{D}}\right)\right)}⟩,⟨{\cdot }_{\mathrm{ndx}},\left({g}\in \left({{K}}^{{D}}\right),{h}\in \left({{K}}^{{D}}\right)⟼\left({k}\in {D}⟼\underset{{x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}}{{\sum }_{{R}}}\left({g}\left({x}\right){\cdot }_{{R}}{h}\left({k}{-}_{f}{x}\right)\right)\right)\right)⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{R}⟩,⟨{\cdot }_{\mathrm{ndx}},\left({x}\in {K},{g}\in \left({{K}}^{{D}}\right)⟼\left({D}×\left\{{x}\right\}\right){{\cdot }_{{R}}}_{f}{g}\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),{\prod }_{𝑡}\left({D}×\left\{\mathrm{TopOpen}\left({R}\right)\right\}\right)⟩\right\}\right)\mathrm{Struct}⟨1,9⟩$
20 baseid ${⊢}\mathrm{Base}=\mathrm{Slot}{\mathrm{Base}}_{\mathrm{ndx}}$
21 snsstp1 ${⊢}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{{K}}^{{D}}⟩\right\}\subseteq \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{{K}}^{{D}}⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_{f}{+}_{{R}}↾}_{\left(\left({{K}}^{{D}}\right)×\left({{K}}^{{D}}\right)\right)}⟩,⟨{\cdot }_{\mathrm{ndx}},\left({g}\in \left({{K}}^{{D}}\right),{h}\in \left({{K}}^{{D}}\right)⟼\left({k}\in {D}⟼\underset{{x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}}{{\sum }_{{R}}}\left({g}\left({x}\right){\cdot }_{{R}}{h}\left({k}{-}_{f}{x}\right)\right)\right)\right)⟩\right\}$
22 ssun1 ${⊢}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{{K}}^{{D}}⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_{f}{+}_{{R}}↾}_{\left(\left({{K}}^{{D}}\right)×\left({{K}}^{{D}}\right)\right)}⟩,⟨{\cdot }_{\mathrm{ndx}},\left({g}\in \left({{K}}^{{D}}\right),{h}\in \left({{K}}^{{D}}\right)⟼\left({k}\in {D}⟼\underset{{x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}}{{\sum }_{{R}}}\left({g}\left({x}\right){\cdot }_{{R}}{h}\left({k}{-}_{f}{x}\right)\right)\right)\right)⟩\right\}\subseteq \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{{K}}^{{D}}⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_{f}{+}_{{R}}↾}_{\left(\left({{K}}^{{D}}\right)×\left({{K}}^{{D}}\right)\right)}⟩,⟨{\cdot }_{\mathrm{ndx}},\left({g}\in \left({{K}}^{{D}}\right),{h}\in \left({{K}}^{{D}}\right)⟼\left({k}\in {D}⟼\underset{{x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}}{{\sum }_{{R}}}\left({g}\left({x}\right){\cdot }_{{R}}{h}\left({k}{-}_{f}{x}\right)\right)\right)\right)⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{R}⟩,⟨{\cdot }_{\mathrm{ndx}},\left({x}\in {K},{g}\in \left({{K}}^{{D}}\right)⟼\left({D}×\left\{{x}\right\}\right){{\cdot }_{{R}}}_{f}{g}\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),{\prod }_{𝑡}\left({D}×\left\{\mathrm{TopOpen}\left({R}\right)\right\}\right)⟩\right\}$
23 21 22 sstri ${⊢}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{{K}}^{{D}}⟩\right\}\subseteq \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{{K}}^{{D}}⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_{f}{+}_{{R}}↾}_{\left(\left({{K}}^{{D}}\right)×\left({{K}}^{{D}}\right)\right)}⟩,⟨{\cdot }_{\mathrm{ndx}},\left({g}\in \left({{K}}^{{D}}\right),{h}\in \left({{K}}^{{D}}\right)⟼\left({k}\in {D}⟼\underset{{x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}}{{\sum }_{{R}}}\left({g}\left({x}\right){\cdot }_{{R}}{h}\left({k}{-}_{f}{x}\right)\right)\right)\right)⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{R}⟩,⟨{\cdot }_{\mathrm{ndx}},\left({x}\in {K},{g}\in \left({{K}}^{{D}}\right)⟼\left({D}×\left\{{x}\right\}\right){{\cdot }_{{R}}}_{f}{g}\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),{\prod }_{𝑡}\left({D}×\left\{\mathrm{TopOpen}\left({R}\right)\right\}\right)⟩\right\}$
24 19 20 23 strfv ${⊢}{{K}}^{{D}}\in \mathrm{V}\to {{K}}^{{D}}={\mathrm{Base}}_{\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{{K}}^{{D}}⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_{f}{+}_{{R}}↾}_{\left(\left({{K}}^{{D}}\right)×\left({{K}}^{{D}}\right)\right)}⟩,⟨{\cdot }_{\mathrm{ndx}},\left({g}\in \left({{K}}^{{D}}\right),{h}\in \left({{K}}^{{D}}\right)⟼\left({k}\in {D}⟼\underset{{x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}}{{\sum }_{{R}}}\left({g}\left({x}\right){\cdot }_{{R}}{h}\left({k}{-}_{f}{x}\right)\right)\right)\right)⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{R}⟩,⟨{\cdot }_{\mathrm{ndx}},\left({x}\in {K},{g}\in \left({{K}}^{{D}}\right)⟼\left({D}×\left\{{x}\right\}\right){{\cdot }_{{R}}}_{f}{g}\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),{\prod }_{𝑡}\left({D}×\left\{\mathrm{TopOpen}\left({R}\right)\right\}\right)⟩\right\}\right)}$
25 18 24 ax-mp ${⊢}{{K}}^{{D}}={\mathrm{Base}}_{\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{{K}}^{{D}}⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_{f}{+}_{{R}}↾}_{\left(\left({{K}}^{{D}}\right)×\left({{K}}^{{D}}\right)\right)}⟩,⟨{\cdot }_{\mathrm{ndx}},\left({g}\in \left({{K}}^{{D}}\right),{h}\in \left({{K}}^{{D}}\right)⟼\left({k}\in {D}⟼\underset{{x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}}{{\sum }_{{R}}}\left({g}\left({x}\right){\cdot }_{{R}}{h}\left({k}{-}_{f}{x}\right)\right)\right)\right)⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{R}⟩,⟨{\cdot }_{\mathrm{ndx}},\left({x}\in {K},{g}\in \left({{K}}^{{D}}\right)⟼\left({D}×\left\{{x}\right\}\right){{\cdot }_{{R}}}_{f}{g}\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),{\prod }_{𝑡}\left({D}×\left\{\mathrm{TopOpen}\left({R}\right)\right\}\right)⟩\right\}\right)}$
26 17 4 25 3eqtr4g ${⊢}\left({\phi }\wedge {R}\in \mathrm{V}\right)\to {B}={{K}}^{{D}}$
27 reldmpsr ${⊢}\mathrm{Rel}\mathrm{dom}\mathrm{mPwSer}$
28 27 ovprc2 ${⊢}¬{R}\in \mathrm{V}\to {I}\mathrm{mPwSer}{R}=\varnothing$
29 28 adantl ${⊢}\left({\phi }\wedge ¬{R}\in \mathrm{V}\right)\to {I}\mathrm{mPwSer}{R}=\varnothing$
30 1 29 syl5eq ${⊢}\left({\phi }\wedge ¬{R}\in \mathrm{V}\right)\to {S}=\varnothing$
31 30 fveq2d ${⊢}\left({\phi }\wedge ¬{R}\in \mathrm{V}\right)\to {\mathrm{Base}}_{{S}}={\mathrm{Base}}_{\varnothing }$
32 base0 ${⊢}\varnothing ={\mathrm{Base}}_{\varnothing }$
33 31 4 32 3eqtr4g ${⊢}\left({\phi }\wedge ¬{R}\in \mathrm{V}\right)\to {B}=\varnothing$
34 fvprc ${⊢}¬{R}\in \mathrm{V}\to {\mathrm{Base}}_{{R}}=\varnothing$
35 34 adantl ${⊢}\left({\phi }\wedge ¬{R}\in \mathrm{V}\right)\to {\mathrm{Base}}_{{R}}=\varnothing$
36 2 35 syl5eq ${⊢}\left({\phi }\wedge ¬{R}\in \mathrm{V}\right)\to {K}=\varnothing$
37 3 fczpsrbag ${⊢}{I}\in {V}\to \left({x}\in {I}⟼0\right)\in {D}$
38 5 37 syl ${⊢}{\phi }\to \left({x}\in {I}⟼0\right)\in {D}$
39 38 adantr ${⊢}\left({\phi }\wedge ¬{R}\in \mathrm{V}\right)\to \left({x}\in {I}⟼0\right)\in {D}$
40 39 ne0d ${⊢}\left({\phi }\wedge ¬{R}\in \mathrm{V}\right)\to {D}\ne \varnothing$
41 2 fvexi ${⊢}{K}\in \mathrm{V}$
42 ovex ${⊢}{{ℕ}_{0}}^{{I}}\in \mathrm{V}$
43 3 42 rabex2 ${⊢}{D}\in \mathrm{V}$
44 41 43 map0 ${⊢}{{K}}^{{D}}=\varnothing ↔\left({K}=\varnothing \wedge {D}\ne \varnothing \right)$
45 36 40 44 sylanbrc ${⊢}\left({\phi }\wedge ¬{R}\in \mathrm{V}\right)\to {{K}}^{{D}}=\varnothing$
46 33 45 eqtr4d ${⊢}\left({\phi }\wedge ¬{R}\in \mathrm{V}\right)\to {B}={{K}}^{{D}}$
47 26 46 pm2.61dan ${⊢}{\phi }\to {B}={{K}}^{{D}}$