Metamath Proof Explorer

Theorem psrmulr

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

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

Proof

Step Hyp Ref Expression
1 psrmulr.s ${⊢}{S}={I}\mathrm{mPwSer}{R}$
2 psrmulr.b ${⊢}{B}={\mathrm{Base}}_{{S}}$
3 psrmulr.m
4 psrmulr.t
5 psrmulr.d ${⊢}{D}=\left\{{h}\in \left({{ℕ}_{0}}^{{I}}\right)|{{h}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\right\}$
6 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
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 6 5 2 9 psrbas ${⊢}\left({I}\in \mathrm{V}\wedge {R}\in \mathrm{V}\right)\to {B}={{\mathrm{Base}}_{{R}}}^{{D}}$
11 eqid ${⊢}{+}_{{S}}={+}_{{S}}$
12 1 2 7 11 psrplusg ${⊢}{+}_{{S}}={{\circ }_{f}{+}_{{R}}↾}_{\left({B}×{B}\right)}$
13 eqid
14 eqid
15 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)$
16 simpr ${⊢}\left({I}\in \mathrm{V}\wedge {R}\in \mathrm{V}\right)\to {R}\in \mathrm{V}$
17 1 6 7 3 8 5 10 12 13 14 15 9 16 psrval
18 17 fveq2d
19 2 fvexi ${⊢}{B}\in \mathrm{V}$
20 19 19 mpoex
21 psrvalstr
22 mulrid ${⊢}{\cdot }_{𝑟}=\mathrm{Slot}{\cdot }_{\mathrm{ndx}}$
23 snsstp3
24 ssun1
25 23 24 sstri
26 21 22 25 strfv
27 20 26 ax-mp
28 18 4 27 3eqtr4g
29 22 str0 ${⊢}\varnothing ={\cdot }_{\varnothing }$
30 29 eqcomi ${⊢}{\cdot }_{\varnothing }=\varnothing$
31 reldmpsr ${⊢}\mathrm{Rel}\mathrm{dom}\mathrm{mPwSer}$
32 31 ovprc ${⊢}¬\left({I}\in \mathrm{V}\wedge {R}\in \mathrm{V}\right)\to {I}\mathrm{mPwSer}{R}=\varnothing$
33 1 32 syl5eq ${⊢}¬\left({I}\in \mathrm{V}\wedge {R}\in \mathrm{V}\right)\to {S}=\varnothing$
34 33 fveq2d ${⊢}¬\left({I}\in \mathrm{V}\wedge {R}\in \mathrm{V}\right)\to {\cdot }_{{S}}={\cdot }_{\varnothing }$
35 4 34 syl5eq
36 33 fveq2d ${⊢}¬\left({I}\in \mathrm{V}\wedge {R}\in \mathrm{V}\right)\to {\mathrm{Base}}_{{S}}={\mathrm{Base}}_{\varnothing }$
37 base0 ${⊢}\varnothing ={\mathrm{Base}}_{\varnothing }$
38 36 2 37 3eqtr4g ${⊢}¬\left({I}\in \mathrm{V}\wedge {R}\in \mathrm{V}\right)\to {B}=\varnothing$
39 38 olcd ${⊢}¬\left({I}\in \mathrm{V}\wedge {R}\in \mathrm{V}\right)\to \left({B}=\varnothing \vee {B}=\varnothing \right)$
40 0mpo0
41 39 40 syl
42 30 35 41 3eqtr4a
43 28 42 pm2.61i