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 𝑆 = ( 𝐼 mPwSer 𝑅 )
mplsubglem.b 𝐵 = ( Base ‘ 𝑆 )
mplsubglem.z 0 = ( 0g𝑅 )
mplsubglem.d 𝐷 = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin }
mplsubglem.i ( 𝜑𝐼𝑊 )
mplsubglem.0 ( 𝜑 → ∅ ∈ 𝐴 )
mplsubglem.a ( ( 𝜑 ∧ ( 𝑥𝐴𝑦𝐴 ) ) → ( 𝑥𝑦 ) ∈ 𝐴 )
mplsubglem.y ( ( 𝜑 ∧ ( 𝑥𝐴𝑦𝑥 ) ) → 𝑦𝐴 )
mplsubglem.u ( 𝜑𝑈 = { 𝑔𝐵 ∣ ( 𝑔 supp 0 ) ∈ 𝐴 } )
mpllsslem.r ( 𝜑𝑅 ∈ Ring )
Assertion mpllsslem ( 𝜑𝑈 ∈ ( LSubSp ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 mplsubglem.s 𝑆 = ( 𝐼 mPwSer 𝑅 )
2 mplsubglem.b 𝐵 = ( Base ‘ 𝑆 )
3 mplsubglem.z 0 = ( 0g𝑅 )
4 mplsubglem.d 𝐷 = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin }
5 mplsubglem.i ( 𝜑𝐼𝑊 )
6 mplsubglem.0 ( 𝜑 → ∅ ∈ 𝐴 )
7 mplsubglem.a ( ( 𝜑 ∧ ( 𝑥𝐴𝑦𝐴 ) ) → ( 𝑥𝑦 ) ∈ 𝐴 )
8 mplsubglem.y ( ( 𝜑 ∧ ( 𝑥𝐴𝑦𝑥 ) ) → 𝑦𝐴 )
9 mplsubglem.u ( 𝜑𝑈 = { 𝑔𝐵 ∣ ( 𝑔 supp 0 ) ∈ 𝐴 } )
10 mpllsslem.r ( 𝜑𝑅 ∈ Ring )
11 1 5 10 psrsca ( 𝜑𝑅 = ( Scalar ‘ 𝑆 ) )
12 eqidd ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) )
13 2 a1i ( 𝜑𝐵 = ( Base ‘ 𝑆 ) )
14 eqidd ( 𝜑 → ( +g𝑆 ) = ( +g𝑆 ) )
15 eqidd ( 𝜑 → ( ·𝑠𝑆 ) = ( ·𝑠𝑆 ) )
16 eqidd ( 𝜑 → ( LSubSp ‘ 𝑆 ) = ( LSubSp ‘ 𝑆 ) )
17 ringgrp ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
18 10 17 syl ( 𝜑𝑅 ∈ Grp )
19 1 2 3 4 5 6 7 8 9 18 mplsubglem ( 𝜑𝑈 ∈ ( SubGrp ‘ 𝑆 ) )
20 2 subgss ( 𝑈 ∈ ( SubGrp ‘ 𝑆 ) → 𝑈𝐵 )
21 19 20 syl ( 𝜑𝑈𝐵 )
22 eqid ( 0g𝑆 ) = ( 0g𝑆 )
23 22 subg0cl ( 𝑈 ∈ ( SubGrp ‘ 𝑆 ) → ( 0g𝑆 ) ∈ 𝑈 )
24 ne0i ( ( 0g𝑆 ) ∈ 𝑈𝑈 ≠ ∅ )
25 19 23 24 3syl ( 𝜑𝑈 ≠ ∅ )
26 19 adantr ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣𝑈𝑤𝑈 ) ) → 𝑈 ∈ ( SubGrp ‘ 𝑆 ) )
27 eqid ( ·𝑠𝑆 ) = ( ·𝑠𝑆 )
28 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
29 10 adantr ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣𝑈 ) ) → 𝑅 ∈ Ring )
30 simprl ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣𝑈 ) ) → 𝑢 ∈ ( Base ‘ 𝑅 ) )
31 simprr ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣𝑈 ) ) → 𝑣𝑈 )
32 9 adantr ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣𝑈 ) ) → 𝑈 = { 𝑔𝐵 ∣ ( 𝑔 supp 0 ) ∈ 𝐴 } )
33 32 eleq2d ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣𝑈 ) ) → ( 𝑣𝑈𝑣 ∈ { 𝑔𝐵 ∣ ( 𝑔 supp 0 ) ∈ 𝐴 } ) )
34 oveq1 ( 𝑔 = 𝑣 → ( 𝑔 supp 0 ) = ( 𝑣 supp 0 ) )
35 34 eleq1d ( 𝑔 = 𝑣 → ( ( 𝑔 supp 0 ) ∈ 𝐴 ↔ ( 𝑣 supp 0 ) ∈ 𝐴 ) )
36 35 elrab ( 𝑣 ∈ { 𝑔𝐵 ∣ ( 𝑔 supp 0 ) ∈ 𝐴 } ↔ ( 𝑣𝐵 ∧ ( 𝑣 supp 0 ) ∈ 𝐴 ) )
37 33 36 bitrdi ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣𝑈 ) ) → ( 𝑣𝑈 ↔ ( 𝑣𝐵 ∧ ( 𝑣 supp 0 ) ∈ 𝐴 ) ) )
38 31 37 mpbid ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣𝑈 ) ) → ( 𝑣𝐵 ∧ ( 𝑣 supp 0 ) ∈ 𝐴 ) )
39 38 simpld ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣𝑈 ) ) → 𝑣𝐵 )
40 1 27 28 2 29 30 39 psrvscacl ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣𝑈 ) ) → ( 𝑢 ( ·𝑠𝑆 ) 𝑣 ) ∈ 𝐵 )
41 ovex ( ( 𝑢 ( ·𝑠𝑆 ) 𝑣 ) supp 0 ) ∈ V
42 41 a1i ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣𝑈 ) ) → ( ( 𝑢 ( ·𝑠𝑆 ) 𝑣 ) supp 0 ) ∈ V )
43 sseq2 ( 𝑥 = ( 𝑣 supp 0 ) → ( 𝑦𝑥𝑦 ⊆ ( 𝑣 supp 0 ) ) )
44 43 imbi1d ( 𝑥 = ( 𝑣 supp 0 ) → ( ( 𝑦𝑥𝑦𝐴 ) ↔ ( 𝑦 ⊆ ( 𝑣 supp 0 ) → 𝑦𝐴 ) ) )
45 44 albidv ( 𝑥 = ( 𝑣 supp 0 ) → ( ∀ 𝑦 ( 𝑦𝑥𝑦𝐴 ) ↔ ∀ 𝑦 ( 𝑦 ⊆ ( 𝑣 supp 0 ) → 𝑦𝐴 ) ) )
46 8 expr ( ( 𝜑𝑥𝐴 ) → ( 𝑦𝑥𝑦𝐴 ) )
47 46 alrimiv ( ( 𝜑𝑥𝐴 ) → ∀ 𝑦 ( 𝑦𝑥𝑦𝐴 ) )
48 47 ralrimiva ( 𝜑 → ∀ 𝑥𝐴𝑦 ( 𝑦𝑥𝑦𝐴 ) )
49 48 adantr ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣𝑈 ) ) → ∀ 𝑥𝐴𝑦 ( 𝑦𝑥𝑦𝐴 ) )
50 38 simprd ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣𝑈 ) ) → ( 𝑣 supp 0 ) ∈ 𝐴 )
51 45 49 50 rspcdva ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣𝑈 ) ) → ∀ 𝑦 ( 𝑦 ⊆ ( 𝑣 supp 0 ) → 𝑦𝐴 ) )
52 1 28 4 2 40 psrelbas ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣𝑈 ) ) → ( 𝑢 ( ·𝑠𝑆 ) 𝑣 ) : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
53 eqid ( .r𝑅 ) = ( .r𝑅 )
54 30 adantr ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣𝑈 ) ) ∧ 𝑘 ∈ ( 𝐷 ∖ ( 𝑣 supp 0 ) ) ) → 𝑢 ∈ ( Base ‘ 𝑅 ) )
55 39 adantr ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣𝑈 ) ) ∧ 𝑘 ∈ ( 𝐷 ∖ ( 𝑣 supp 0 ) ) ) → 𝑣𝐵 )
56 eldifi ( 𝑘 ∈ ( 𝐷 ∖ ( 𝑣 supp 0 ) ) → 𝑘𝐷 )
57 56 adantl ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣𝑈 ) ) ∧ 𝑘 ∈ ( 𝐷 ∖ ( 𝑣 supp 0 ) ) ) → 𝑘𝐷 )
58 1 27 28 2 53 4 54 55 57 psrvscaval ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣𝑈 ) ) ∧ 𝑘 ∈ ( 𝐷 ∖ ( 𝑣 supp 0 ) ) ) → ( ( 𝑢 ( ·𝑠𝑆 ) 𝑣 ) ‘ 𝑘 ) = ( 𝑢 ( .r𝑅 ) ( 𝑣𝑘 ) ) )
59 1 28 4 2 39 psrelbas ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣𝑈 ) ) → 𝑣 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
60 ssidd ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣𝑈 ) ) → ( 𝑣 supp 0 ) ⊆ ( 𝑣 supp 0 ) )
61 ovex ( ℕ0m 𝐼 ) ∈ V
62 4 61 rabex2 𝐷 ∈ V
63 62 a1i ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣𝑈 ) ) → 𝐷 ∈ V )
64 3 fvexi 0 ∈ V
65 64 a1i ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣𝑈 ) ) → 0 ∈ V )
66 59 60 63 65 suppssr ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣𝑈 ) ) ∧ 𝑘 ∈ ( 𝐷 ∖ ( 𝑣 supp 0 ) ) ) → ( 𝑣𝑘 ) = 0 )
67 66 oveq2d ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣𝑈 ) ) ∧ 𝑘 ∈ ( 𝐷 ∖ ( 𝑣 supp 0 ) ) ) → ( 𝑢 ( .r𝑅 ) ( 𝑣𝑘 ) ) = ( 𝑢 ( .r𝑅 ) 0 ) )
68 28 53 3 ringrz ( ( 𝑅 ∈ Ring ∧ 𝑢 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑢 ( .r𝑅 ) 0 ) = 0 )
69 10 30 68 syl2an2r ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣𝑈 ) ) → ( 𝑢 ( .r𝑅 ) 0 ) = 0 )
70 69 adantr ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣𝑈 ) ) ∧ 𝑘 ∈ ( 𝐷 ∖ ( 𝑣 supp 0 ) ) ) → ( 𝑢 ( .r𝑅 ) 0 ) = 0 )
71 58 67 70 3eqtrd ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣𝑈 ) ) ∧ 𝑘 ∈ ( 𝐷 ∖ ( 𝑣 supp 0 ) ) ) → ( ( 𝑢 ( ·𝑠𝑆 ) 𝑣 ) ‘ 𝑘 ) = 0 )
72 52 71 suppss ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣𝑈 ) ) → ( ( 𝑢 ( ·𝑠𝑆 ) 𝑣 ) supp 0 ) ⊆ ( 𝑣 supp 0 ) )
73 sseq1 ( 𝑦 = ( ( 𝑢 ( ·𝑠𝑆 ) 𝑣 ) supp 0 ) → ( 𝑦 ⊆ ( 𝑣 supp 0 ) ↔ ( ( 𝑢 ( ·𝑠𝑆 ) 𝑣 ) supp 0 ) ⊆ ( 𝑣 supp 0 ) ) )
74 eleq1 ( 𝑦 = ( ( 𝑢 ( ·𝑠𝑆 ) 𝑣 ) supp 0 ) → ( 𝑦𝐴 ↔ ( ( 𝑢 ( ·𝑠𝑆 ) 𝑣 ) supp 0 ) ∈ 𝐴 ) )
75 73 74 imbi12d ( 𝑦 = ( ( 𝑢 ( ·𝑠𝑆 ) 𝑣 ) supp 0 ) → ( ( 𝑦 ⊆ ( 𝑣 supp 0 ) → 𝑦𝐴 ) ↔ ( ( ( 𝑢 ( ·𝑠𝑆 ) 𝑣 ) supp 0 ) ⊆ ( 𝑣 supp 0 ) → ( ( 𝑢 ( ·𝑠𝑆 ) 𝑣 ) supp 0 ) ∈ 𝐴 ) ) )
76 75 spcgv ( ( ( 𝑢 ( ·𝑠𝑆 ) 𝑣 ) supp 0 ) ∈ V → ( ∀ 𝑦 ( 𝑦 ⊆ ( 𝑣 supp 0 ) → 𝑦𝐴 ) → ( ( ( 𝑢 ( ·𝑠𝑆 ) 𝑣 ) supp 0 ) ⊆ ( 𝑣 supp 0 ) → ( ( 𝑢 ( ·𝑠𝑆 ) 𝑣 ) supp 0 ) ∈ 𝐴 ) ) )
77 42 51 72 76 syl3c ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣𝑈 ) ) → ( ( 𝑢 ( ·𝑠𝑆 ) 𝑣 ) supp 0 ) ∈ 𝐴 )
78 32 eleq2d ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣𝑈 ) ) → ( ( 𝑢 ( ·𝑠𝑆 ) 𝑣 ) ∈ 𝑈 ↔ ( 𝑢 ( ·𝑠𝑆 ) 𝑣 ) ∈ { 𝑔𝐵 ∣ ( 𝑔 supp 0 ) ∈ 𝐴 } ) )
79 oveq1 ( 𝑔 = ( 𝑢 ( ·𝑠𝑆 ) 𝑣 ) → ( 𝑔 supp 0 ) = ( ( 𝑢 ( ·𝑠𝑆 ) 𝑣 ) supp 0 ) )
80 79 eleq1d ( 𝑔 = ( 𝑢 ( ·𝑠𝑆 ) 𝑣 ) → ( ( 𝑔 supp 0 ) ∈ 𝐴 ↔ ( ( 𝑢 ( ·𝑠𝑆 ) 𝑣 ) supp 0 ) ∈ 𝐴 ) )
81 80 elrab ( ( 𝑢 ( ·𝑠𝑆 ) 𝑣 ) ∈ { 𝑔𝐵 ∣ ( 𝑔 supp 0 ) ∈ 𝐴 } ↔ ( ( 𝑢 ( ·𝑠𝑆 ) 𝑣 ) ∈ 𝐵 ∧ ( ( 𝑢 ( ·𝑠𝑆 ) 𝑣 ) supp 0 ) ∈ 𝐴 ) )
82 78 81 bitrdi ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣𝑈 ) ) → ( ( 𝑢 ( ·𝑠𝑆 ) 𝑣 ) ∈ 𝑈 ↔ ( ( 𝑢 ( ·𝑠𝑆 ) 𝑣 ) ∈ 𝐵 ∧ ( ( 𝑢 ( ·𝑠𝑆 ) 𝑣 ) supp 0 ) ∈ 𝐴 ) ) )
83 40 77 82 mpbir2and ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣𝑈 ) ) → ( 𝑢 ( ·𝑠𝑆 ) 𝑣 ) ∈ 𝑈 )
84 83 3adantr3 ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣𝑈𝑤𝑈 ) ) → ( 𝑢 ( ·𝑠𝑆 ) 𝑣 ) ∈ 𝑈 )
85 simpr3 ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣𝑈𝑤𝑈 ) ) → 𝑤𝑈 )
86 eqid ( +g𝑆 ) = ( +g𝑆 )
87 86 subgcl ( ( 𝑈 ∈ ( SubGrp ‘ 𝑆 ) ∧ ( 𝑢 ( ·𝑠𝑆 ) 𝑣 ) ∈ 𝑈𝑤𝑈 ) → ( ( 𝑢 ( ·𝑠𝑆 ) 𝑣 ) ( +g𝑆 ) 𝑤 ) ∈ 𝑈 )
88 26 84 85 87 syl3anc ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣𝑈𝑤𝑈 ) ) → ( ( 𝑢 ( ·𝑠𝑆 ) 𝑣 ) ( +g𝑆 ) 𝑤 ) ∈ 𝑈 )
89 11 12 13 14 15 16 21 25 88 islssd ( 𝜑𝑈 ∈ ( LSubSp ‘ 𝑆 ) )