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

Metamath Proof Explorer

Theorem lspexchn1

Proof