This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑆 = ( 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 ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) → ( 𝑇 ∩ 𝑈 ) ∈ 𝑆 )