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

Theorem mpllsslem 16180
 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.)
Hypotheses
Ref Expression
mplsubglem.s mPwSer
mplsubglem.b
mplsubglem.z
mplsubglem.d
mplsubglem.i
mplsubglem.0
mplsubglem.a
mplsubglem.y
mplsubglem.u
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 16134 . 2 Scalar
5 eqidd 2284 . 2
6 mplsubglem.b . . 3
76a1i 10 . 2
8 eqidd 2284 . 2
9 eqidd 2284 . 2
10 eqidd 2284 . 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
17 rnggrp 15346 . . . . 5
183, 17syl 15 . . . 4
191, 6, 11, 12, 2, 13, 14, 15, 16, 18mplsubglem 16179 . . 3 SubGrp
206subgss 14622 . . 3 SubGrp
2119, 20syl 15 . 2
22 eqid 2283 . . . 4
2322subg0cl 14629 . . 3 SubGrp
24 ne0i 3461 . . 3
2519, 23, 243syl 18 . 2
2619adantr 451 . . 3 SubGrp
27 eqid 2283 . . . . . 6
28 eqid 2283 . . . . . 6
293adantr 451 . . . . . 6
30 simprl 732 . . . . . 6
31 simprr 733 . . . . . . . 8
3216adantr 451 . . . . . . . . . 10
3332eleq2d 2350 . . . . . . . . 9
34 cnveq 4855 . . . . . . . . . . . 12
3534imaeq1d 5011 . . . . . . . . . . 11
3635eleq1d 2349 . . . . . . . . . 10
3736elrab 2923 . . . . . . . . 9
3833, 37syl6bb 252 . . . . . . . 8
3931, 38mpbid 201 . . . . . . 7
4039simpld 445 . . . . . 6
411, 27, 28, 6, 29, 30, 40psrvscacl 16138 . . . . 5
421, 28, 12, 6, 41psrelbas 16125 . . . . . . . 8
43 eqid 2283 . . . . . . . . . 10
4430adantr 451 . . . . . . . . . 10
4540adantr 451 . . . . . . . . . 10
46 eldifi 3298 . . . . . . . . . . 11
4746adantl 452 . . . . . . . . . 10
481, 27, 28, 6, 43, 12, 44, 45, 47psrvscaval 16137 . . . . . . . . 9
491, 28, 12, 6, 40psrelbas 16125 . . . . . . . . . . 11
50 ssid 3197 . . . . . . . . . . . 12
5150a1i 10 . . . . . . . . . . 11
5249, 51suppssr 5659 . . . . . . . . . 10
5352oveq2d 5874 . . . . . . . . 9
5428, 43, 11rngrz 15378 . . . . . . . . . . 11
5529, 30, 54syl2anc 642 . . . . . . . . . 10
5655adantr 451 . . . . . . . . 9
5748, 53, 563eqtrd 2319 . . . . . . . 8
5842, 57suppss 5658 . . . . . . 7
5939simprd 449 . . . . . . 7
60 ssexg 4160 . . . . . . 7
6158, 59, 60syl2anc 642 . . . . . 6
6215expr 598 . . . . . . . . . 10
6362alrimiv 1617 . . . . . . . . 9
6463ralrimiva 2626 . . . . . . . 8
6564adantr 451 . . . . . . 7
66 sseq2 3200 . . . . . . . . . 10
6766imbi1d 308 . . . . . . . . 9
6867albidv 1611 . . . . . . . 8
6968rspcv 2880 . . . . . . 7
7059, 65, 69sylc 56 . . . . . 6
71 sseq1 3199 . . . . . . . 8
72 eleq1 2343 . . . . . . . 8
7371, 72imbi12d 311 . . . . . . 7
7473spcgv 2868 . . . . . 6
7561, 70, 58, 74syl3c 57 . . . . 5
7632eleq2d 2350 . . . . . 6
77 cnveq 4855 . . . . . . . . 9
7877imaeq1d 5011 . . . . . . . 8
7978eleq1d 2349 . . . . . . 7
8079elrab 2923 . . . . . 6
8176, 80syl6bb 252 . . . . 5
8241, 75, 81mpbir2and 888 . . . 4