Theorem lcfl5

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

	Ref	Expression
Hypotheses	lcfl5.h	|- H = ( LHyp ` K )
	lcfl5.i	|- I = ( ( DIsoH ` K ) ` W )
	lcfl5.o	|- ._|_ = ( ( ocH ` K ) ` W )
	lcfl5.u	|- U = ( ( DVecH ` K ) ` W )
	lcfl5.f	|- F = ( LFnl ` U )
	lcfl5.l	|- L = ( LKer ` U )
	lcfl5.c	|- C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }
	lcfl5.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	lcfl5.g	|- ( ph -> G e. F )
Assertion	lcfl5	|- ( ph -> ( G e. C <-> ( L ` G ) e. ran I ) )

Proof

Step	Hyp	Ref	Expression
1		lcfl5.h	|- H = ( LHyp ` K )
2		lcfl5.i	|- I = ( ( DIsoH ` K ) ` W )
3		lcfl5.o	|- ._|_ = ( ( ocH ` K ) ` W )
4		lcfl5.u	|- U = ( ( DVecH ` K ) ` W )
5		lcfl5.f	|- F = ( LFnl ` U )
6		lcfl5.l	|- L = ( LKer ` U )
7		lcfl5.c	|- C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }
8		lcfl5.k	|- ( ph -> ( K e. HL /\ W e. H ) )
9		lcfl5.g	|- ( ph -> G e. F )
10	7 9	lcfl1	|- ( ph -> ( G e. C <-> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) ) )
11		eqid	|- ( Base ` U ) = ( Base ` U )
12	1 4 8	dvhlmod	|- ( ph -> U e. LMod )
13	11 5 6 12 9	lkrssv	|- ( ph -> ( L ` G ) C_ ( Base ` U ) )
14	1 2 4 11 3 8 13	dochoccl	|- ( ph -> ( ( L ` G ) e. ran I <-> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) ) )
15	10 14	bitr4d	|- ( ph -> ( G e. C <-> ( L ` G ) e. ran I ) )