Metamath Proof Explorer


Theorem lspsnel6

Description: Relationship between a vector and the 1-dim (or 0-dim) subspace it generates. (Contributed by NM, 8-Aug-2014) (Revised by Mario Carneiro, 8-Jan-2015)

Ref Expression
Hypotheses lspsnel5.v
|- V = ( Base ` W )
lspsnel5.s
|- S = ( LSubSp ` W )
lspsnel5.n
|- N = ( LSpan ` W )
lspsnel5.w
|- ( ph -> W e. LMod )
lspsnel5.a
|- ( ph -> U e. S )
Assertion lspsnel6
|- ( ph -> ( X e. U <-> ( X e. V /\ ( N ` { X } ) C_ U ) ) )

Proof

Step Hyp Ref Expression
1 lspsnel5.v
 |-  V = ( Base ` W )
2 lspsnel5.s
 |-  S = ( LSubSp ` W )
3 lspsnel5.n
 |-  N = ( LSpan ` W )
4 lspsnel5.w
 |-  ( ph -> W e. LMod )
5 lspsnel5.a
 |-  ( ph -> U e. S )
6 1 2 lssel
 |-  ( ( U e. S /\ X e. U ) -> X e. V )
7 5 6 sylan
 |-  ( ( ph /\ X e. U ) -> X e. V )
8 4 adantr
 |-  ( ( ph /\ X e. U ) -> W e. LMod )
9 5 adantr
 |-  ( ( ph /\ X e. U ) -> U e. S )
10 simpr
 |-  ( ( ph /\ X e. U ) -> X e. U )
11 2 3 lspsnss
 |-  ( ( W e. LMod /\ U e. S /\ X e. U ) -> ( N ` { X } ) C_ U )
12 8 9 10 11 syl3anc
 |-  ( ( ph /\ X e. U ) -> ( N ` { X } ) C_ U )
13 7 12 jca
 |-  ( ( ph /\ X e. U ) -> ( X e. V /\ ( N ` { X } ) C_ U ) )
14 1 3 lspsnid
 |-  ( ( W e. LMod /\ X e. V ) -> X e. ( N ` { X } ) )
15 4 14 sylan
 |-  ( ( ph /\ X e. V ) -> X e. ( N ` { X } ) )
16 ssel
 |-  ( ( N ` { X } ) C_ U -> ( X e. ( N ` { X } ) -> X e. U ) )
17 15 16 syl5com
 |-  ( ( ph /\ X e. V ) -> ( ( N ` { X } ) C_ U -> X e. U ) )
18 17 impr
 |-  ( ( ph /\ ( X e. V /\ ( N ` { X } ) C_ U ) ) -> X e. U )
19 13 18 impbida
 |-  ( ph -> ( X e. U <-> ( X e. V /\ ( N ` { X } ) C_ U ) ) )