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 = I mPwSer R
mplsubglem.b B = Base S
mplsubglem.z 0 ˙ = 0 R
mplsubglem.d D = f 0 I | f -1 Fin
mplsubglem.i φ I W
mplsubglem.0 φ A
mplsubglem.a φ x A y A x y A
mplsubglem.y φ x A y x y A
mplsubglem.u φ U = g B | g supp 0 ˙ A
mplsubglem.r φ R Grp
Assertion mplsubglem φ U SubGrp S

Proof

Step Hyp Ref Expression
1 mplsubglem.s S = I mPwSer R
2 mplsubglem.b B = Base S
3 mplsubglem.z 0 ˙ = 0 R
4 mplsubglem.d D = f 0 I | f -1 Fin
5 mplsubglem.i φ I W
6 mplsubglem.0 φ A
7 mplsubglem.a φ x A y A x y A
8 mplsubglem.y φ x A y x y A
9 mplsubglem.u φ U = g B | g supp 0 ˙ A
10 mplsubglem.r φ R Grp
11 ssrab2 g B | g supp 0 ˙ A B
12 9 11 eqsstrdi φ U B
13 1 5 10 4 3 2 psr0cl φ D × 0 ˙ B
14 eqid Base R = Base R
15 14 3 grpidcl R Grp 0 ˙ Base R
16 fconst6g 0 ˙ Base R D × 0 ˙ : D Base R
17 10 15 16 3syl φ D × 0 ˙ : D Base R
18 eldifi u D u D
19 3 fvexi 0 ˙ V
20 19 fvconst2 u D D × 0 ˙ u = 0 ˙
21 18 20 syl u D D × 0 ˙ u = 0 ˙
22 21 adantl φ u D D × 0 ˙ u = 0 ˙
23 17 22 suppss φ D × 0 ˙ supp 0 ˙
24 ss0 D × 0 ˙ supp 0 ˙ D × 0 ˙ supp 0 ˙ =
25 23 24 syl φ D × 0 ˙ supp 0 ˙ =
26 25 6 eqeltrd φ D × 0 ˙ supp 0 ˙ A
27 9 eleq2d φ D × 0 ˙ U D × 0 ˙ g B | g supp 0 ˙ A
28 oveq1 g = D × 0 ˙ g supp 0 ˙ = D × 0 ˙ supp 0 ˙
29 28 eleq1d g = D × 0 ˙ g supp 0 ˙ A D × 0 ˙ supp 0 ˙ A
30 29 elrab D × 0 ˙ g B | g supp 0 ˙ A D × 0 ˙ B D × 0 ˙ supp 0 ˙ A
31 27 30 bitrdi φ D × 0 ˙ U D × 0 ˙ B D × 0 ˙ supp 0 ˙ A
32 13 26 31 mpbir2and φ D × 0 ˙ U
33 32 ne0d φ U
34 eqid + S = + S
35 10 grpmgmd φ R Mgm
36 35 ad2antrr φ u U v U R Mgm
37 9 eleq2d φ u U u g B | g supp 0 ˙ A
38 oveq1 g = u g supp 0 ˙ = u supp 0 ˙
39 38 eleq1d g = u g supp 0 ˙ A u supp 0 ˙ A
40 39 elrab u g B | g supp 0 ˙ A u B u supp 0 ˙ A
41 37 40 bitrdi φ u U u B u supp 0 ˙ A
42 41 biimpa φ u U u B u supp 0 ˙ A
43 42 simpld φ u U u B
44 43 adantr φ u U v U u B
45 9 adantr φ u U U = g B | g supp 0 ˙ A
46 45 eleq2d φ u U v U v g B | g supp 0 ˙ A
47 oveq1 g = v g supp 0 ˙ = v supp 0 ˙
48 47 eleq1d g = v g supp 0 ˙ A v supp 0 ˙ A
49 48 elrab v g B | g supp 0 ˙ A v B v supp 0 ˙ A
50 46 49 bitrdi φ u U v U v B v supp 0 ˙ A
51 50 biimpa φ u U v U v B v supp 0 ˙ A
52 51 simpld φ u U v U v B
53 1 2 34 36 44 52 psraddcl φ u U v U u + S v B
54 ovexd φ u U v U u + S v supp 0 ˙ V
55 sseq2 x = supp 0 ˙ u supp 0 ˙ v y x y supp 0 ˙ u supp 0 ˙ v
56 55 imbi1d x = supp 0 ˙ u supp 0 ˙ v y x y A y supp 0 ˙ u supp 0 ˙ v y A
57 56 albidv x = supp 0 ˙ u supp 0 ˙ v y y x y A y y supp 0 ˙ u supp 0 ˙ v y A
58 8 expr φ x A y x y A
59 58 alrimiv φ x A y y x y A
60 59 ralrimiva φ x A y y x y A
61 60 ad2antrr φ u U v U x A y y x y A
62 42 simprd φ u U u supp 0 ˙ A
63 62 adantr φ u U v U u supp 0 ˙ A
64 51 simprd φ u U v U v supp 0 ˙ A
65 7 ralrimivva φ x A y A x y A
66 65 ad2antrr φ u U v U x A y A x y A
67 uneq1 x = u supp 0 ˙ x y = supp 0 ˙ u y
68 67 eleq1d x = u supp 0 ˙ x y A supp 0 ˙ u y A
69 uneq2 y = v supp 0 ˙ supp 0 ˙ u y = supp 0 ˙ u supp 0 ˙ v
70 69 eleq1d y = v supp 0 ˙ supp 0 ˙ u y A supp 0 ˙ u supp 0 ˙ v A
71 68 70 rspc2va u supp 0 ˙ A v supp 0 ˙ A x A y A x y A supp 0 ˙ u supp 0 ˙ v A
72 63 64 66 71 syl21anc φ u U v U supp 0 ˙ u supp 0 ˙ v A
73 57 61 72 rspcdva φ u U v U y y supp 0 ˙ u supp 0 ˙ v y A
74 1 14 4 2 53 psrelbas φ u U v U u + S v : D Base R
75 eqid + R = + R
76 1 2 75 34 44 52 psradd φ u U v U u + S v = u + R f v
77 76 fveq1d φ u U v U u + S v k = u + R f v k
78 77 adantr φ u U v U k D supp 0 ˙ u supp 0 ˙ v u + S v k = u + R f v k
79 eldifi k D supp 0 ˙ u supp 0 ˙ v k D
80 1 14 4 2 43 psrelbas φ u U u : D Base R
81 80 adantr φ u U v U u : D Base R
82 81 ffnd φ u U v U u Fn D
83 1 14 4 2 52 psrelbas φ u U v U v : D Base R
84 83 ffnd φ u U v U v Fn D
85 ovex 0 I V
86 4 85 rabex2 D V
87 86 a1i φ u U v U D V
88 inidm D D = D
89 eqidd φ u U v U k D u k = u k
90 eqidd φ u U v U k D v k = v k
91 82 84 87 87 88 89 90 ofval φ u U v U k D u + R f v k = u k + R v k
92 79 91 sylan2 φ u U v U k D supp 0 ˙ u supp 0 ˙ v u + R f v k = u k + R v k
93 ssun1 u supp 0 ˙ supp 0 ˙ u supp 0 ˙ v
94 sscon u supp 0 ˙ supp 0 ˙ u supp 0 ˙ v D supp 0 ˙ u supp 0 ˙ v D supp 0 ˙ u
95 93 94 ax-mp D supp 0 ˙ u supp 0 ˙ v D supp 0 ˙ u
96 95 sseli k D supp 0 ˙ u supp 0 ˙ v k D supp 0 ˙ u
97 ssidd φ u U u supp 0 ˙ u supp 0 ˙
98 86 a1i φ u U D V
99 19 a1i φ u U 0 ˙ V
100 80 97 98 99 suppssr φ u U k D supp 0 ˙ u u k = 0 ˙
101 100 adantlr φ u U v U k D supp 0 ˙ u u k = 0 ˙
102 96 101 sylan2 φ u U v U k D supp 0 ˙ u supp 0 ˙ v u k = 0 ˙
103 ssun2 v supp 0 ˙ supp 0 ˙ u supp 0 ˙ v
104 sscon v supp 0 ˙ supp 0 ˙ u supp 0 ˙ v D supp 0 ˙ u supp 0 ˙ v D supp 0 ˙ v
105 103 104 ax-mp D supp 0 ˙ u supp 0 ˙ v D supp 0 ˙ v
106 105 sseli k D supp 0 ˙ u supp 0 ˙ v k D supp 0 ˙ v
107 ssidd φ u U v U v supp 0 ˙ v supp 0 ˙
108 19 a1i φ u U v U 0 ˙ V
109 83 107 87 108 suppssr φ u U v U k D supp 0 ˙ v v k = 0 ˙
110 106 109 sylan2 φ u U v U k D supp 0 ˙ u supp 0 ˙ v v k = 0 ˙
111 102 110 oveq12d φ u U v U k D supp 0 ˙ u supp 0 ˙ v u k + R v k = 0 ˙ + R 0 ˙
112 10 ad2antrr φ u U v U R Grp
113 14 75 3 grplid R Grp 0 ˙ Base R 0 ˙ + R 0 ˙ = 0 ˙
114 112 15 113 syl2anc2 φ u U v U 0 ˙ + R 0 ˙ = 0 ˙
115 114 adantr φ u U v U k D supp 0 ˙ u supp 0 ˙ v 0 ˙ + R 0 ˙ = 0 ˙
116 111 115 eqtrd φ u U v U k D supp 0 ˙ u supp 0 ˙ v u k + R v k = 0 ˙
117 78 92 116 3eqtrd φ u U v U k D supp 0 ˙ u supp 0 ˙ v u + S v k = 0 ˙
118 74 117 suppss φ u U v U u + S v supp 0 ˙ supp 0 ˙ u supp 0 ˙ v
119 sseq1 y = u + S v supp 0 ˙ y supp 0 ˙ u supp 0 ˙ v u + S v supp 0 ˙ supp 0 ˙ u supp 0 ˙ v
120 eleq1 y = u + S v supp 0 ˙ y A u + S v supp 0 ˙ A
121 119 120 imbi12d y = u + S v supp 0 ˙ y supp 0 ˙ u supp 0 ˙ v y A u + S v supp 0 ˙ supp 0 ˙ u supp 0 ˙ v u + S v supp 0 ˙ A
122 121 spcgv u + S v supp 0 ˙ V y y supp 0 ˙ u supp 0 ˙ v y A u + S v supp 0 ˙ supp 0 ˙ u supp 0 ˙ v u + S v supp 0 ˙ A
123 54 73 118 122 syl3c φ u U v U u + S v supp 0 ˙ A
124 9 ad2antrr φ u U v U U = g B | g supp 0 ˙ A
125 124 eleq2d φ u U v U u + S v U u + S v g B | g supp 0 ˙ A
126 oveq1 g = u + S v g supp 0 ˙ = u + S v supp 0 ˙
127 126 eleq1d g = u + S v g supp 0 ˙ A u + S v supp 0 ˙ A
128 127 elrab u + S v g B | g supp 0 ˙ A u + S v B u + S v supp 0 ˙ A
129 125 128 bitrdi φ u U v U u + S v U u + S v B u + S v supp 0 ˙ A
130 53 123 129 mpbir2and φ u U v U u + S v U
131 130 ralrimiva φ u U v U u + S v U
132 1 5 10 psrgrp φ S Grp
133 eqid inv g S = inv g S
134 2 133 grpinvcl S Grp u B inv g S u B
135 132 43 134 syl2an2r φ u U inv g S u B
136 ovexd φ u U inv g S u supp 0 ˙ V
137 sseq2 x = u supp 0 ˙ y x y u supp 0 ˙
138 137 imbi1d x = u supp 0 ˙ y x y A y u supp 0 ˙ y A
139 138 albidv x = u supp 0 ˙ y y x y A y y u supp 0 ˙ y A
140 60 adantr φ u U x A y y x y A
141 139 140 62 rspcdva φ u U y y u supp 0 ˙ y A
142 5 adantr φ u U I W
143 10 adantr φ u U R Grp
144 eqid inv g R = inv g R
145 1 142 143 4 144 2 133 43 psrneg φ u U inv g S u = inv g R u
146 145 oveq1d φ u U inv g S u supp 0 ˙ = inv g R u supp 0 ˙
147 14 144 grpinvfn inv g R Fn Base R
148 147 a1i φ u U inv g R Fn Base R
149 3 144 grpinvid R Grp inv g R 0 ˙ = 0 ˙
150 143 149 syl φ u U inv g R 0 ˙ = 0 ˙
151 148 80 98 99 150 suppcoss φ u U inv g R u supp 0 ˙ u supp 0 ˙
152 146 151 eqsstrd φ u U inv g S u supp 0 ˙ u supp 0 ˙
153 sseq1 y = inv g S u supp 0 ˙ y u supp 0 ˙ inv g S u supp 0 ˙ u supp 0 ˙
154 eleq1 y = inv g S u supp 0 ˙ y A inv g S u supp 0 ˙ A
155 153 154 imbi12d y = inv g S u supp 0 ˙ y u supp 0 ˙ y A inv g S u supp 0 ˙ u supp 0 ˙ inv g S u supp 0 ˙ A
156 155 spcgv inv g S u supp 0 ˙ V y y u supp 0 ˙ y A inv g S u supp 0 ˙ u supp 0 ˙ inv g S u supp 0 ˙ A
157 136 141 152 156 syl3c φ u U inv g S u supp 0 ˙ A
158 45 eleq2d φ u U inv g S u U inv g S u g B | g supp 0 ˙ A
159 oveq1 g = inv g S u g supp 0 ˙ = inv g S u supp 0 ˙
160 159 eleq1d g = inv g S u g supp 0 ˙ A inv g S u supp 0 ˙ A
161 160 elrab inv g S u g B | g supp 0 ˙ A inv g S u B inv g S u supp 0 ˙ A
162 158 161 bitrdi φ u U inv g S u U inv g S u B inv g S u supp 0 ˙ A
163 135 157 162 mpbir2and φ u U inv g S u U
164 131 163 jca φ u U v U u + S v U inv g S u U
165 164 ralrimiva φ u U v U u + S v U inv g S u U
166 2 34 133 issubg2 S Grp U SubGrp S U B U u U v U u + S v U inv g S u U
167 132 166 syl φ U SubGrp S U B U u U v U u + S v U inv g S u U
168 12 33 165 167 mpbir3and φ U SubGrp S