# Metamath Proof Explorer

## Theorem psrvscafval

Description: The scalar multiplication operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014) (Revised by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses psrvsca.s ${⊢}{S}={I}\mathrm{mPwSer}{R}$
psrvsca.n
psrvsca.k ${⊢}{K}={\mathrm{Base}}_{{R}}$
psrvsca.b ${⊢}{B}={\mathrm{Base}}_{{S}}$
psrvsca.m
psrvsca.d ${⊢}{D}=\left\{{h}\in \left({{ℕ}_{0}}^{{I}}\right)|{{h}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\right\}$
Assertion psrvscafval

### Proof

Step Hyp Ref Expression
1 psrvsca.s ${⊢}{S}={I}\mathrm{mPwSer}{R}$
2 psrvsca.n
3 psrvsca.k ${⊢}{K}={\mathrm{Base}}_{{R}}$
4 psrvsca.b ${⊢}{B}={\mathrm{Base}}_{{S}}$
5 psrvsca.m
6 psrvsca.d ${⊢}{D}=\left\{{h}\in \left({{ℕ}_{0}}^{{I}}\right)|{{h}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\right\}$
7 eqid ${⊢}{+}_{{R}}={+}_{{R}}$
8 eqid ${⊢}\mathrm{TopOpen}\left({R}\right)=\mathrm{TopOpen}\left({R}\right)$
9 simpl ${⊢}\left({I}\in \mathrm{V}\wedge {R}\in \mathrm{V}\right)\to {I}\in \mathrm{V}$
10 1 3 6 4 9 psrbas ${⊢}\left({I}\in \mathrm{V}\wedge {R}\in \mathrm{V}\right)\to {B}={{K}}^{{D}}$
11 eqid ${⊢}{+}_{{S}}={+}_{{S}}$
12 1 4 7 11 psrplusg ${⊢}{+}_{{S}}={{\circ }_{f}{+}_{{R}}↾}_{\left({B}×{B}\right)}$
13 eqid ${⊢}{\cdot }_{{S}}={\cdot }_{{S}}$
14 1 4 5 13 6 psrmulr
15 eqid
16 eqidd ${⊢}\left({I}\in \mathrm{V}\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)$
17 simpr ${⊢}\left({I}\in \mathrm{V}\wedge {R}\in \mathrm{V}\right)\to {R}\in \mathrm{V}$
18 1 3 7 5 8 6 10 12 14 15 16 9 17 psrval
19 18 fveq2d
20 3 fvexi ${⊢}{K}\in \mathrm{V}$
21 4 fvexi ${⊢}{B}\in \mathrm{V}$
22 20 21 mpoex
23 psrvalstr
24 vscaid ${⊢}{\cdot }_{𝑠}=\mathrm{Slot}{\cdot }_{\mathrm{ndx}}$
25 snsstp2
26 ssun2
27 25 26 sstri
28 23 24 27 strfv
29 22 28 ax-mp
30 19 2 29 3eqtr4g
31 eqid ${⊢}\varnothing =\varnothing$
32 fn0 ${⊢}\varnothing Fn\varnothing ↔\varnothing =\varnothing$
33 31 32 mpbir ${⊢}\varnothing Fn\varnothing$
34 reldmpsr ${⊢}\mathrm{Rel}\mathrm{dom}\mathrm{mPwSer}$
35 34 ovprc ${⊢}¬\left({I}\in \mathrm{V}\wedge {R}\in \mathrm{V}\right)\to {I}\mathrm{mPwSer}{R}=\varnothing$
36 1 35 syl5eq ${⊢}¬\left({I}\in \mathrm{V}\wedge {R}\in \mathrm{V}\right)\to {S}=\varnothing$
37 36 fveq2d ${⊢}¬\left({I}\in \mathrm{V}\wedge {R}\in \mathrm{V}\right)\to {\cdot }_{{S}}={\cdot }_{\varnothing }$
38 df-vsca ${⊢}{\cdot }_{𝑠}=\mathrm{Slot}6$
39 38 str0 ${⊢}\varnothing ={\cdot }_{\varnothing }$
40 37 2 39 3eqtr4g
41 34 1 4 elbasov ${⊢}{f}\in {B}\to \left({I}\in \mathrm{V}\wedge {R}\in \mathrm{V}\right)$
42 41 con3i ${⊢}¬\left({I}\in \mathrm{V}\wedge {R}\in \mathrm{V}\right)\to ¬{f}\in {B}$
43 42 eq0rdv ${⊢}¬\left({I}\in \mathrm{V}\wedge {R}\in \mathrm{V}\right)\to {B}=\varnothing$
44 43 xpeq2d ${⊢}¬\left({I}\in \mathrm{V}\wedge {R}\in \mathrm{V}\right)\to {K}×{B}={K}×\varnothing$
45 xp0 ${⊢}{K}×\varnothing =\varnothing$
46 44 45 syl6eq ${⊢}¬\left({I}\in \mathrm{V}\wedge {R}\in \mathrm{V}\right)\to {K}×{B}=\varnothing$
47 40 46 fneq12d
48 33 47 mpbiri
49 fnov
50 48 49 sylib
51 42 pm2.21d
52 51 a1d
53 52 3imp
54 53 mpoeq3dva
55 50 54 eqtr4d
56 30 55 pm2.61i