Theorem dochexmidat

Description: Special case of excluded middle for the singleton of a vector. (Contributed by NM, 27-Oct-2014)

	Ref	Expression
Hypotheses	dochexmidat.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dochexmidat.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
	dochexmidat.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	dochexmidat.v	$$⊢V={\mathrm{Base}}_U$$
	dochexmidat.z	$$⊢\underset{\dot{}}{0}=0_U$$
	dochexmidat.r	$$⊢N=\mathrm{LSpan}\left(U\right)$$
	dochexmidat.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(U\right)$$
	dochexmidat.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	dochexmidat.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
Assertion	dochexmidat	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\left\{X\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{X\right\}\right)=V$$

Proof

Step	Hyp	Ref	Expression
1		dochexmidat.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		dochexmidat.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
3		dochexmidat.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
4		dochexmidat.v	$$⊢V={\mathrm{Base}}_U$$
5		dochexmidat.z	$$⊢\underset{\dot{}}{0}=0_U$$
6		dochexmidat.r	$$⊢N=\mathrm{LSpan}\left(U\right)$$
7		dochexmidat.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(U\right)$$
8		dochexmidat.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
9		dochexmidat.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
10	1 2 3 4 5 8 9	dochnel	$$⊢\phi \to \neg X\in \underset{\dot{}}{\perp }\left(\left\{X\right\}\right)$$
11		eqid	$$⊢\mathrm{LSHyp}\left(U\right)=\mathrm{LSHyp}\left(U\right)$$
12	1 3 8	dvhlvec	$$⊢\phi \to U\in \mathrm{LVec}$$
13	1 2 3 4 5 11 8 9	dochsnshp	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\left\{X\right\}\right)\in \mathrm{LSHyp}\left(U\right)$$
14	9	eldifad	$$⊢\phi \to X\in V$$
15	4 6 7 11 12 13 14	lshpnelb	$$⊢\phi \to \left(\neg X\in \underset{\dot{}}{\perp }\left(\left\{X\right\}\right)\leftrightarrow \underset{\dot{}}{\perp }\left(\left\{X\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{X\right\}\right)=V\right)$$
16	10 15	mpbid	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\left\{X\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{X\right\}\right)=V$$