Theorem lcfl3

Description: Property of a functional with a closed kernel. (Contributed by NM, 1-Jan-2015)

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

Proof

Step	Hyp	Ref	Expression
1		lcfl3.h	|- H = ( LHyp ` K )
2		lcfl3.o	|- ._|_ = ( ( ocH ` K ) ` W )
3		lcfl3.u	|- U = ( ( DVecH ` K ) ` W )
4		lcfl3.v	|- V = ( Base ` U )
5		lcfl3.a	|- A = ( LSAtoms ` U )
6		lcfl3.f	|- F = ( LFnl ` U )
7		lcfl3.l	|- L = ( LKer ` U )
8		lcfl3.c	|- C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }
9		lcfl3.k	|- ( ph -> ( K e. HL /\ W e. H ) )
10		lcfl3.g	|- ( ph -> G e. F )
11	1 2 3 4 6 7 8 9 10	lcfl2	|- ( ph -> ( G e. C <-> ( ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= V \/ ( L ` G ) = V ) ) )
12	1 2 3 4 5 6 7 9 10	dochkrsat2	|- ( ph -> ( ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= V <-> ( ._|_ ` ( L ` G ) ) e. A ) )
13	12	orbi1d	|- ( ph -> ( ( ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= V \/ ( L ` G ) = V ) <-> ( ( ._|_ ` ( L ` G ) ) e. A \/ ( L ` G ) = V ) ) )
14	11 13	bitrd	|- ( ph -> ( G e. C <-> ( ( ._|_ ` ( L ` G ) ) e. A \/ ( L ` G ) = V ) ) )