Theorem lcfl5a

Description: Property of a functional with a closed kernel. TODO: Make lcfl5 etc. obsolete and rewrite without C hypothesis? (Contributed by NM, 29-Jan-2015)

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

Proof

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