Theorem dochkrsat2

Description: The orthocomplement of a kernel is an atom iff the double orthocomplement is not the vector space. (Contributed by NM, 1-Jan-2015)

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

Proof

Step	Hyp	Ref	Expression
1		dochkrsat2.h	|- H = ( LHyp ` K )
2		dochkrsat2.o	|- ._|_ = ( ( ocH ` K ) ` W )
3		dochkrsat2.u	|- U = ( ( DVecH ` K ) ` W )
4		dochkrsat2.v	|- V = ( Base ` U )
5		dochkrsat2.a	|- A = ( LSAtoms ` U )
6		dochkrsat2.f	|- F = ( LFnl ` U )
7		dochkrsat2.l	|- L = ( LKer ` U )
8		dochkrsat2.k	|- ( ph -> ( K e. HL /\ W e. H ) )
9		dochkrsat2.g	|- ( ph -> G e. F )
10		eqid	|- ( 0g ` U ) = ( 0g ` U )
11	1 3 8	dvhlmod	|- ( ph -> U e. LMod )
12	4 6 7 11 9	lkrssv	|- ( ph -> ( L ` G ) C_ V )
13	1 2 3 4 10 8 12	dochn0nv	|- ( ph -> ( ( ._|_ ` ( L ` G ) ) =/= { ( 0g ` U ) } <-> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= V ) )
14	1 2 3 5 6 7 10 8 9	dochkrsat	|- ( ph -> ( ( ._|_ ` ( L ` G ) ) =/= { ( 0g ` U ) } <-> ( ._|_ ` ( L ` G ) ) e. A ) )
15	13 14	bitr3d	|- ( ph -> ( ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= V <-> ( ._|_ ` ( L ` G ) ) e. A ) )