# Metamath Proof Explorer

## Theorem psrdi

Description: Distributive law for the ring of power series (left-distributivity). (Contributed by Mario Carneiro, 7-Jan-2015)

Ref Expression
Hypotheses psrring.s ${⊢}{S}={I}\mathrm{mPwSer}{R}$
psrring.i ${⊢}{\phi }\to {I}\in {V}$
psrring.r ${⊢}{\phi }\to {R}\in \mathrm{Ring}$
psrass.d ${⊢}{D}=\left\{{f}\in \left({{ℕ}_{0}}^{{I}}\right)|{{f}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\right\}$
psrass.t
psrass.b ${⊢}{B}={\mathrm{Base}}_{{S}}$
psrass.x ${⊢}{\phi }\to {X}\in {B}$
psrass.y ${⊢}{\phi }\to {Y}\in {B}$
psrass.z ${⊢}{\phi }\to {Z}\in {B}$
psrdi.a
Assertion psrdi

### Proof

Step Hyp Ref Expression
1 psrring.s ${⊢}{S}={I}\mathrm{mPwSer}{R}$
2 psrring.i ${⊢}{\phi }\to {I}\in {V}$
3 psrring.r ${⊢}{\phi }\to {R}\in \mathrm{Ring}$
4 psrass.d ${⊢}{D}=\left\{{f}\in \left({{ℕ}_{0}}^{{I}}\right)|{{f}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\right\}$
5 psrass.t
6 psrass.b ${⊢}{B}={\mathrm{Base}}_{{S}}$
7 psrass.x ${⊢}{\phi }\to {X}\in {B}$
8 psrass.y ${⊢}{\phi }\to {Y}\in {B}$
9 psrass.z ${⊢}{\phi }\to {Z}\in {B}$
10 psrdi.a
11 eqid ${⊢}{+}_{{R}}={+}_{{R}}$
12 1 6 11 10 8 9 psradd
13 12 fveq1d
15 ssrab2 ${⊢}\left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}\subseteq {D}$
16 2 ad2antrr ${⊢}\left(\left({\phi }\wedge {k}\in {D}\right)\wedge {x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}\right)\to {I}\in {V}$
17 simplr ${⊢}\left(\left({\phi }\wedge {k}\in {D}\right)\wedge {x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}\right)\to {k}\in {D}$
18 simpr ${⊢}\left(\left({\phi }\wedge {k}\in {D}\right)\wedge {x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}\right)\to {x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}$
19 eqid ${⊢}\left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}=\left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}$
20 4 19 psrbagconcl ${⊢}\left({I}\in {V}\wedge {k}\in {D}\wedge {x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}\right)\to {k}{-}_{f}{x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}$
21 16 17 18 20 syl3anc ${⊢}\left(\left({\phi }\wedge {k}\in {D}\right)\wedge {x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}\right)\to {k}{-}_{f}{x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}$
22 15 21 sseldi ${⊢}\left(\left({\phi }\wedge {k}\in {D}\right)\wedge {x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}\right)\to {k}{-}_{f}{x}\in {D}$
23 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
24 1 23 4 6 8 psrelbas ${⊢}{\phi }\to {Y}:{D}⟶{\mathrm{Base}}_{{R}}$
25 24 ad2antrr ${⊢}\left(\left({\phi }\wedge {k}\in {D}\right)\wedge {x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}\right)\to {Y}:{D}⟶{\mathrm{Base}}_{{R}}$
26 25 ffnd ${⊢}\left(\left({\phi }\wedge {k}\in {D}\right)\wedge {x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}\right)\to {Y}Fn{D}$
27 1 23 4 6 9 psrelbas ${⊢}{\phi }\to {Z}:{D}⟶{\mathrm{Base}}_{{R}}$
28 27 ad2antrr ${⊢}\left(\left({\phi }\wedge {k}\in {D}\right)\wedge {x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}\right)\to {Z}:{D}⟶{\mathrm{Base}}_{{R}}$
29 28 ffnd ${⊢}\left(\left({\phi }\wedge {k}\in {D}\right)\wedge {x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}\right)\to {Z}Fn{D}$
30 ovex ${⊢}{{ℕ}_{0}}^{{I}}\in \mathrm{V}$
31 4 30 rabex2 ${⊢}{D}\in \mathrm{V}$
32 31 a1i ${⊢}\left(\left({\phi }\wedge {k}\in {D}\right)\wedge {x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}\right)\to {D}\in \mathrm{V}$
33 inidm ${⊢}{D}\cap {D}={D}$
34 eqidd ${⊢}\left(\left(\left({\phi }\wedge {k}\in {D}\right)\wedge {x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}\right)\wedge {k}{-}_{f}{x}\in {D}\right)\to {Y}\left({k}{-}_{f}{x}\right)={Y}\left({k}{-}_{f}{x}\right)$
35 eqidd ${⊢}\left(\left(\left({\phi }\wedge {k}\in {D}\right)\wedge {x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}\right)\wedge {k}{-}_{f}{x}\in {D}\right)\to {Z}\left({k}{-}_{f}{x}\right)={Z}\left({k}{-}_{f}{x}\right)$
36 26 29 32 32 33 34 35 ofval ${⊢}\left(\left(\left({\phi }\wedge {k}\in {D}\right)\wedge {x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}\right)\wedge {k}{-}_{f}{x}\in {D}\right)\to \left({Y}{{+}_{{R}}}_{f}{Z}\right)\left({k}{-}_{f}{x}\right)={Y}\left({k}{-}_{f}{x}\right){+}_{{R}}{Z}\left({k}{-}_{f}{x}\right)$
37 22 36 mpdan ${⊢}\left(\left({\phi }\wedge {k}\in {D}\right)\wedge {x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}\right)\to \left({Y}{{+}_{{R}}}_{f}{Z}\right)\left({k}{-}_{f}{x}\right)={Y}\left({k}{-}_{f}{x}\right){+}_{{R}}{Z}\left({k}{-}_{f}{x}\right)$
38 14 37 eqtrd
39 38 oveq2d
40 3 ad2antrr ${⊢}\left(\left({\phi }\wedge {k}\in {D}\right)\wedge {x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}\right)\to {R}\in \mathrm{Ring}$
41 1 23 4 6 7 psrelbas ${⊢}{\phi }\to {X}:{D}⟶{\mathrm{Base}}_{{R}}$
42 41 ad2antrr ${⊢}\left(\left({\phi }\wedge {k}\in {D}\right)\wedge {x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}\right)\to {X}:{D}⟶{\mathrm{Base}}_{{R}}$
43 15 18 sseldi ${⊢}\left(\left({\phi }\wedge {k}\in {D}\right)\wedge {x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}\right)\to {x}\in {D}$
44 42 43 ffvelrnd ${⊢}\left(\left({\phi }\wedge {k}\in {D}\right)\wedge {x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}\right)\to {X}\left({x}\right)\in {\mathrm{Base}}_{{R}}$
45 25 22 ffvelrnd ${⊢}\left(\left({\phi }\wedge {k}\in {D}\right)\wedge {x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}\right)\to {Y}\left({k}{-}_{f}{x}\right)\in {\mathrm{Base}}_{{R}}$
46 28 22 ffvelrnd ${⊢}\left(\left({\phi }\wedge {k}\in {D}\right)\wedge {x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}\right)\to {Z}\left({k}{-}_{f}{x}\right)\in {\mathrm{Base}}_{{R}}$
47 eqid ${⊢}{\cdot }_{{R}}={\cdot }_{{R}}$
48 23 11 47 ringdi ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({X}\left({x}\right)\in {\mathrm{Base}}_{{R}}\wedge {Y}\left({k}{-}_{f}{x}\right)\in {\mathrm{Base}}_{{R}}\wedge {Z}\left({k}{-}_{f}{x}\right)\in {\mathrm{Base}}_{{R}}\right)\right)\to {X}\left({x}\right){\cdot }_{{R}}\left({Y}\left({k}{-}_{f}{x}\right){+}_{{R}}{Z}\left({k}{-}_{f}{x}\right)\right)=\left({X}\left({x}\right){\cdot }_{{R}}{Y}\left({k}{-}_{f}{x}\right)\right){+}_{{R}}\left({X}\left({x}\right){\cdot }_{{R}}{Z}\left({k}{-}_{f}{x}\right)\right)$
49 40 44 45 46 48 syl13anc ${⊢}\left(\left({\phi }\wedge {k}\in {D}\right)\wedge {x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}\right)\to {X}\left({x}\right){\cdot }_{{R}}\left({Y}\left({k}{-}_{f}{x}\right){+}_{{R}}{Z}\left({k}{-}_{f}{x}\right)\right)=\left({X}\left({x}\right){\cdot }_{{R}}{Y}\left({k}{-}_{f}{x}\right)\right){+}_{{R}}\left({X}\left({x}\right){\cdot }_{{R}}{Z}\left({k}{-}_{f}{x}\right)\right)$
50 39 49 eqtrd
51 50 mpteq2dva
52 4 psrbaglefi ${⊢}\left({I}\in {V}\wedge {k}\in {D}\right)\to \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}\in \mathrm{Fin}$
53 2 52 sylan ${⊢}\left({\phi }\wedge {k}\in {D}\right)\to \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}\in \mathrm{Fin}$
54 23 47 ringcl ${⊢}\left({R}\in \mathrm{Ring}\wedge {X}\left({x}\right)\in {\mathrm{Base}}_{{R}}\wedge {Y}\left({k}{-}_{f}{x}\right)\in {\mathrm{Base}}_{{R}}\right)\to {X}\left({x}\right){\cdot }_{{R}}{Y}\left({k}{-}_{f}{x}\right)\in {\mathrm{Base}}_{{R}}$
55 40 44 45 54 syl3anc ${⊢}\left(\left({\phi }\wedge {k}\in {D}\right)\wedge {x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}\right)\to {X}\left({x}\right){\cdot }_{{R}}{Y}\left({k}{-}_{f}{x}\right)\in {\mathrm{Base}}_{{R}}$
56 23 47 ringcl ${⊢}\left({R}\in \mathrm{Ring}\wedge {X}\left({x}\right)\in {\mathrm{Base}}_{{R}}\wedge {Z}\left({k}{-}_{f}{x}\right)\in {\mathrm{Base}}_{{R}}\right)\to {X}\left({x}\right){\cdot }_{{R}}{Z}\left({k}{-}_{f}{x}\right)\in {\mathrm{Base}}_{{R}}$
57 40 44 46 56 syl3anc ${⊢}\left(\left({\phi }\wedge {k}\in {D}\right)\wedge {x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}\right)\to {X}\left({x}\right){\cdot }_{{R}}{Z}\left({k}{-}_{f}{x}\right)\in {\mathrm{Base}}_{{R}}$
58 eqidd ${⊢}\left({\phi }\wedge {k}\in {D}\right)\to \left({x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}⟼{X}\left({x}\right){\cdot }_{{R}}{Y}\left({k}{-}_{f}{x}\right)\right)=\left({x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}⟼{X}\left({x}\right){\cdot }_{{R}}{Y}\left({k}{-}_{f}{x}\right)\right)$
59 eqidd ${⊢}\left({\phi }\wedge {k}\in {D}\right)\to \left({x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}⟼{X}\left({x}\right){\cdot }_{{R}}{Z}\left({k}{-}_{f}{x}\right)\right)=\left({x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}⟼{X}\left({x}\right){\cdot }_{{R}}{Z}\left({k}{-}_{f}{x}\right)\right)$
60 53 55 57 58 59 offval2 ${⊢}\left({\phi }\wedge {k}\in {D}\right)\to \left({x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}⟼{X}\left({x}\right){\cdot }_{{R}}{Y}\left({k}{-}_{f}{x}\right)\right){{+}_{{R}}}_{f}\left({x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}⟼{X}\left({x}\right){\cdot }_{{R}}{Z}\left({k}{-}_{f}{x}\right)\right)=\left({x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}⟼\left({X}\left({x}\right){\cdot }_{{R}}{Y}\left({k}{-}_{f}{x}\right)\right){+}_{{R}}\left({X}\left({x}\right){\cdot }_{{R}}{Z}\left({k}{-}_{f}{x}\right)\right)\right)$
61 51 60 eqtr4d
62 61 oveq2d
63 3 adantr ${⊢}\left({\phi }\wedge {k}\in {D}\right)\to {R}\in \mathrm{Ring}$
64 ringcmn ${⊢}{R}\in \mathrm{Ring}\to {R}\in \mathrm{CMnd}$
65 63 64 syl ${⊢}\left({\phi }\wedge {k}\in {D}\right)\to {R}\in \mathrm{CMnd}$
66 eqid ${⊢}\left({x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}⟼{X}\left({x}\right){\cdot }_{{R}}{Y}\left({k}{-}_{f}{x}\right)\right)=\left({x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}⟼{X}\left({x}\right){\cdot }_{{R}}{Y}\left({k}{-}_{f}{x}\right)\right)$
67 eqid ${⊢}\left({x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}⟼{X}\left({x}\right){\cdot }_{{R}}{Z}\left({k}{-}_{f}{x}\right)\right)=\left({x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}⟼{X}\left({x}\right){\cdot }_{{R}}{Z}\left({k}{-}_{f}{x}\right)\right)$
68 23 11 65 53 55 57 66 67 gsummptfidmadd2 ${⊢}\left({\phi }\wedge {k}\in {D}\right)\to {\sum }_{{R}}\left(\left({x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}⟼{X}\left({x}\right){\cdot }_{{R}}{Y}\left({k}{-}_{f}{x}\right)\right){{+}_{{R}}}_{f}\left({x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}⟼{X}\left({x}\right){\cdot }_{{R}}{Z}\left({k}{-}_{f}{x}\right)\right)\right)=\left(\underset{{x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}}{{\sum }_{{R}}},\left({X}\left({x}\right){\cdot }_{{R}}{Y}\left({k}{-}_{f}{x}\right)\right)\right){+}_{{R}}\left(\underset{{x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}}{{\sum }_{{R}}},\left({X}\left({x}\right){\cdot }_{{R}}{Z}\left({k}{-}_{f}{x}\right)\right)\right)$
69 62 68 eqtrd
70 69 mpteq2dva
71 ringgrp ${⊢}{R}\in \mathrm{Ring}\to {R}\in \mathrm{Grp}$
72 3 71 syl ${⊢}{\phi }\to {R}\in \mathrm{Grp}$
73 1 6 10 72 8 9 psraddcl
74 1 6 47 5 4 7 73 psrmulfval
75 1 6 5 3 7 8 psrmulcl
76 1 6 5 3 7 9 psrmulcl
77 1 6 11 10 75 76 psradd
78 31 a1i ${⊢}{\phi }\to {D}\in \mathrm{V}$
79 ovexd ${⊢}\left({\phi }\wedge {k}\in {D}\right)\to \underset{{x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}}{{\sum }_{{R}}}\left({X}\left({x}\right){\cdot }_{{R}}{Y}\left({k}{-}_{f}{x}\right)\right)\in \mathrm{V}$
80 ovexd ${⊢}\left({\phi }\wedge {k}\in {D}\right)\to \underset{{x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}}{{\sum }_{{R}}}\left({X}\left({x}\right){\cdot }_{{R}}{Z}\left({k}{-}_{f}{x}\right)\right)\in \mathrm{V}$
81 1 6 47 5 4 7 8 psrmulfval
82 1 6 47 5 4 7 9 psrmulfval
83 78 79 80 81 82 offval2
84 77 83 eqtrd
85 70 74 84 3eqtr4d