# Metamath Proof Explorer

## Theorem 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}=\mathrm{LSubSp}\left({W}\right)$
Assertion lssincl ${⊢}\left({W}\in \mathrm{LMod}\wedge {T}\in {S}\wedge {U}\in {S}\right)\to {T}\cap {U}\in {S}$

### Proof

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