Theorem lcfl8a

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

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

Proof

Step	Hyp	Ref	Expression
1		lcfl8a.h	|- H = ( LHyp ` K )
2		lcfl8a.o	|- ._|_ = ( ( ocH ` K ) ` W )
3		lcfl8a.u	|- U = ( ( DVecH ` K ) ` W )
4		lcfl8a.v	|- V = ( Base ` U )
5		lcfl8a.f	|- F = ( LFnl ` U )
6		lcfl8a.l	|- L = ( LKer ` U )
7		lcfl8a.k	|- ( ph -> ( K e. HL /\ W e. H ) )
8		lcfl8a.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	lcfl8	|- ( ph -> ( G e. { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) } <-> E. x e. V ( L ` G ) = ( ._|_ ` { x } ) ) )
12	10 11	bitr3d	|- ( ph -> ( ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) <-> E. x e. V ( L ` G ) = ( ._|_ ` { x } ) ) )