Theorem lspsnnecom

Description: Swap two vectors with different spans. (Contributed by NM, 20-May-2015)

	Ref	Expression
Hypotheses	lspsnnecom.v	$$⊢V={\mathrm{Base}}_W$$
	lspsnnecom.o	$$⊢\underset{\dot{}}{0}=0_W$$
	lspsnnecom.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
	lspsnnecom.w	$$⊢\phi \to W\in \mathrm{LVec}$$
	lspsnnecom.x	$$⊢\phi \to X\in V$$
	lspsnnecom.y	$$⊢\phi \to Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	lspsnnecom.e	$$⊢\phi \to \neg X\in N\left(\left\{Y\right\}\right)$$
Assertion	lspsnnecom	$$⊢\phi \to \neg Y\in N\left(\left\{X\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		lspsnnecom.v	$$⊢V={\mathrm{Base}}_W$$
2		lspsnnecom.o	$$⊢\underset{\dot{}}{0}=0_W$$
3		lspsnnecom.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
4		lspsnnecom.w	$$⊢\phi \to W\in \mathrm{LVec}$$
5		lspsnnecom.x	$$⊢\phi \to X\in V$$
6		lspsnnecom.y	$$⊢\phi \to Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
7		lspsnnecom.e	$$⊢\phi \to \neg X\in N\left(\left\{Y\right\}\right)$$
8		lveclmod	$$⊢W\in \mathrm{LVec}\to W\in \mathrm{LMod}$$
9	4 8	syl	$$⊢\phi \to W\in \mathrm{LMod}$$
10	6	eldifad	$$⊢\phi \to Y\in V$$
11	1 3 9 5 10 7	lspsnne2	$$⊢\phi \to N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)$$
12	11	necomd	$$⊢\phi \to N\left(\left\{Y\right\}\right)\ne N\left(\left\{X\right\}\right)$$
13	1 2 3 4 6 5 12	lspsnne1	$$⊢\phi \to \neg Y\in N\left(\left\{X\right\}\right)$$