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 ) )