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

Metamath Proof Explorer

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