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