Theorem dochkrsat

Description: The orthocomplement of a kernel is an atom iff it is nonzero. (Contributed by NM, 1-Nov-2014)

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

Proof

Step	Hyp	Ref	Expression
1		dochkrsat.h	|- H = ( LHyp ` K )
2		dochkrsat.o	|- ._|_ = ( ( ocH ` K ) ` W )
3		dochkrsat.u	|- U = ( ( DVecH ` K ) ` W )
4		dochkrsat.a	|- A = ( LSAtoms ` U )
5		dochkrsat.f	|- F = ( LFnl ` U )
6		dochkrsat.l	|- L = ( LKer ` U )
7		dochkrsat.z	|- .0. = ( 0g ` U )
8		dochkrsat.k	|- ( ph -> ( K e. HL /\ W e. H ) )
9		dochkrsat.g	|- ( ph -> G e. F )
10		eqid	|- ( Base ` U ) = ( Base ` U )
11		eqid	|- ( LSHyp ` U ) = ( LSHyp ` U )
12	1 2 3 10 11 5 6 8 9	dochkrshp	|- ( ph -> ( ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= ( Base ` U ) <-> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) e. ( LSHyp ` U ) ) )
13	1 3 8	dvhlmod	|- ( ph -> U e. LMod )
14	10 5 6 13 9	lkrssv	|- ( ph -> ( L ` G ) C_ ( Base ` U ) )
15	1 2 3 10 7 8 14	dochn0nv	|- ( ph -> ( ( ._|_ ` ( L ` G ) ) =/= { .0. } <-> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= ( Base ` U ) ) )
16		eqid	|- ( LSubSp ` U ) = ( LSubSp ` U )
17	1 3 10 16 2	dochlss	|- ( ( ( K e. HL /\ W e. H ) /\ ( L ` G ) C_ ( Base ` U ) ) -> ( ._|_ ` ( L ` G ) ) e. ( LSubSp ` U ) )
18	8 14 17	syl2anc	|- ( ph -> ( ._|_ ` ( L ` G ) ) e. ( LSubSp ` U ) )
19	1 2 3 16 4 11 8 18	dochsatshpb	|- ( ph -> ( ( ._|_ ` ( L ` G ) ) e. A <-> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) e. ( LSHyp ` U ) ) )
20	12 15 19	3bitr4d	|- ( ph -> ( ( ._|_ ` ( L ` G ) ) =/= { .0. } <-> ( ._|_ ` ( L ` G ) ) e. A ) )