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	$⊢ \underset{˙}{0} = 0_{R}$
	mplsubglem.d	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
	mplsubglem.i	$⊢ φ \to I \in W$
	mplsubglem.0	$⊢ φ \to \emptyset \in A$
	mplsubglem.a	$⊢ (φ \land (x \in A \land y \in A)) \to x \cup y \in A$
	mplsubglem.y	$⊢ (φ \land (x \in A \land y \subseteq x)) \to y \in A$
	mplsubglem.u	$⊢ φ \to U = \{g \in B \| g supp \underset{˙}{0} \in A\}$
	mpllsslem.r	$⊢ φ \to R \in Ring$
Assertion	mpllsslem	$⊢ φ \to U \in LSubSp (S)$

Proof

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

Metamath Proof Explorer

Theorem mpllsslem

Proof