Metamath Proof Explorer

Theorem mpllsslem

Description: If A is an ideal of subsets (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 linear subspace 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. = ( 0g ` R )
mplsubglem.d 
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
mplsubglem.i 
|- ( ph -> I e. W )
mplsubglem.0 
|- ( ph -> (/) e. A )
mplsubglem.a 
|- ( ( ph /\ ( x e. A /\ y e. A ) ) -> ( x u. y ) e. A )
mplsubglem.y 
|- ( ( ph /\ ( x e. A /\ y C_ x ) ) -> y e. A )
mplsubglem.u 
|- ( ph -> U = { g e. B | ( g supp .0. ) e. A } )
mpllsslem.r 
|- ( ph -> R e. Ring )
Assertion mpllsslem 
|- ( ph -> U e. ( LSubSp ` S ) )

Proof

Step Hyp Ref Expression
1 mplsubglem.s 
 |-  S = ( I mPwSer R )
2 mplsubglem.b 
 |-  B = ( Base ` S )
3 mplsubglem.z 
 |-  .0. = ( 0g ` R )
4 mplsubglem.d 
 |-  D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
5 mplsubglem.i 
 |-  ( ph -> I e. W )
6 mplsubglem.0 
 |-  ( ph -> (/) e. A )
7 mplsubglem.a 
 |-  ( ( ph /\ ( x e. A /\ y e. A ) ) -> ( x u. y ) e. A )
8 mplsubglem.y 
 |-  ( ( ph /\ ( x e. A /\ y C_ x ) ) -> y e. A )
9 mplsubglem.u 
 |-  ( ph -> U = { g e. B | ( g supp .0. ) e. A } )
10 mpllsslem.r 
 |-  ( ph -> R e. Ring )
11 1 5 10 psrsca 
 |-  ( ph -> R = ( Scalar ` S ) )
12 eqidd 
 |-  ( ph -> ( Base ` R ) = ( Base ` R ) )
13 2 a1i 
 |-  ( ph -> B = ( Base ` S ) )
14 eqidd 
 |-  ( ph -> ( +g ` S ) = ( +g ` S ) )
15 eqidd 
 |-  ( ph -> ( .s ` S ) = ( .s ` S ) )
16 eqidd 
 |-  ( ph -> ( LSubSp ` S ) = ( LSubSp ` S ) )
17 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
18 10 17 syl 
 |-  ( ph -> R e. Grp )
19 1 2 3 4 5 6 7 8 9 18 mplsubglem 
 |-  ( ph -> U e. ( SubGrp ` S ) )
20 2 subgss 
 |-  ( U e. ( SubGrp ` S ) -> U C_ B )
21 19 20 syl 
 |-  ( ph -> U C_ B )
22 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
23 22 subg0cl 
 |-  ( U e. ( SubGrp ` S ) -> ( 0g ` S ) e. U )
24 ne0i 
 |-  ( ( 0g ` S ) e. U -> U =/= (/) )
25 19 23 24 3syl 
 |-  ( ph -> U =/= (/) )
26 19 adantr 
 |-  ( ( ph /\ ( u e. ( Base ` R ) /\ v e. U /\ w e. U ) ) -> U e. ( SubGrp ` S ) )
27 eqid 
 |-  ( .s ` S ) = ( .s ` S )
28 eqid 
 |-  ( Base ` R ) = ( Base ` R )
29 10 adantr 
 |-  ( ( ph /\ ( u e. ( Base ` R ) /\ v e. U ) ) -> R e. Ring )
30 simprl 
 |-  ( ( ph /\ ( u e. ( Base ` R ) /\ v e. U ) ) -> u e. ( Base ` R ) )
31 simprr 
 |-  ( ( ph /\ ( u e. ( Base ` R ) /\ v e. U ) ) -> v e. U )
32 9 adantr 
 |-  ( ( ph /\ ( u e. ( Base ` R ) /\ v e. U ) ) -> U = { g e. B | ( g supp .0. ) e. A } )
33 32 eleq2d 
 |-  ( ( ph /\ ( u e. ( Base ` R ) /\ v e. U ) ) -> ( v e. U <-> v e. { g e. B | ( g supp .0. ) e. A } ) )
34 oveq1 
 |-  ( g = v -> ( g supp .0. ) = ( v supp .0. ) )
35 34 eleq1d 
 |-  ( g = v -> ( ( g supp .0. ) e. A <-> ( v supp .0. ) e. A ) )
36 35 elrab 
 |-  ( v e. { g e. B | ( g supp .0. ) e. A } <-> ( v e. B /\ ( v supp .0. ) e. A ) )
37 33 36 bitrdi 
 |-  ( ( ph /\ ( u e. ( Base ` R ) /\ v e. U ) ) -> ( v e. U <-> ( v e. B /\ ( v supp .0. ) e. A ) ) )
38 31 37 mpbid 
 |-  ( ( ph /\ ( u e. ( Base ` R ) /\ v e. U ) ) -> ( v e. B /\ ( v supp .0. ) e. A ) )
39 38 simpld 
 |-  ( ( ph /\ ( u e. ( Base ` R ) /\ v e. U ) ) -> v e. B )
40 1 27 28 2 29 30 39 psrvscacl 
 |-  ( ( ph /\ ( u e. ( Base ` R ) /\ v e. U ) ) -> ( u ( .s ` S ) v ) e. B )
41 ovex 
 |-  ( ( u ( .s ` S ) v ) supp .0. ) e. _V
42 41 a1i 
 |-  ( ( ph /\ ( u e. ( Base ` R ) /\ v e. U ) ) -> ( ( u ( .s ` S ) v ) supp .0. ) e. _V )
43 sseq2 
 |-  ( x = ( v supp .0. ) -> ( y C_ x <-> y C_ ( v supp .0. ) ) )
44 43 imbi1d 
 |-  ( x = ( v supp .0. ) -> ( ( y C_ x -> y e. A ) <-> ( y C_ ( v supp .0. ) -> y e. A ) ) )
45 44 albidv 
 |-  ( x = ( v supp .0. ) -> ( A. y ( y C_ x -> y e. A ) <-> A. y ( y C_ ( v supp .0. ) -> y e. A ) ) )
46 8 expr 
 |-  ( ( ph /\ x e. A ) -> ( y C_ x -> y e. A ) )
47 46 alrimiv 
 |-  ( ( ph /\ x e. A ) -> A. y ( y C_ x -> y e. A ) )
48 47 ralrimiva 
 |-  ( ph -> A. x e. A A. y ( y C_ x -> y e. A ) )
49 48 adantr 
 |-  ( ( ph /\ ( u e. ( Base ` R ) /\ v e. U ) ) -> A. x e. A A. y ( y C_ x -> y e. A ) )
50 38 simprd 
 |-  ( ( ph /\ ( u e. ( Base ` R ) /\ v e. U ) ) -> ( v supp .0. ) e. A )
51 45 49 50 rspcdva 
 |-  ( ( ph /\ ( u e. ( Base ` R ) /\ v e. U ) ) -> A. y ( y C_ ( v supp .0. ) -> y e. A ) )
52 1 28 4 2 40 psrelbas 
 |-  ( ( ph /\ ( u e. ( Base ` R ) /\ v e. U ) ) -> ( u ( .s ` S ) v ) : D --> ( Base ` R ) )
53 eqid 
 |-  ( .r ` R ) = ( .r ` R )
54 30 adantr 
 |-  ( ( ( ph /\ ( u e. ( Base ` R ) /\ v e. U ) ) /\ k e. ( D \ ( v supp .0. ) ) ) -> u e. ( Base ` R ) )
55 39 adantr 
 |-  ( ( ( ph /\ ( u e. ( Base ` R ) /\ v e. U ) ) /\ k e. ( D \ ( v supp .0. ) ) ) -> v e. B )
56 eldifi 
 |-  ( k e. ( D \ ( v supp .0. ) ) -> k e. D )
57 56 adantl 
 |-  ( ( ( ph /\ ( u e. ( Base ` R ) /\ v e. U ) ) /\ k e. ( D \ ( v supp .0. ) ) ) -> k e. D )
58 1 27 28 2 53 4 54 55 57 psrvscaval 
 |-  ( ( ( ph /\ ( u e. ( Base ` R ) /\ v e. U ) ) /\ k e. ( D \ ( v supp .0. ) ) ) -> ( ( u ( .s ` S ) v ) ` k ) = ( u ( .r ` R ) ( v ` k ) ) )
59 1 28 4 2 39 psrelbas 
 |-  ( ( ph /\ ( u e. ( Base ` R ) /\ v e. U ) ) -> v : D --> ( Base ` R ) )
60 ssidd 
 |-  ( ( ph /\ ( u e. ( Base ` R ) /\ v e. U ) ) -> ( v supp .0. ) C_ ( v supp .0. ) )
61 ovex 
 |-  ( NN0 ^m I ) e. _V
62 4 61 rabex2 
 |-  D e. _V
63 62 a1i 
 |-  ( ( ph /\ ( u e. ( Base ` R ) /\ v e. U ) ) -> D e. _V )
64 3 fvexi 
 |-  .0. e. _V
65 64 a1i 
 |-  ( ( ph /\ ( u e. ( Base ` R ) /\ v e. U ) ) -> .0. e. _V )
66 59 60 63 65 suppssr 
 |-  ( ( ( ph /\ ( u e. ( Base ` R ) /\ v e. U ) ) /\ k e. ( D \ ( v supp .0. ) ) ) -> ( v ` k ) = .0. )
67 66 oveq2d 
 |-  ( ( ( ph /\ ( u e. ( Base ` R ) /\ v e. U ) ) /\ k e. ( D \ ( v supp .0. ) ) ) -> ( u ( .r ` R ) ( v ` k ) ) = ( u ( .r ` R ) .0. ) )
68 28 53 3 ringrz 
 |-  ( ( R e. Ring /\ u e. ( Base ` R ) ) -> ( u ( .r ` R ) .0. ) = .0. )
69 10 30 68 syl2an2r 
 |-  ( ( ph /\ ( u e. ( Base ` R ) /\ v e. U ) ) -> ( u ( .r ` R ) .0. ) = .0. )
70 69 adantr 
 |-  ( ( ( ph /\ ( u e. ( Base ` R ) /\ v e. U ) ) /\ k e. ( D \ ( v supp .0. ) ) ) -> ( u ( .r ` R ) .0. ) = .0. )
71 58 67 70 3eqtrd 
 |-  ( ( ( ph /\ ( u e. ( Base ` R ) /\ v e. U ) ) /\ k e. ( D \ ( v supp .0. ) ) ) -> ( ( u ( .s ` S ) v ) ` k ) = .0. )
72 52 71 suppss 
 |-  ( ( ph /\ ( u e. ( Base ` R ) /\ v e. U ) ) -> ( ( u ( .s ` S ) v ) supp .0. ) C_ ( v supp .0. ) )
73 sseq1 
 |-  ( y = ( ( u ( .s ` S ) v ) supp .0. ) -> ( y C_ ( v supp .0. ) <-> ( ( u ( .s ` S ) v ) supp .0. ) C_ ( v supp .0. ) ) )
74 eleq1 
 |-  ( y = ( ( u ( .s ` S ) v ) supp .0. ) -> ( y e. A <-> ( ( u ( .s ` S ) v ) supp .0. ) e. A ) )
75 73 74 imbi12d 
 |-  ( y = ( ( u ( .s ` S ) v ) supp .0. ) -> ( ( y C_ ( v supp .0. ) -> y e. A ) <-> ( ( ( u ( .s ` S ) v ) supp .0. ) C_ ( v supp .0. ) -> ( ( u ( .s ` S ) v ) supp .0. ) e. A ) ) )
76 75 spcgv 
 |-  ( ( ( u ( .s ` S ) v ) supp .0. ) e. _V -> ( A. y ( y C_ ( v supp .0. ) -> y e. A ) -> ( ( ( u ( .s ` S ) v ) supp .0. ) C_ ( v supp .0. ) -> ( ( u ( .s ` S ) v ) supp .0. ) e. A ) ) )
77 42 51 72 76 syl3c 
 |-  ( ( ph /\ ( u e. ( Base ` R ) /\ v e. U ) ) -> ( ( u ( .s ` S ) v ) supp .0. ) e. A )
78 32 eleq2d 
 |-  ( ( ph /\ ( u e. ( Base ` R ) /\ v e. U ) ) -> ( ( u ( .s ` S ) v ) e. U <-> ( u ( .s ` S ) v ) e. { g e. B | ( g supp .0. ) e. A } ) )
79 oveq1 
 |-  ( g = ( u ( .s ` S ) v ) -> ( g supp .0. ) = ( ( u ( .s ` S ) v ) supp .0. ) )
80 79 eleq1d 
 |-  ( g = ( u ( .s ` S ) v ) -> ( ( g supp .0. ) e. A <-> ( ( u ( .s ` S ) v ) supp .0. ) e. A ) )
81 80 elrab 
 |-  ( ( u ( .s ` S ) v ) e. { g e. B | ( g supp .0. ) e. A } <-> ( ( u ( .s ` S ) v ) e. B /\ ( ( u ( .s ` S ) v ) supp .0. ) e. A ) )
82 78 81 bitrdi 
 |-  ( ( ph /\ ( u e. ( Base ` R ) /\ v e. U ) ) -> ( ( u ( .s ` S ) v ) e. U <-> ( ( u ( .s ` S ) v ) e. B /\ ( ( u ( .s ` S ) v ) supp .0. ) e. A ) ) )
83 40 77 82 mpbir2and 
 |-  ( ( ph /\ ( u e. ( Base ` R ) /\ v e. U ) ) -> ( u ( .s ` S ) v ) e. U )
84 83 3adantr3 
 |-  ( ( ph /\ ( u e. ( Base ` R ) /\ v e. U /\ w e. U ) ) -> ( u ( .s ` S ) v ) e. U )
85 simpr3 
 |-  ( ( ph /\ ( u e. ( Base ` R ) /\ v e. U /\ w e. U ) ) -> w e. U )
86 eqid 
 |-  ( +g ` S ) = ( +g ` S )
87 86 subgcl 
 |-  ( ( U e. ( SubGrp ` S ) /\ ( u ( .s ` S ) v ) e. U /\ w e. U ) -> ( ( u ( .s ` S ) v ) ( +g ` S ) w ) e. U )
88 26 84 85 87 syl3anc 
 |-  ( ( ph /\ ( u e. ( Base ` R ) /\ v e. U /\ w e. U ) ) -> ( ( u ( .s ` S ) v ) ( +g ` S ) w ) e. U )
89 11 12 13 14 15 16 21 25 88 islssd 
 |-  ( ph -> U e. ( LSubSp ` S ) )