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 = ( LHyp ` K )
	dochsat0.o	|- ._|_ = ( ( ocH ` K ) ` W )
	dochsat0.u	|- U = ( ( DVecH ` K ) ` W )
	dochsat0.z	|- .0. = ( 0g ` U )
	dochsat0.a	|- A = ( LSAtoms ` U )
	dochsat0.f	|- F = ( LFnl ` U )
	dochsat0.l	|- L = ( LKer ` U )
	dochsat0.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	dochsat0.g	|- ( ph -> G e. F )
Assertion	dochsat0	|- ( ph -> ( ( ._|_ ` ( L ` G ) ) e. A \/ ( ._|_ ` ( L ` G ) ) = { .0. } ) )

Proof

Step	Hyp	Ref	Expression
1		dochsat0.h	|- H = ( LHyp ` K )
2		dochsat0.o	|- ._|_ = ( ( ocH ` K ) ` W )
3		dochsat0.u	|- U = ( ( DVecH ` K ) ` W )
4		dochsat0.z	|- .0. = ( 0g ` U )
5		dochsat0.a	|- A = ( LSAtoms ` U )
6		dochsat0.f	|- F = ( LFnl ` U )
7		dochsat0.l	|- L = ( LKer ` U )
8		dochsat0.k	|- ( ph -> ( K e. HL /\ W e. H ) )
9		dochsat0.g	|- ( ph -> G e. F )
10	1 2 3 5 6 7 4 8 9	dochkrsat	|- ( ph -> ( ( ._|_ ` ( L ` G ) ) =/= { .0. } <-> ( ._|_ ` ( L ` G ) ) e. A ) )
11	10	biimpd	|- ( ph -> ( ( ._|_ ` ( L ` G ) ) =/= { .0. } -> ( ._|_ ` ( L ` G ) ) e. A ) )
12	11	necon1bd	|- ( ph -> ( -. ( ._|_ ` ( L ` G ) ) e. A -> ( ._|_ ` ( L ` G ) ) = { .0. } ) )
13	12	orrd	|- ( ph -> ( ( ._|_ ` ( L ` G ) ) e. A \/ ( ._|_ ` ( L ` G ) ) = { .0. } ) )