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=BaseW
lspexchn2.n N=LSpanW
lspexchn2.w φWLVec
lspexchn2.x φXV
lspexchn2.y φYV
lspexchn2.z φZV
lspexchn2.q φ¬YNZ
lspexchn2.e φ¬XNZY
Assertion lspexchn2 φ¬YNZX

Proof

Step Hyp Ref Expression
1 lspexchn2.v V=BaseW
2 lspexchn2.n N=LSpanW
3 lspexchn2.w φWLVec
4 lspexchn2.x φXV
5 lspexchn2.y φYV
6 lspexchn2.z φZV
7 lspexchn2.q φ¬YNZ
8 lspexchn2.e φ¬XNZY
9 prcom ZY=YZ
10 9 fveq2i NZY=NYZ
11 10 eleq2i XNZYXNYZ
12 8 11 sylnib φ¬XNYZ
13 1 2 3 4 5 6 7 12 lspexchn1 φ¬YNXZ
14 prcom XZ=ZX
15 14 fveq2i NXZ=NZX
16 15 eleq2i YNXZYNZX
17 13 16 sylnib φ¬YNZX