Metamath Proof Explorer

Theorem psrdir

Description: Distributive law for the ring of power series (right-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 psrdir

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 7 8 psradd
13 12 fveq1d
15 ssrab2 ${⊢}\left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}\subseteq {D}$
16 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\}$
17 15 16 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}$
18 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
19 1 18 4 6 7 psrelbas ${⊢}{\phi }\to {X}:{D}⟶{\mathrm{Base}}_{{R}}$
20 19 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}}$
21 20 ffnd ${⊢}\left(\left({\phi }\wedge {k}\in {D}\right)\wedge {x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}\right)\to {X}Fn{D}$
22 1 18 4 6 8 psrelbas ${⊢}{\phi }\to {Y}:{D}⟶{\mathrm{Base}}_{{R}}$
23 22 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}}$
24 23 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}$
25 ovex ${⊢}{{ℕ}_{0}}^{{I}}\in \mathrm{V}$
26 4 25 rabex2 ${⊢}{D}\in \mathrm{V}$
27 26 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}$
28 inidm ${⊢}{D}\cap {D}={D}$
29 eqidd ${⊢}\left(\left(\left({\phi }\wedge {k}\in {D}\right)\wedge {x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}\right)\wedge {x}\in {D}\right)\to {X}\left({x}\right)={X}\left({x}\right)$
30 eqidd ${⊢}\left(\left(\left({\phi }\wedge {k}\in {D}\right)\wedge {x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}\right)\wedge {x}\in {D}\right)\to {Y}\left({x}\right)={Y}\left({x}\right)$
31 21 24 27 27 28 29 30 ofval ${⊢}\left(\left(\left({\phi }\wedge {k}\in {D}\right)\wedge {x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}\right)\wedge {x}\in {D}\right)\to \left({X}{{+}_{{R}}}_{f}{Y}\right)\left({x}\right)={X}\left({x}\right){+}_{{R}}{Y}\left({x}\right)$
32 17 31 mpdan ${⊢}\left(\left({\phi }\wedge {k}\in {D}\right)\wedge {x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}\right)\to \left({X}{{+}_{{R}}}_{f}{Y}\right)\left({x}\right)={X}\left({x}\right){+}_{{R}}{Y}\left({x}\right)$
33 14 32 eqtrd
34 33 oveq1d
35 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}$
36 20 17 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}}$
37 23 17 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({x}\right)\in {\mathrm{Base}}_{{R}}$
38 1 18 4 6 9 psrelbas ${⊢}{\phi }\to {Z}:{D}⟶{\mathrm{Base}}_{{R}}$
39 38 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}}$
40 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}$
41 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}$
42 eqid ${⊢}\left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}=\left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}$
43 4 42 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\}$
44 40 41 16 43 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\}$
45 15 44 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}$
46 39 45 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 18 11 47 ringdir ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({X}\left({x}\right)\in {\mathrm{Base}}_{{R}}\wedge {Y}\left({x}\right)\in {\mathrm{Base}}_{{R}}\wedge {Z}\left({k}{-}_{f}{x}\right)\in {\mathrm{Base}}_{{R}}\right)\right)\to \left({X}\left({x}\right){+}_{{R}}{Y}\left({x}\right)\right){\cdot }_{{R}}{Z}\left({k}{-}_{f}{x}\right)=\left({X}\left({x}\right){\cdot }_{{R}}{Z}\left({k}{-}_{f}{x}\right)\right){+}_{{R}}\left({Y}\left({x}\right){\cdot }_{{R}}{Z}\left({k}{-}_{f}{x}\right)\right)$
49 35 36 37 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 \left({X}\left({x}\right){+}_{{R}}{Y}\left({x}\right)\right){\cdot }_{{R}}{Z}\left({k}{-}_{f}{x}\right)=\left({X}\left({x}\right){\cdot }_{{R}}{Z}\left({k}{-}_{f}{x}\right)\right){+}_{{R}}\left({Y}\left({x}\right){\cdot }_{{R}}{Z}\left({k}{-}_{f}{x}\right)\right)$
50 34 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 18 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}}$
55 35 36 46 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}}{Z}\left({k}{-}_{f}{x}\right)\in {\mathrm{Base}}_{{R}}$
56 18 47 ringcl ${⊢}\left({R}\in \mathrm{Ring}\wedge {Y}\left({x}\right)\in {\mathrm{Base}}_{{R}}\wedge {Z}\left({k}{-}_{f}{x}\right)\in {\mathrm{Base}}_{{R}}\right)\to {Y}\left({x}\right){\cdot }_{{R}}{Z}\left({k}{-}_{f}{x}\right)\in {\mathrm{Base}}_{{R}}$
57 35 37 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 {Y}\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}}{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)$
59 eqidd ${⊢}\left({\phi }\wedge {k}\in {D}\right)\to \left({x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}⟼{Y}\left({x}\right){\cdot }_{{R}}{Z}\left({k}{-}_{f}{x}\right)\right)=\left({x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}⟼{Y}\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}}{Z}\left({k}{-}_{f}{x}\right)\right){{+}_{{R}}}_{f}\left({x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}⟼{Y}\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}}{Z}\left({k}{-}_{f}{x}\right)\right){+}_{{R}}\left({Y}\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}}{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)$
67 eqid ${⊢}\left({x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}⟼{Y}\left({x}\right){\cdot }_{{R}}{Z}\left({k}{-}_{f}{x}\right)\right)=\left({x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}⟼{Y}\left({x}\right){\cdot }_{{R}}{Z}\left({k}{-}_{f}{x}\right)\right)$
68 18 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}}{Z}\left({k}{-}_{f}{x}\right)\right){{+}_{{R}}}_{f}\left({x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}⟼{Y}\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}}{Z}\left({k}{-}_{f}{x}\right)\right)\right){+}_{{R}}\left(\underset{{x}\in \left\{{y}\in {D}|{y}{\le }_{f}{k}\right\}}{{\sum }_{{R}}},\left({Y}\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 7 8 psraddcl
74 1 6 47 5 4 73 9 psrmulfval
75 1 6 5 3 7 9 psrmulcl
76 1 6 5 3 8 9 psrmulcl
77 1 6 11 10 75 76 psradd
78 26 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}}{Z}\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({Y}\left({x}\right){\cdot }_{{R}}{Z}\left({k}{-}_{f}{x}\right)\right)\in \mathrm{V}$
81 1 6 47 5 4 7 9 psrmulfval
82 1 6 47 5 4 8 9 psrmulfval
83 78 79 80 81 82 offval2
84 77 83 eqtrd
85 70 74 84 3eqtr4d