Metamath Proof Explorer

Theorem psrval

Description: Value of the multivariate power series structure. (Contributed by Mario Carneiro, 29-Dec-2014)

Ref Expression
Hypotheses psrval.s ${⊢}{S}={I}\mathrm{mPwSer}{R}$
psrval.k ${⊢}{K}={\mathrm{Base}}_{{R}}$
psrval.a
psrval.m
psrval.o ${⊢}{O}=\mathrm{TopOpen}\left({R}\right)$
psrval.d ${⊢}{D}=\left\{{h}\in \left({{ℕ}_{0}}^{{I}}\right)|{{h}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\right\}$
psrval.b ${⊢}{\phi }\to {B}={{K}}^{{D}}$
psrval.p
psrval.t
psrval.v
psrval.j ${⊢}{\phi }\to {J}={\prod }_{𝑡}\left({D}×\left\{{O}\right\}\right)$
psrval.i ${⊢}{\phi }\to {I}\in {W}$
psrval.r ${⊢}{\phi }\to {R}\in {X}$
Assertion psrval

Proof

Step Hyp Ref Expression
1 psrval.s ${⊢}{S}={I}\mathrm{mPwSer}{R}$
2 psrval.k ${⊢}{K}={\mathrm{Base}}_{{R}}$
3 psrval.a
4 psrval.m
5 psrval.o ${⊢}{O}=\mathrm{TopOpen}\left({R}\right)$
6 psrval.d ${⊢}{D}=\left\{{h}\in \left({{ℕ}_{0}}^{{I}}\right)|{{h}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\right\}$
7 psrval.b ${⊢}{\phi }\to {B}={{K}}^{{D}}$
8 psrval.p
9 psrval.t
10 psrval.v
11 psrval.j ${⊢}{\phi }\to {J}={\prod }_{𝑡}\left({D}×\left\{{O}\right\}\right)$
12 psrval.i ${⊢}{\phi }\to {I}\in {W}$
13 psrval.r ${⊢}{\phi }\to {R}\in {X}$
14 df-psr
15 14 a1i
16 simprl ${⊢}\left({\phi }\wedge \left({i}={I}\wedge {r}={R}\right)\right)\to {i}={I}$
17 16 oveq2d ${⊢}\left({\phi }\wedge \left({i}={I}\wedge {r}={R}\right)\right)\to {{ℕ}_{0}}^{{i}}={{ℕ}_{0}}^{{I}}$
18 rabeq ${⊢}{{ℕ}_{0}}^{{i}}={{ℕ}_{0}}^{{I}}\to \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\}$
19 17 18 syl ${⊢}\left({\phi }\wedge \left({i}={I}\wedge {r}={R}\right)\right)\to \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\}$
20 19 6 syl6eqr ${⊢}\left({\phi }\wedge \left({i}={I}\wedge {r}={R}\right)\right)\to \left\{{h}\in \left({{ℕ}_{0}}^{{i}}\right)|{{h}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\right\}={D}$
21 20 csbeq1d
22 ovex ${⊢}{{ℕ}_{0}}^{{i}}\in \mathrm{V}$
23 22 rabex ${⊢}\left\{{h}\in \left({{ℕ}_{0}}^{{i}}\right)|{{h}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\right\}\in \mathrm{V}$
24 20 23 eqeltrrdi ${⊢}\left({\phi }\wedge \left({i}={I}\wedge {r}={R}\right)\right)\to {D}\in \mathrm{V}$
25 simplrr ${⊢}\left(\left({\phi }\wedge \left({i}={I}\wedge {r}={R}\right)\right)\wedge {d}={D}\right)\to {r}={R}$
26 25 fveq2d ${⊢}\left(\left({\phi }\wedge \left({i}={I}\wedge {r}={R}\right)\right)\wedge {d}={D}\right)\to {\mathrm{Base}}_{{r}}={\mathrm{Base}}_{{R}}$
27 26 2 syl6eqr ${⊢}\left(\left({\phi }\wedge \left({i}={I}\wedge {r}={R}\right)\right)\wedge {d}={D}\right)\to {\mathrm{Base}}_{{r}}={K}$
28 simpr ${⊢}\left(\left({\phi }\wedge \left({i}={I}\wedge {r}={R}\right)\right)\wedge {d}={D}\right)\to {d}={D}$
29 27 28 oveq12d ${⊢}\left(\left({\phi }\wedge \left({i}={I}\wedge {r}={R}\right)\right)\wedge {d}={D}\right)\to {{\mathrm{Base}}_{{r}}}^{{d}}={{K}}^{{D}}$
30 7 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({i}={I}\wedge {r}={R}\right)\right)\wedge {d}={D}\right)\to {B}={{K}}^{{D}}$
31 29 30 eqtr4d ${⊢}\left(\left({\phi }\wedge \left({i}={I}\wedge {r}={R}\right)\right)\wedge {d}={D}\right)\to {{\mathrm{Base}}_{{r}}}^{{d}}={B}$
32 31 csbeq1d
33 ovex ${⊢}{{\mathrm{Base}}_{{r}}}^{{d}}\in \mathrm{V}$
34 31 33 eqeltrrdi ${⊢}\left(\left({\phi }\wedge \left({i}={I}\wedge {r}={R}\right)\right)\wedge {d}={D}\right)\to {B}\in \mathrm{V}$
35 simpr ${⊢}\left(\left(\left({\phi }\wedge \left({i}={I}\wedge {r}={R}\right)\right)\wedge {d}={D}\right)\wedge {b}={B}\right)\to {b}={B}$
36 35 opeq2d ${⊢}\left(\left(\left({\phi }\wedge \left({i}={I}\wedge {r}={R}\right)\right)\wedge {d}={D}\right)\wedge {b}={B}\right)\to ⟨{\mathrm{Base}}_{\mathrm{ndx}},{b}⟩=⟨{\mathrm{Base}}_{\mathrm{ndx}},{B}⟩$
37 25 adantr ${⊢}\left(\left(\left({\phi }\wedge \left({i}={I}\wedge {r}={R}\right)\right)\wedge {d}={D}\right)\wedge {b}={B}\right)\to {r}={R}$
38 37 fveq2d ${⊢}\left(\left(\left({\phi }\wedge \left({i}={I}\wedge {r}={R}\right)\right)\wedge {d}={D}\right)\wedge {b}={B}\right)\to {+}_{{r}}={+}_{{R}}$
39 38 3 syl6eqr
40 ofeq
41 39 40 syl
42 35 35 xpeq12d ${⊢}\left(\left(\left({\phi }\wedge \left({i}={I}\wedge {r}={R}\right)\right)\wedge {d}={D}\right)\wedge {b}={B}\right)\to {b}×{b}={B}×{B}$
43 41 42 reseq12d
44 43 8 syl6eqr
45 44 opeq2d
46 28 adantr ${⊢}\left(\left(\left({\phi }\wedge \left({i}={I}\wedge {r}={R}\right)\right)\wedge {d}={D}\right)\wedge {b}={B}\right)\to {d}={D}$
47 rabeq ${⊢}{d}={D}\to \left\{{y}\in {d}|{y}{\le }_{f}{k}\right\}=\left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}$
48 46 47 syl ${⊢}\left(\left(\left({\phi }\wedge \left({i}={I}\wedge {r}={R}\right)\right)\wedge {d}={D}\right)\wedge {b}={B}\right)\to \left\{{y}\in {d}|{y}{\le }_{f}{k}\right\}=\left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}$
49 37 fveq2d ${⊢}\left(\left(\left({\phi }\wedge \left({i}={I}\wedge {r}={R}\right)\right)\wedge {d}={D}\right)\wedge {b}={B}\right)\to {\cdot }_{{r}}={\cdot }_{{R}}$
50 49 4 syl6eqr
51 50 oveqd
52 48 51 mpteq12dv
53 37 52 oveq12d
54 46 53 mpteq12dv
55 35 35 54 mpoeq123dv
56 55 9 syl6eqr
57 56 opeq2d
58 36 45 57 tpeq123d
59 37 opeq2d ${⊢}\left(\left(\left({\phi }\wedge \left({i}={I}\wedge {r}={R}\right)\right)\wedge {d}={D}\right)\wedge {b}={B}\right)\to ⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{r}⟩=⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{R}⟩$
60 27 adantr ${⊢}\left(\left(\left({\phi }\wedge \left({i}={I}\wedge {r}={R}\right)\right)\wedge {d}={D}\right)\wedge {b}={B}\right)\to {\mathrm{Base}}_{{r}}={K}$
61 ofeq
62 50 61 syl
63 46 xpeq1d ${⊢}\left(\left(\left({\phi }\wedge \left({i}={I}\wedge {r}={R}\right)\right)\wedge {d}={D}\right)\wedge {b}={B}\right)\to {d}×\left\{{x}\right\}={D}×\left\{{x}\right\}$
64 eqidd ${⊢}\left(\left(\left({\phi }\wedge \left({i}={I}\wedge {r}={R}\right)\right)\wedge {d}={D}\right)\wedge {b}={B}\right)\to {f}={f}$
65 62 63 64 oveq123d
66 60 35 65 mpoeq123dv
67 66 10 syl6eqr
68 67 opeq2d
69 37 fveq2d ${⊢}\left(\left(\left({\phi }\wedge \left({i}={I}\wedge {r}={R}\right)\right)\wedge {d}={D}\right)\wedge {b}={B}\right)\to \mathrm{TopOpen}\left({r}\right)=\mathrm{TopOpen}\left({R}\right)$
70 69 5 syl6eqr ${⊢}\left(\left(\left({\phi }\wedge \left({i}={I}\wedge {r}={R}\right)\right)\wedge {d}={D}\right)\wedge {b}={B}\right)\to \mathrm{TopOpen}\left({r}\right)={O}$
71 70 sneqd ${⊢}\left(\left(\left({\phi }\wedge \left({i}={I}\wedge {r}={R}\right)\right)\wedge {d}={D}\right)\wedge {b}={B}\right)\to \left\{\mathrm{TopOpen}\left({r}\right)\right\}=\left\{{O}\right\}$
72 46 71 xpeq12d ${⊢}\left(\left(\left({\phi }\wedge \left({i}={I}\wedge {r}={R}\right)\right)\wedge {d}={D}\right)\wedge {b}={B}\right)\to {d}×\left\{\mathrm{TopOpen}\left({r}\right)\right\}={D}×\left\{{O}\right\}$
73 72 fveq2d ${⊢}\left(\left(\left({\phi }\wedge \left({i}={I}\wedge {r}={R}\right)\right)\wedge {d}={D}\right)\wedge {b}={B}\right)\to {\prod }_{𝑡}\left({d}×\left\{\mathrm{TopOpen}\left({r}\right)\right\}\right)={\prod }_{𝑡}\left({D}×\left\{{O}\right\}\right)$
74 11 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge \left({i}={I}\wedge {r}={R}\right)\right)\wedge {d}={D}\right)\wedge {b}={B}\right)\to {J}={\prod }_{𝑡}\left({D}×\left\{{O}\right\}\right)$
75 73 74 eqtr4d ${⊢}\left(\left(\left({\phi }\wedge \left({i}={I}\wedge {r}={R}\right)\right)\wedge {d}={D}\right)\wedge {b}={B}\right)\to {\prod }_{𝑡}\left({d}×\left\{\mathrm{TopOpen}\left({r}\right)\right\}\right)={J}$
76 75 opeq2d ${⊢}\left(\left(\left({\phi }\wedge \left({i}={I}\wedge {r}={R}\right)\right)\wedge {d}={D}\right)\wedge {b}={B}\right)\to ⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),{\prod }_{𝑡}\left({d}×\left\{\mathrm{TopOpen}\left({r}\right)\right\}\right)⟩=⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),{J}⟩$
77 59 68 76 tpeq123d
78 58 77 uneq12d
79 34 78 csbied
80 32 79 eqtrd
81 24 80 csbied
82 21 81 eqtrd
83 12 elexd ${⊢}{\phi }\to {I}\in \mathrm{V}$
84 13 elexd ${⊢}{\phi }\to {R}\in \mathrm{V}$
85 tpex
86 tpex
87 85 86 unex
88 87 a1i
89 15 82 83 84 88 ovmpod
90 1 89 syl5eq