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

Metamath Proof Explorer

Theorem lspid

Description: The span of a subspace is itself. ( spanid analog.) (Contributed by NM, 15-Dec-2013) (Revised by Mario Carneiro, 19-Jun-2014)

Ref Expression
Hypotheses lspid.s 
|- S = ( LSubSp ` W )
lspid.n 
|- N = ( LSpan ` W )
Assertion lspid 
|- ( ( W e. LMod /\ U e. S ) -> ( N ` U ) = U )

Proof

Step Hyp Ref Expression
1 lspid.s 
 |-  S = ( LSubSp ` W )
2 lspid.n 
 |-  N = ( LSpan ` W )
3 eqid 
 |-  ( Base ` W ) = ( Base ` W )
4 3 1 lssss 
 |-  ( U e. S -> U C_ ( Base ` W ) )
5 3 1 2 lspval 
 |-  ( ( W e. LMod /\ U C_ ( Base ` W ) ) -> ( N ` U ) = |^| { t e. S | U C_ t } )
6 4 5 sylan2 
 |-  ( ( W e. LMod /\ U e. S ) -> ( N ` U ) = |^| { t e. S | U C_ t } )
7 intmin 
 |-  ( U e. S -> |^| { t e. S | U C_ t } = U )
8 7 adantl 
 |-  ( ( W e. LMod /\ U e. S ) -> |^| { t e. S | U C_ t } = U )
9 6 8 eqtrd 
 |-  ( ( W e. LMod /\ U e. S ) -> ( N ` U ) = U )