Theorem lspexchn1

Description: Exchange property for span of a pair with negated membership. TODO: look at uses of lspexch to see if this will shorten proofs. (Contributed by NM, 20-May-2015)

	Ref	Expression
Hypotheses	lspexchn1.v	|- V = ( Base ` W )
	lspexchn1.n	|- N = ( LSpan ` W )
	lspexchn1.w	|- ( ph -> W e. LVec )
	lspexchn1.x	|- ( ph -> X e. V )
	lspexchn1.y	|- ( ph -> Y e. V )
	lspexchn1.z	|- ( ph -> Z e. V )
	lspexchn1.q	|- ( ph -> -. Y e. ( N ` { Z } ) )
	lspexchn1.e	|- ( ph -> -. X e. ( N ` { Y , Z } ) )
Assertion	lspexchn1	|- ( ph -> -. Y e. ( N ` { X , Z } ) )

Proof

Step	Hyp	Ref	Expression
1		lspexchn1.v	|- V = ( Base ` W )
2		lspexchn1.n	|- N = ( LSpan ` W )
3		lspexchn1.w	|- ( ph -> W e. LVec )
4		lspexchn1.x	|- ( ph -> X e. V )
5		lspexchn1.y	|- ( ph -> Y e. V )
6		lspexchn1.z	|- ( ph -> Z e. V )
7		lspexchn1.q	|- ( ph -> -. Y e. ( N ` { Z } ) )
8		lspexchn1.e	|- ( ph -> -. X e. ( N ` { Y , Z } ) )
9		eqid	|- ( 0g ` W ) = ( 0g ` W )
10	3	adantr	|- ( ( ph /\ Y e. ( N ` { X , Z } ) ) -> W e. LVec )
11		eqid	|- ( LSubSp ` W ) = ( LSubSp ` W )
12		lveclmod	|- ( W e. LVec -> W e. LMod )
13	3 12	syl	|- ( ph -> W e. LMod )
14	1 11 2	lspsncl	|- ( ( W e. LMod /\ Z e. V ) -> ( N ` { Z } ) e. ( LSubSp ` W ) )
15	13 6 14	syl2anc	|- ( ph -> ( N ` { Z } ) e. ( LSubSp ` W ) )
16	9 11 13 15 5 7	lssneln0	|- ( ph -> Y e. ( V \ { ( 0g ` W ) } ) )
17	16	adantr	|- ( ( ph /\ Y e. ( N ` { X , Z } ) ) -> Y e. ( V \ { ( 0g ` W ) } ) )
18	4	adantr	|- ( ( ph /\ Y e. ( N ` { X , Z } ) ) -> X e. V )
19	6	adantr	|- ( ( ph /\ Y e. ( N ` { X , Z } ) ) -> Z e. V )
20	1 2 13 5 6 7	lspsnne2	|- ( ph -> ( N ` { Y } ) =/= ( N ` { Z } ) )
21	20	adantr	|- ( ( ph /\ Y e. ( N ` { X , Z } ) ) -> ( N ` { Y } ) =/= ( N ` { Z } ) )
22		simpr	|- ( ( ph /\ Y e. ( N ` { X , Z } ) ) -> Y e. ( N ` { X , Z } ) )
23	1 9 2 10 17 18 19 21 22	lspexch	|- ( ( ph /\ Y e. ( N ` { X , Z } ) ) -> X e. ( N ` { Y , Z } ) )
24	8 23	mtand	|- ( ph -> -. Y e. ( N ` { X , Z } ) )