lssincl

Description: The intersection of two subspaces is a subspace. (Contributed by NM, 7-Mar-2014) (Revised by Mario Carneiro, 19-Jun-2014)

		Ref	Expression
	Hypothesis	lssintcl.s	$⊢ S = LSubSp (W)$
	Assertion	lssincl	$⊢ (W \in LMod \land T \in S \land U \in S) \to T \cap U \in S$

Step	Hyp	Ref	Expression
1		lssintcl.s	$⊢ S = LSubSp (W)$
2		intprg	$⊢ (T \in S \land U \in S) \to ⋂ \{T, U\} = T \cap U$
3	2	3adant1	$⊢ (W \in LMod \land T \in S \land U \in S) \to ⋂ \{T, U\} = T \cap U$
4		simp1	$⊢ (W \in LMod \land T \in S \land U \in S) \to W \in LMod$
5		prssi	$⊢ (T \in S \land U \in S) \to \{T, U\} \subseteq S$
6	5	3adant1	$⊢ (W \in LMod \land T \in S \land U \in S) \to \{T, U\} \subseteq S$
7		prnzg	$⊢ T \in S \to \{T, U\} \neq \emptyset$
8	7	3ad2ant2	$⊢ (W \in LMod \land T \in S \land U \in S) \to \{T, U\} \neq \emptyset$
9	1	lssintcl	$⊢ (W \in LMod \land \{T, U\} \subseteq S \land \{T, U\} \neq \emptyset) \to ⋂ \{T, U\} \in S$
10	4 6 8 9	syl3anc	$⊢ (W \in LMod \land T \in S \land U \in S) \to ⋂ \{T, U\} \in S$
11	3 10	eqeltrrd	$⊢ (W \in LMod \land T \in S \land U \in S) \to T \cap U \in S$

Metamath Proof Explorer