Theorem dochnel2

Description: A nonzero member of a subspace doesn't belong to the orthocomplement of the subspace. (Contributed by NM, 28-Feb-2015)

	Ref	Expression
Hypotheses	dochnoncon.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dochnoncon.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	dochnoncon.s	$$⊢S=\mathrm{LSubSp}\left(U\right)$$
	dochnoncon.z	$$⊢\underset{\dot{}}{0}=0_U$$
	dochnoncon.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
	dochnel2.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	dochnel2.t	$$⊢\phi \to T\in S$$
	dochnel2.x	$$⊢\phi \to X\in \left(T\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
Assertion	dochnel2	$$⊢\phi \to \neg X\in \underset{\dot{}}{\perp }\left(T\right)$$

Proof

Step	Hyp	Ref	Expression
1		dochnoncon.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		dochnoncon.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		dochnoncon.s	$$⊢S=\mathrm{LSubSp}\left(U\right)$$
4		dochnoncon.z	$$⊢\underset{\dot{}}{0}=0_U$$
5		dochnoncon.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
6		dochnel2.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
7		dochnel2.t	$$⊢\phi \to T\in S$$
8		dochnel2.x	$$⊢\phi \to X\in \left(T\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
9	8	eldifbd	$$⊢\phi \to \neg X\in \left\{\underset{\dot{}}{0}\right\}$$
10	8	eldifad	$$⊢\phi \to X\in T$$
11		elin	$$⊢X\in \left(T\cap \underset{\dot{}}{\perp }\left(T\right)\right)\leftrightarrow \left(X\in T\wedge X\in \underset{\dot{}}{\perp }\left(T\right)\right)$$
12	1 2 3 4 5	dochnoncon	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge T\in S\right)\to T\cap \underset{\dot{}}{\perp }\left(T\right)=\left\{\underset{\dot{}}{0}\right\}$$
13	6 7 12	syl2anc	$$⊢\phi \to T\cap \underset{\dot{}}{\perp }\left(T\right)=\left\{\underset{\dot{}}{0}\right\}$$
14	13	eleq2d	$$⊢\phi \to \left(X\in \left(T\cap \underset{\dot{}}{\perp }\left(T\right)\right)\leftrightarrow X\in \left\{\underset{\dot{}}{0}\right\}\right)$$
15	11 14	bitr3id	$$⊢\phi \to \left(\left(X\in T\wedge X\in \underset{\dot{}}{\perp }\left(T\right)\right)\leftrightarrow X\in \left\{\underset{\dot{}}{0}\right\}\right)$$
16	15	biimpd	$$⊢\phi \to \left(\left(X\in T\wedge X\in \underset{\dot{}}{\perp }\left(T\right)\right)\to X\in \left\{\underset{\dot{}}{0}\right\}\right)$$
17	10 16	mpand	$$⊢\phi \to \left(X\in \underset{\dot{}}{\perp }\left(T\right)\to X\in \left\{\underset{\dot{}}{0}\right\}\right)$$
18	9 17	mtod	$$⊢\phi \to \neg X\in \underset{\dot{}}{\perp }\left(T\right)$$