Theorem lspexchn2

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, 24-May-2015)

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

Proof

Step	Hyp	Ref	Expression
1		lspexchn2.v	|- V = ( Base ` W )
2		lspexchn2.n	|- N = ( LSpan ` W )
3		lspexchn2.w	|- ( ph -> W e. LVec )
4		lspexchn2.x	|- ( ph -> X e. V )
5		lspexchn2.y	|- ( ph -> Y e. V )
6		lspexchn2.z	|- ( ph -> Z e. V )
7		lspexchn2.q	|- ( ph -> -. Y e. ( N ` { Z } ) )
8		lspexchn2.e	|- ( ph -> -. X e. ( N ` { Z , Y } ) )
9		prcom	|- { Z , Y } = { Y , Z }
10	9	fveq2i	|- ( N ` { Z , Y } ) = ( N ` { Y , Z } )
11	10	eleq2i	|- ( X e. ( N ` { Z , Y } ) <-> X e. ( N ` { Y , Z } ) )
12	8 11	sylnib	|- ( ph -> -. X e. ( N ` { Y , Z } ) )
13	1 2 3 4 5 6 7 12	lspexchn1	|- ( ph -> -. Y e. ( N ` { X , Z } ) )
14		prcom	|- { X , Z } = { Z , X }
15	14	fveq2i	|- ( N ` { X , Z } ) = ( N ` { Z , X } )
16	15	eleq2i	|- ( Y e. ( N ` { X , Z } ) <-> Y e. ( N ` { Z , X } ) )
17	13 16	sylnib	|- ( ph -> -. Y e. ( N ` { Z , X } ) )