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 
|- S = ( LSubSp ` W )
Assertion lssincl 
|- ( ( W e. LMod /\ T e. S /\ U e. S ) -> ( T i^i U ) e. S )

Proof

Step Hyp Ref Expression
1 lssintcl.s 
 |-  S = ( LSubSp ` W )
2 intprg 
 |-  ( ( T e. S /\ U e. S ) -> |^| { T , U } = ( T i^i U ) )
3 2 3adant1 
 |-  ( ( W e. LMod /\ T e. S /\ U e. S ) -> |^| { T , U } = ( T i^i U ) )
4 simp1 
 |-  ( ( W e. LMod /\ T e. S /\ U e. S ) -> W e. LMod )
5 prssi 
 |-  ( ( T e. S /\ U e. S ) -> { T , U } C_ S )
6 5 3adant1 
 |-  ( ( W e. LMod /\ T e. S /\ U e. S ) -> { T , U } C_ S )
7 prnzg 
 |-  ( T e. S -> { T , U } =/= (/) )
8 7 3ad2ant2 
 |-  ( ( W e. LMod /\ T e. S /\ U e. S ) -> { T , U } =/= (/) )
9 1 lssintcl 
 |-  ( ( W e. LMod /\ { T , U } C_ S /\ { T , U } =/= (/) ) -> |^| { T , U } e. S )
10 4 6 8 9 syl3anc 
 |-  ( ( W e. LMod /\ T e. S /\ U e. S ) -> |^| { T , U } e. S )
11 3 10 eqeltrrd 
 |-  ( ( W e. LMod /\ T e. S /\ U e. S ) -> ( T i^i U ) e. S )