Theorem lcfl1

Description: Property of a functional with a closed kernel. (Contributed by NM, 31-Dec-2014)

	Ref	Expression
Hypotheses	lcfl1.c	|- C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }
	lcfl1.g	|- ( ph -> G e. F )
Assertion	lcfl1	|- ( ph -> ( G e. C <-> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) ) )

Proof

Step	Hyp	Ref	Expression
1		lcfl1.c	|- C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }
2		lcfl1.g	|- ( ph -> G e. F )
3	1	lcfl1lem	|- ( G e. C <-> ( G e. F /\ ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) ) )
4	2	biantrurd	|- ( ph -> ( ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) <-> ( G e. F /\ ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) ) ) )
5	3 4	bitr4id	|- ( ph -> ( G e. C <-> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) ) )