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

Metamath Proof Explorer

Theorem ellspsn6

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 ellspsn5b.v 
|- V = ( Base ` W )
ellspsn5b.s 
|- S = ( LSubSp ` W )
ellspsn5b.n 
|- N = ( LSpan ` W )
ellspsn5b.w 
|- ( ph -> W e. LMod )
ellspsn5b.a 
|- ( ph -> U e. S )
Assertion ellspsn6 
|- ( ph -> ( X e. U <-> ( X e. V /\ ( N ` { X } ) C_ U ) ) )

Proof

Step Hyp Ref Expression
1 ellspsn5b.v 
 |-  V = ( Base ` W )
2 ellspsn5b.s 
 |-  S = ( LSubSp ` W )
3 ellspsn5b.n 
 |-  N = ( LSpan ` W )
4 ellspsn5b.w 
 |-  ( ph -> W e. LMod )
5 ellspsn5b.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 ) ) )