Theorem dochsat0

Description: The orthocomplement of a kernel is either an atom or zero. (Contributed by NM, 29-Jan-2015)

	Ref	Expression
Hypotheses	dochsat0.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dochsat0.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
	dochsat0.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	dochsat0.z	$$⊢\underset{\dot{}}{0}=0_U$$
	dochsat0.a	$$⊢A=\mathrm{LSAtoms}\left(U\right)$$
	dochsat0.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
	dochsat0.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
	dochsat0.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	dochsat0.g	$$⊢\phi \to G\in F$$
Assertion	dochsat0	$$⊢\phi \to \left(\underset{\dot{}}{\perp }\left(L\left(G\right)\right)\in A\vee \underset{\dot{}}{\perp }\left(L\left(G\right)\right)=\left\{\underset{\dot{}}{0}\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		dochsat0.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		dochsat0.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
3		dochsat0.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
4		dochsat0.z	$$⊢\underset{\dot{}}{0}=0_U$$
5		dochsat0.a	$$⊢A=\mathrm{LSAtoms}\left(U\right)$$
6		dochsat0.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
7		dochsat0.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
8		dochsat0.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
9		dochsat0.g	$$⊢\phi \to G\in F$$
10	1 2 3 5 6 7 4 8 9	dochkrsat	$$⊢\phi \to \left(\underset{\dot{}}{\perp }\left(L\left(G\right)\right)\ne \left\{\underset{\dot{}}{0}\right\}\leftrightarrow \underset{\dot{}}{\perp }\left(L\left(G\right)\right)\in A\right)$$
11	10	biimpd	$$⊢\phi \to \left(\underset{\dot{}}{\perp }\left(L\left(G\right)\right)\ne \left\{\underset{\dot{}}{0}\right\}\to \underset{\dot{}}{\perp }\left(L\left(G\right)\right)\in A\right)$$
12	11	necon1bd	$$⊢\phi \to \left(\neg \underset{\dot{}}{\perp }\left(L\left(G\right)\right)\in A\to \underset{\dot{}}{\perp }\left(L\left(G\right)\right)=\left\{\underset{\dot{}}{0}\right\}\right)$$
13	12	orrd	$$⊢\phi \to \left(\underset{\dot{}}{\perp }\left(L\left(G\right)\right)\in A\vee \underset{\dot{}}{\perp }\left(L\left(G\right)\right)=\left\{\underset{\dot{}}{0}\right\}\right)$$