lssintcl

Description: The intersection of a nonempty set of subspaces is a subspace. (Contributed by NM, 8-Dec-2013) (Revised by Mario Carneiro, 19-Jun-2014)

		Ref	Expression
	Hypothesis	lssintcl.s	$⊢ S = LSubSp (W)$
	Assertion	lssintcl	$⊢ (W \in LMod \land A \subseteq S \land A \neq \emptyset) \to ⋂ A \in S$

Proof

Step	Hyp	Ref	Expression
1		lssintcl.s	$⊢ S = LSubSp (W)$
2		eqidd	$⊢ (W \in LMod \land A \subseteq S \land A \neq \emptyset) \to Scalar (W) = Scalar (W)$
3		eqidd	$⊢ (W \in LMod \land A \subseteq S \land A \neq \emptyset) \to {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
4		eqidd	$⊢ (W \in LMod \land A \subseteq S \land A \neq \emptyset) \to {Base}_{W} = {Base}_{W}$
5		eqidd	$⊢ (W \in LMod \land A \subseteq S \land A \neq \emptyset) \to +_{W} = +_{W}$
6		eqidd	$⊢ (W \in LMod \land A \subseteq S \land A \neq \emptyset) \to \cdot_{W} = \cdot_{W}$
7	1	a1i	$⊢ (W \in LMod \land A \subseteq S \land A \neq \emptyset) \to S = LSubSp (W)$
8		intssuni2	$⊢ (A \subseteq S \land A \neq \emptyset) \to ⋂ A \subseteq ⋃ S$
9	8	3adant1	$⊢ (W \in LMod \land A \subseteq S \land A \neq \emptyset) \to ⋂ A \subseteq ⋃ S$
10		eqid	$⊢ {Base}_{W} = {Base}_{W}$
11	10 1	lssss	$⊢ y \in S \to y \subseteq {Base}_{W}$
12		velpw	$⊢ y \in 𝒫 {Base}_{W} \leftrightarrow y \subseteq {Base}_{W}$
13	11 12	sylibr	$⊢ y \in S \to y \in 𝒫 {Base}_{W}$
14	13	ssriv	$⊢ S \subseteq 𝒫 {Base}_{W}$
15		sspwuni	$⊢ S \subseteq 𝒫 {Base}_{W} \leftrightarrow ⋃ S \subseteq {Base}_{W}$
16	14 15	mpbi	$⊢ ⋃ S \subseteq {Base}_{W}$
17	9 16	sstrdi	$⊢ (W \in LMod \land A \subseteq S \land A \neq \emptyset) \to ⋂ A \subseteq {Base}_{W}$
18		simpl1	$⊢ ((W \in LMod \land A \subseteq S \land A \neq \emptyset) \land y \in A) \to W \in LMod$
19		simp2	$⊢ (W \in LMod \land A \subseteq S \land A \neq \emptyset) \to A \subseteq S$
20	19	sselda	$⊢ ((W \in LMod \land A \subseteq S \land A \neq \emptyset) \land y \in A) \to y \in S$
21		eqid	$⊢ 0_{W} = 0_{W}$
22	21 1	lss0cl	$⊢ (W \in LMod \land y \in S) \to 0_{W} \in y$
23	18 20 22	syl2anc	$⊢ ((W \in LMod \land A \subseteq S \land A \neq \emptyset) \land y \in A) \to 0_{W} \in y$
24	23	ralrimiva	$⊢ (W \in LMod \land A \subseteq S \land A \neq \emptyset) \to \forall y \in A 0_{W} \in y$
25		fvex	$⊢ 0_{W} \in V$
26	25	elint2	$⊢ 0_{W} \in ⋂ A \leftrightarrow \forall y \in A 0_{W} \in y$
27	24 26	sylibr	$⊢ (W \in LMod \land A \subseteq S \land A \neq \emptyset) \to 0_{W} \in ⋂ A$
28	27	ne0d	$⊢ (W \in LMod \land A \subseteq S \land A \neq \emptyset) \to ⋂ A \neq \emptyset$
29	20	adantlr	$⊢ (((W \in LMod \land A \subseteq S \land A \neq \emptyset) \land (x \in {Base}_{Scalar (W)} \land a \in ⋂ A \land b \in ⋂ A)) \land y \in A) \to y \in S$
30		simplr1	$⊢ (((W \in LMod \land A \subseteq S \land A \neq \emptyset) \land (x \in {Base}_{Scalar (W)} \land a \in ⋂ A \land b \in ⋂ A)) \land y \in A) \to x \in {Base}_{Scalar (W)}$
31		simplr2	$⊢ (((W \in LMod \land A \subseteq S \land A \neq \emptyset) \land (x \in {Base}_{Scalar (W)} \land a \in ⋂ A \land b \in ⋂ A)) \land y \in A) \to a \in ⋂ A$
32		simpr	$⊢ (((W \in LMod \land A \subseteq S \land A \neq \emptyset) \land (x \in {Base}_{Scalar (W)} \land a \in ⋂ A \land b \in ⋂ A)) \land y \in A) \to y \in A$
33		elinti	$⊢ a \in ⋂ A \to (y \in A \to a \in y)$
34	31 32 33	sylc	$⊢ (((W \in LMod \land A \subseteq S \land A \neq \emptyset) \land (x \in {Base}_{Scalar (W)} \land a \in ⋂ A \land b \in ⋂ A)) \land y \in A) \to a \in y$
35		simplr3	$⊢ (((W \in LMod \land A \subseteq S \land A \neq \emptyset) \land (x \in {Base}_{Scalar (W)} \land a \in ⋂ A \land b \in ⋂ A)) \land y \in A) \to b \in ⋂ A$
36		elinti	$⊢ b \in ⋂ A \to (y \in A \to b \in y)$
37	35 32 36	sylc	$⊢ (((W \in LMod \land A \subseteq S \land A \neq \emptyset) \land (x \in {Base}_{Scalar (W)} \land a \in ⋂ A \land b \in ⋂ A)) \land y \in A) \to b \in y$
38		eqid	$⊢ Scalar (W) = Scalar (W)$
39		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
40		eqid	$⊢ +_{W} = +_{W}$
41		eqid	$⊢ \cdot_{W} = \cdot_{W}$
42	38 39 40 41 1	lsscl	$⊢ (y \in S \land (x \in {Base}_{Scalar (W)} \land a \in y \land b \in y)) \to (x \cdot_{W} a) +_{W} b \in y$
43	29 30 34 37 42	syl13anc	$⊢ (((W \in LMod \land A \subseteq S \land A \neq \emptyset) \land (x \in {Base}_{Scalar (W)} \land a \in ⋂ A \land b \in ⋂ A)) \land y \in A) \to (x \cdot_{W} a) +_{W} b \in y$
44	43	ralrimiva	$⊢ ((W \in LMod \land A \subseteq S \land A \neq \emptyset) \land (x \in {Base}_{Scalar (W)} \land a \in ⋂ A \land b \in ⋂ A)) \to \forall y \in A (x \cdot_{W} a) +_{W} b \in y$
45		ovex	$⊢ (x \cdot_{W} a) +_{W} b \in V$
46	45	elint2	$⊢ (x \cdot_{W} a) +_{W} b \in ⋂ A \leftrightarrow \forall y \in A (x \cdot_{W} a) +_{W} b \in y$
47	44 46	sylibr	$⊢ ((W \in LMod \land A \subseteq S \land A \neq \emptyset) \land (x \in {Base}_{Scalar (W)} \land a \in ⋂ A \land b \in ⋂ A)) \to (x \cdot_{W} a) +_{W} b \in ⋂ A$
48	2 3 4 5 6 7 17 28 47	islssd	$⊢ (W \in LMod \land A \subseteq S \land A \neq \emptyset) \to ⋂ A \in S$

Metamath Proof Explorer

Theorem lssintcl

Proof