Metamath Proof Explorer

Theorem lcfls1c

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

Ref Expression
Hypotheses lcfls1.c 
|- C = { f e. F | ( ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) /\ ( ._|_ ` ( L ` f ) ) C_ Q ) }
lcfls1c.c 
|- D = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }
Assertion lcfls1c 
|- ( G e. C <-> ( G e. D /\ ( ._|_ ` ( L ` G ) ) C_ Q ) )

Proof

Step Hyp Ref Expression
1 lcfls1.c 
 |-  C = { f e. F | ( ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) /\ ( ._|_ ` ( L ` f ) ) C_ Q ) }
2 lcfls1c.c 
 |-  D = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }
3 df-3an 
 |-  ( ( G e. F /\ ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) /\ ( ._|_ ` ( L ` G ) ) C_ Q ) <-> ( ( G e. F /\ ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) ) /\ ( ._|_ ` ( L ` G ) ) C_ Q ) )
4 1 lcfls1lem 
 |-  ( G e. C <-> ( G e. F /\ ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) /\ ( ._|_ ` ( L ` G ) ) C_ Q ) )
5 2 lcfl1lem 
 |-  ( G e. D <-> ( G e. F /\ ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) ) )
6 5 anbi1i 
 |-  ( ( G e. D /\ ( ._|_ ` ( L ` G ) ) C_ Q ) <-> ( ( G e. F /\ ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) ) /\ ( ._|_ ` ( L ` G ) ) C_ Q ) )
7 3 4 6 3bitr4i 
 |-  ( G e. C <-> ( G e. D /\ ( ._|_ ` ( L ` G ) ) C_ Q ) )