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	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
Assertion	lssincl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) → ( 𝑇 ∩ 𝑈 ) ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		lssintcl.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
2		intprg	⊢ ( ( 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) → ∩ { 𝑇 , 𝑈 } = ( 𝑇 ∩ 𝑈 ) )
3	2	3adant1	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) → ∩ { 𝑇 , 𝑈 } = ( 𝑇 ∩ 𝑈 ) )
4		simp1	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) → 𝑊 ∈ LMod )
5		prssi	⊢ ( ( 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) → { 𝑇 , 𝑈 } ⊆ 𝑆 )
6	5	3adant1	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) → { 𝑇 , 𝑈 } ⊆ 𝑆 )
7		prnzg	⊢ ( 𝑇 ∈ 𝑆 → { 𝑇 , 𝑈 } ≠ ∅ )
8	7	3ad2ant2	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) → { 𝑇 , 𝑈 } ≠ ∅ )
9	1	lssintcl	⊢ ( ( 𝑊 ∈ LMod ∧ { 𝑇 , 𝑈 } ⊆ 𝑆 ∧ { 𝑇 , 𝑈 } ≠ ∅ ) → ∩ { 𝑇 , 𝑈 } ∈ 𝑆 )
10	4 6 8 9	syl3anc	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) → ∩ { 𝑇 , 𝑈 } ∈ 𝑆 )
11	3 10	eqeltrrd	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) → ( 𝑇 ∩ 𝑈 ) ∈ 𝑆 )