Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpllsslem Structured version   Unicode version

Theorem mpllsslem 17965
 Description: If is an ideal of subsets (a nonempty collection closed under subset and binary union) of the set of finite bags (the primary applications being and for some ), then the set of all power series whose coefficient functions are supported on an element of is a linear subspace of the set of all power series. (Contributed by Mario Carneiro, 12-Jan-2015.) (Revised by AV, 16-Jul-2019.)
Hypotheses
Ref Expression
mplsubglem.s mPwSer
mplsubglem.b
mplsubglem.z
mplsubglem.d
mplsubglem.i
mplsubglem.0
mplsubglem.a
mplsubglem.y
mplsubglem.u supp
mpllsslem.r
Assertion
Ref Expression
mpllsslem
Distinct variable groups:   ,,,,   ,,,,   ,,   ,   ,   ,,   ,,,
Allowed substitution hints:   (,)   (,)   (,,)   (,,,)   ()   (,,,)   (,,)   (,,,)

Proof of Theorem mpllsslem
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mplsubglem.s . . 3 mPwSer
2 mplsubglem.i . . 3
3 mpllsslem.r . . 3
41, 2, 3psrsca 17913 . 2 Scalar
5 eqidd 2442 . 2
6 mplsubglem.b . . 3
76a1i 11 . 2
8 eqidd 2442 . 2
9 eqidd 2442 . 2
10 eqidd 2442 . 2
11 mplsubglem.z . . . 4
12 mplsubglem.d . . . 4
13 mplsubglem.0 . . . 4
14 mplsubglem.a . . . 4
15 mplsubglem.y . . . 4
16 mplsubglem.u . . . 4 supp
17 ringgrp 17074 . . . . 5
183, 17syl 16 . . . 4
191, 6, 11, 12, 2, 13, 14, 15, 16, 18mplsubglem 17964 . . 3 SubGrp
206subgss 16073 . . 3 SubGrp
2119, 20syl 16 . 2
22 eqid 2441 . . . 4
2322subg0cl 16080 . . 3 SubGrp
24 ne0i 3774 . . 3
2519, 23, 243syl 20 . 2
2619adantr 465 . . 3 SubGrp
27 eqid 2441 . . . . . 6
28 eqid 2441 . . . . . 6
293adantr 465 . . . . . 6
30 simprl 755 . . . . . 6
31 simprr 756 . . . . . . . 8
3216adantr 465 . . . . . . . . . 10 supp
3332eleq2d 2511 . . . . . . . . 9 supp
34 oveq1 6285 . . . . . . . . . . 11 supp supp
3534eleq1d 2510 . . . . . . . . . 10 supp supp
3635elrab 3241 . . . . . . . . 9 supp supp
3733, 36syl6bb 261 . . . . . . . 8 supp
3831, 37mpbid 210 . . . . . . 7 supp
3938simpld 459 . . . . . 6
401, 27, 28, 6, 29, 30, 39psrvscacl 17917 . . . . 5
41 ovex 6306 . . . . . . 7 supp
4241a1i 11 . . . . . 6 supp
4338simprd 463 . . . . . . 7 supp
4415expr 615 . . . . . . . . . 10
4544alrimiv 1704 . . . . . . . . 9
4645ralrimiva 2855 . . . . . . . 8
4746adantr 465 . . . . . . 7
48 sseq2 3509 . . . . . . . . . 10 supp supp
4948imbi1d 317 . . . . . . . . 9 supp supp
5049albidv 1698 . . . . . . . 8 supp supp
5150rspcv 3190 . . . . . . 7 supp supp
5243, 47, 51sylc 60 . . . . . 6 supp
531, 28, 12, 6, 40psrelbas 17903 . . . . . . 7
54 eqid 2441 . . . . . . . . 9
5530adantr 465 . . . . . . . . 9 supp
5639adantr 465 . . . . . . . . 9 supp
57 eldifi 3609 . . . . . . . . . 10 supp
5857adantl 466 . . . . . . . . 9 supp
591, 27, 28, 6, 54, 12, 55, 56, 58psrvscaval 17916 . . . . . . . 8 supp
601, 28, 12, 6, 39psrelbas 17903 . . . . . . . . . 10
61 ssid 3506 . . . . . . . . . . 11 supp supp
6261a1i 11 . . . . . . . . . 10 supp supp
63 ovex 6306 . . . . . . . . . . . 12
6412, 63rabex2 4587 . . . . . . . . . . 11
6564a1i 11 . . . . . . . . . 10
66 fvex 5863 . . . . . . . . . . . 12
6711, 66eqeltri 2525 . . . . . . . . . . 11
6867a1i 11 . . . . . . . . . 10
6960, 62, 65, 68suppssr 6930 . . . . . . . . 9 supp
7069oveq2d 6294 . . . . . . . 8 supp
7128, 54, 11ringrz 17107 . . . . . . . . . 10
7229, 30, 71syl2anc 661 . . . . . . . . 9
7372adantr 465 . . . . . . . 8 supp
7459, 70, 733eqtrd 2486 . . . . . . 7 supp
7553, 74suppss 6929 . . . . . 6 supp supp
76 sseq1 3508 . . . . . . . 8 supp supp supp supp
77 eleq1 2513 . . . . . . . 8 supp supp
7876, 77imbi12d 320 . . . . . . 7 supp supp supp supp supp
7978spcgv 3178 . . . . . 6 supp supp supp supp supp
8042, 52, 75, 79syl3c 61 . . . . 5 supp
8132eleq2d 2511 . . . . . 6 supp
82 oveq1 6285 . . . . . . . 8 supp supp
8382eleq1d 2510 . . . . . . 7 supp supp
8483elrab 3241 . . . . . 6 supp supp
8581, 84syl6bb 261 . . . . 5 supp
8640, 80, 85mpbir2and 920 . . . 4