# 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}={\mathrm{Base}}_{{W}}$
lspexchn2.n ${⊢}{N}=\mathrm{LSpan}\left({W}\right)$
lspexchn2.w ${⊢}{\phi }\to {W}\in \mathrm{LVec}$
lspexchn2.x ${⊢}{\phi }\to {X}\in {V}$
lspexchn2.y ${⊢}{\phi }\to {Y}\in {V}$
lspexchn2.z ${⊢}{\phi }\to {Z}\in {V}$
lspexchn2.q ${⊢}{\phi }\to ¬{Y}\in {N}\left(\left\{{Z}\right\}\right)$
lspexchn2.e ${⊢}{\phi }\to ¬{X}\in {N}\left(\left\{{Z},{Y}\right\}\right)$
Assertion lspexchn2 ${⊢}{\phi }\to ¬{Y}\in {N}\left(\left\{{Z},{X}\right\}\right)$

### Proof

Step Hyp Ref Expression
1 lspexchn2.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
2 lspexchn2.n ${⊢}{N}=\mathrm{LSpan}\left({W}\right)$
3 lspexchn2.w ${⊢}{\phi }\to {W}\in \mathrm{LVec}$
4 lspexchn2.x ${⊢}{\phi }\to {X}\in {V}$
5 lspexchn2.y ${⊢}{\phi }\to {Y}\in {V}$
6 lspexchn2.z ${⊢}{\phi }\to {Z}\in {V}$
7 lspexchn2.q ${⊢}{\phi }\to ¬{Y}\in {N}\left(\left\{{Z}\right\}\right)$
8 lspexchn2.e ${⊢}{\phi }\to ¬{X}\in {N}\left(\left\{{Z},{Y}\right\}\right)$
9 prcom ${⊢}\left\{{Z},{Y}\right\}=\left\{{Y},{Z}\right\}$
10 9 fveq2i ${⊢}{N}\left(\left\{{Z},{Y}\right\}\right)={N}\left(\left\{{Y},{Z}\right\}\right)$
11 10 eleq2i ${⊢}{X}\in {N}\left(\left\{{Z},{Y}\right\}\right)↔{X}\in {N}\left(\left\{{Y},{Z}\right\}\right)$
12 8 11 sylnib ${⊢}{\phi }\to ¬{X}\in {N}\left(\left\{{Y},{Z}\right\}\right)$
13 1 2 3 4 5 6 7 12 lspexchn1 ${⊢}{\phi }\to ¬{Y}\in {N}\left(\left\{{X},{Z}\right\}\right)$
14 prcom ${⊢}\left\{{X},{Z}\right\}=\left\{{Z},{X}\right\}$
15 14 fveq2i ${⊢}{N}\left(\left\{{X},{Z}\right\}\right)={N}\left(\left\{{Z},{X}\right\}\right)$
16 15 eleq2i ${⊢}{Y}\in {N}\left(\left\{{X},{Z}\right\}\right)↔{Y}\in {N}\left(\left\{{Z},{X}\right\}\right)$
17 13 16 sylnib ${⊢}{\phi }\to ¬{Y}\in {N}\left(\left\{{Z},{X}\right\}\right)$