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

Metamath Proof Explorer

Theorem ellspsn4

Description: A member of the span of the singleton of a vector is a member of a subspace containing the vector. ( elspansn4 analog.) (Contributed by NM, 4-Jul-2014)

Ref Expression
Hypotheses ellspsn4.v 
|- V = ( Base ` W )
ellspsn4.o 
|- .0. = ( 0g ` W )
ellspsn4.s 
|- S = ( LSubSp ` W )
ellspsn4.n 
|- N = ( LSpan ` W )
ellspsn4.w 
|- ( ph -> W e. LVec )
ellspsn4.u 
|- ( ph -> U e. S )
ellspsn4.x 
|- ( ph -> X e. V )
ellspsn4.y 
|- ( ph -> Y e. ( N ` { X } ) )
ellspsn4.z 
|- ( ph -> Y =/= .0. )
Assertion ellspsn4 
|- ( ph -> ( X e. U <-> Y e. U ) )

Proof

Step Hyp Ref Expression
1 ellspsn4.v 
 |-  V = ( Base ` W )
2 ellspsn4.o 
 |-  .0. = ( 0g ` W )
3 ellspsn4.s 
 |-  S = ( LSubSp ` W )
4 ellspsn4.n 
 |-  N = ( LSpan ` W )
5 ellspsn4.w 
 |-  ( ph -> W e. LVec )
6 ellspsn4.u 
 |-  ( ph -> U e. S )
7 ellspsn4.x 
 |-  ( ph -> X e. V )
8 ellspsn4.y 
 |-  ( ph -> Y e. ( N ` { X } ) )
9 ellspsn4.z 
 |-  ( ph -> Y =/= .0. )
10 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
11 5 10 syl 
 |-  ( ph -> W e. LMod )
12 11 adantr 
 |-  ( ( ph /\ X e. U ) -> W e. LMod )
13 6 adantr 
 |-  ( ( ph /\ X e. U ) -> U e. S )
14 simpr 
 |-  ( ( ph /\ X e. U ) -> X e. U )
15 8 adantr 
 |-  ( ( ph /\ X e. U ) -> Y e. ( N ` { X } ) )
16 3 4 12 13 14 15 ellspsn3 
 |-  ( ( ph /\ X e. U ) -> Y e. U )
17 11 adantr 
 |-  ( ( ph /\ Y e. U ) -> W e. LMod )
18 6 adantr 
 |-  ( ( ph /\ Y e. U ) -> U e. S )
19 simpr 
 |-  ( ( ph /\ Y e. U ) -> Y e. U )
20 1 4 lspsnid 
 |-  ( ( W e. LMod /\ X e. V ) -> X e. ( N ` { X } ) )
21 11 7 20 syl2anc 
 |-  ( ph -> X e. ( N ` { X } ) )
22 1 2 4 5 7 8 9 lspsneleq 
 |-  ( ph -> ( N ` { Y } ) = ( N ` { X } ) )
23 21 22 eleqtrrd 
 |-  ( ph -> X e. ( N ` { Y } ) )
24 23 adantr 
 |-  ( ( ph /\ Y e. U ) -> X e. ( N ` { Y } ) )
25 3 4 17 18 19 24 ellspsn3 
 |-  ( ( ph /\ Y e. U ) -> X e. U )
26 16 25 impbida 
 |-  ( ph -> ( X e. U <-> Y e. U ) )