Metamath Proof Explorer


Theorem mplsubglem

Description: If A is an ideal of sets (a nonempty collection closed under subset and binary union) of the set D of finite bags (the primary applications being A = Fin and A = ~P B for some B ), then the set of all power series whose coefficient functions are supported on an element of A is a subgroup of the set of all power series. (Contributed by Mario Carneiro, 12-Jan-2015) (Revised by AV, 16-Jul-2019)

Ref Expression
Hypotheses mplsubglem.s S=ImPwSerR
mplsubglem.b B=BaseS
mplsubglem.z 0˙=0R
mplsubglem.d D=f0I|f-1Fin
mplsubglem.i φIW
mplsubglem.0 φA
mplsubglem.a φxAyAxyA
mplsubglem.y φxAyxyA
mplsubglem.u φU=gB|gsupp0˙A
mplsubglem.r φRGrp
Assertion mplsubglem φUSubGrpS

Proof

Step Hyp Ref Expression
1 mplsubglem.s S=ImPwSerR
2 mplsubglem.b B=BaseS
3 mplsubglem.z 0˙=0R
4 mplsubglem.d D=f0I|f-1Fin
5 mplsubglem.i φIW
6 mplsubglem.0 φA
7 mplsubglem.a φxAyAxyA
8 mplsubglem.y φxAyxyA
9 mplsubglem.u φU=gB|gsupp0˙A
10 mplsubglem.r φRGrp
11 ssrab2 gB|gsupp0˙AB
12 9 11 eqsstrdi φUB
13 1 5 10 4 3 2 psr0cl φD×0˙B
14 eqid BaseR=BaseR
15 14 3 grpidcl RGrp0˙BaseR
16 fconst6g 0˙BaseRD×0˙:DBaseR
17 10 15 16 3syl φD×0˙:DBaseR
18 eldifi uDuD
19 3 fvexi 0˙V
20 19 fvconst2 uDD×0˙u=0˙
21 18 20 syl uDD×0˙u=0˙
22 21 adantl φuDD×0˙u=0˙
23 17 22 suppss φD×0˙supp0˙
24 ss0 D×0˙supp0˙D×0˙supp0˙=
25 23 24 syl φD×0˙supp0˙=
26 25 6 eqeltrd φD×0˙supp0˙A
27 9 eleq2d φD×0˙UD×0˙gB|gsupp0˙A
28 oveq1 g=D×0˙gsupp0˙=D×0˙supp0˙
29 28 eleq1d g=D×0˙gsupp0˙AD×0˙supp0˙A
30 29 elrab D×0˙gB|gsupp0˙AD×0˙BD×0˙supp0˙A
31 27 30 bitrdi φD×0˙UD×0˙BD×0˙supp0˙A
32 13 26 31 mpbir2and φD×0˙U
33 32 ne0d φU
34 eqid +S=+S
35 10 ad2antrr φuUvURGrp
36 9 eleq2d φuUugB|gsupp0˙A
37 oveq1 g=ugsupp0˙=usupp0˙
38 37 eleq1d g=ugsupp0˙Ausupp0˙A
39 38 elrab ugB|gsupp0˙AuBusupp0˙A
40 36 39 bitrdi φuUuBusupp0˙A
41 40 biimpa φuUuBusupp0˙A
42 41 simpld φuUuB
43 42 adantr φuUvUuB
44 9 adantr φuUU=gB|gsupp0˙A
45 44 eleq2d φuUvUvgB|gsupp0˙A
46 oveq1 g=vgsupp0˙=vsupp0˙
47 46 eleq1d g=vgsupp0˙Avsupp0˙A
48 47 elrab vgB|gsupp0˙AvBvsupp0˙A
49 45 48 bitrdi φuUvUvBvsupp0˙A
50 49 biimpa φuUvUvBvsupp0˙A
51 50 simpld φuUvUvB
52 1 2 34 35 43 51 psraddcl φuUvUu+SvB
53 ovexd φuUvUu+Svsupp0˙V
54 sseq2 x=supp0˙usupp0˙vyxysupp0˙usupp0˙v
55 54 imbi1d x=supp0˙usupp0˙vyxyAysupp0˙usupp0˙vyA
56 55 albidv x=supp0˙usupp0˙vyyxyAyysupp0˙usupp0˙vyA
57 8 expr φxAyxyA
58 57 alrimiv φxAyyxyA
59 58 ralrimiva φxAyyxyA
60 59 ad2antrr φuUvUxAyyxyA
61 41 simprd φuUusupp0˙A
62 61 adantr φuUvUusupp0˙A
63 50 simprd φuUvUvsupp0˙A
64 7 ralrimivva φxAyAxyA
65 64 ad2antrr φuUvUxAyAxyA
66 uneq1 x=usupp0˙xy=supp0˙uy
67 66 eleq1d x=usupp0˙xyAsupp0˙uyA
68 uneq2 y=vsupp0˙supp0˙uy=supp0˙usupp0˙v
69 68 eleq1d y=vsupp0˙supp0˙uyAsupp0˙usupp0˙vA
70 67 69 rspc2va usupp0˙Avsupp0˙AxAyAxyAsupp0˙usupp0˙vA
71 62 63 65 70 syl21anc φuUvUsupp0˙usupp0˙vA
72 56 60 71 rspcdva φuUvUyysupp0˙usupp0˙vyA
73 1 14 4 2 52 psrelbas φuUvUu+Sv:DBaseR
74 eqid +R=+R
75 1 2 74 34 43 51 psradd φuUvUu+Sv=u+Rfv
76 75 fveq1d φuUvUu+Svk=u+Rfvk
77 76 adantr φuUvUkDsupp0˙usupp0˙vu+Svk=u+Rfvk
78 eldifi kDsupp0˙usupp0˙vkD
79 1 14 4 2 42 psrelbas φuUu:DBaseR
80 79 adantr φuUvUu:DBaseR
81 80 ffnd φuUvUuFnD
82 1 14 4 2 51 psrelbas φuUvUv:DBaseR
83 82 ffnd φuUvUvFnD
84 ovex 0IV
85 4 84 rabex2 DV
86 85 a1i φuUvUDV
87 inidm DD=D
88 eqidd φuUvUkDuk=uk
89 eqidd φuUvUkDvk=vk
90 81 83 86 86 87 88 89 ofval φuUvUkDu+Rfvk=uk+Rvk
91 78 90 sylan2 φuUvUkDsupp0˙usupp0˙vu+Rfvk=uk+Rvk
92 ssun1 usupp0˙supp0˙usupp0˙v
93 sscon usupp0˙supp0˙usupp0˙vDsupp0˙usupp0˙vDsupp0˙u
94 92 93 ax-mp Dsupp0˙usupp0˙vDsupp0˙u
95 94 sseli kDsupp0˙usupp0˙vkDsupp0˙u
96 ssidd φuUusupp0˙usupp0˙
97 85 a1i φuUDV
98 19 a1i φuU0˙V
99 79 96 97 98 suppssr φuUkDsupp0˙uuk=0˙
100 99 adantlr φuUvUkDsupp0˙uuk=0˙
101 95 100 sylan2 φuUvUkDsupp0˙usupp0˙vuk=0˙
102 ssun2 vsupp0˙supp0˙usupp0˙v
103 sscon vsupp0˙supp0˙usupp0˙vDsupp0˙usupp0˙vDsupp0˙v
104 102 103 ax-mp Dsupp0˙usupp0˙vDsupp0˙v
105 104 sseli kDsupp0˙usupp0˙vkDsupp0˙v
106 ssidd φuUvUvsupp0˙vsupp0˙
107 19 a1i φuUvU0˙V
108 82 106 86 107 suppssr φuUvUkDsupp0˙vvk=0˙
109 105 108 sylan2 φuUvUkDsupp0˙usupp0˙vvk=0˙
110 101 109 oveq12d φuUvUkDsupp0˙usupp0˙vuk+Rvk=0˙+R0˙
111 14 74 3 grplid RGrp0˙BaseR0˙+R0˙=0˙
112 35 15 111 syl2anc2 φuUvU0˙+R0˙=0˙
113 112 adantr φuUvUkDsupp0˙usupp0˙v0˙+R0˙=0˙
114 110 113 eqtrd φuUvUkDsupp0˙usupp0˙vuk+Rvk=0˙
115 77 91 114 3eqtrd φuUvUkDsupp0˙usupp0˙vu+Svk=0˙
116 73 115 suppss φuUvUu+Svsupp0˙supp0˙usupp0˙v
117 sseq1 y=u+Svsupp0˙ysupp0˙usupp0˙vu+Svsupp0˙supp0˙usupp0˙v
118 eleq1 y=u+Svsupp0˙yAu+Svsupp0˙A
119 117 118 imbi12d y=u+Svsupp0˙ysupp0˙usupp0˙vyAu+Svsupp0˙supp0˙usupp0˙vu+Svsupp0˙A
120 119 spcgv u+Svsupp0˙Vyysupp0˙usupp0˙vyAu+Svsupp0˙supp0˙usupp0˙vu+Svsupp0˙A
121 53 72 116 120 syl3c φuUvUu+Svsupp0˙A
122 9 ad2antrr φuUvUU=gB|gsupp0˙A
123 122 eleq2d φuUvUu+SvUu+SvgB|gsupp0˙A
124 oveq1 g=u+Svgsupp0˙=u+Svsupp0˙
125 124 eleq1d g=u+Svgsupp0˙Au+Svsupp0˙A
126 125 elrab u+SvgB|gsupp0˙Au+SvBu+Svsupp0˙A
127 123 126 bitrdi φuUvUu+SvUu+SvBu+Svsupp0˙A
128 52 121 127 mpbir2and φuUvUu+SvU
129 128 ralrimiva φuUvUu+SvU
130 1 5 10 psrgrp φSGrp
131 eqid invgS=invgS
132 2 131 grpinvcl SGrpuBinvgSuB
133 130 42 132 syl2an2r φuUinvgSuB
134 ovexd φuUinvgSusupp0˙V
135 sseq2 x=usupp0˙yxyusupp0˙
136 135 imbi1d x=usupp0˙yxyAyusupp0˙yA
137 136 albidv x=usupp0˙yyxyAyyusupp0˙yA
138 59 adantr φuUxAyyxyA
139 137 138 61 rspcdva φuUyyusupp0˙yA
140 5 adantr φuUIW
141 10 adantr φuURGrp
142 eqid invgR=invgR
143 1 140 141 4 142 2 131 42 psrneg φuUinvgSu=invgRu
144 143 oveq1d φuUinvgSusupp0˙=invgRusupp0˙
145 14 142 grpinvfn invgRFnBaseR
146 145 a1i φuUinvgRFnBaseR
147 3 142 grpinvid RGrpinvgR0˙=0˙
148 141 147 syl φuUinvgR0˙=0˙
149 146 79 97 98 148 suppcoss φuUinvgRusupp0˙usupp0˙
150 144 149 eqsstrd φuUinvgSusupp0˙usupp0˙
151 sseq1 y=invgSusupp0˙yusupp0˙invgSusupp0˙usupp0˙
152 eleq1 y=invgSusupp0˙yAinvgSusupp0˙A
153 151 152 imbi12d y=invgSusupp0˙yusupp0˙yAinvgSusupp0˙usupp0˙invgSusupp0˙A
154 153 spcgv invgSusupp0˙Vyyusupp0˙yAinvgSusupp0˙usupp0˙invgSusupp0˙A
155 134 139 150 154 syl3c φuUinvgSusupp0˙A
156 44 eleq2d φuUinvgSuUinvgSugB|gsupp0˙A
157 oveq1 g=invgSugsupp0˙=invgSusupp0˙
158 157 eleq1d g=invgSugsupp0˙AinvgSusupp0˙A
159 158 elrab invgSugB|gsupp0˙AinvgSuBinvgSusupp0˙A
160 156 159 bitrdi φuUinvgSuUinvgSuBinvgSusupp0˙A
161 133 155 160 mpbir2and φuUinvgSuU
162 129 161 jca φuUvUu+SvUinvgSuU
163 162 ralrimiva φuUvUu+SvUinvgSuU
164 2 34 131 issubg2 SGrpUSubGrpSUBUuUvUu+SvUinvgSuU
165 130 164 syl φUSubGrpSUBUuUvUu+SvUinvgSuU
166 12 33 163 165 mpbir3and φUSubGrpS