Metamath Proof Explorer


Theorem lcfl2

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

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

Proof

Step Hyp Ref Expression
1 lcfl2.h
 |-  H = ( LHyp ` K )
2 lcfl2.o
 |-  ._|_ = ( ( ocH ` K ) ` W )
3 lcfl2.u
 |-  U = ( ( DVecH ` K ) ` W )
4 lcfl2.v
 |-  V = ( Base ` U )
5 lcfl2.f
 |-  F = ( LFnl ` U )
6 lcfl2.l
 |-  L = ( LKer ` U )
7 lcfl2.c
 |-  C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }
8 lcfl2.k
 |-  ( ph -> ( K e. HL /\ W e. H ) )
9 lcfl2.g
 |-  ( ph -> G e. F )
10 7 9 lcfl1
 |-  ( ph -> ( G e. C <-> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) ) )
11 1 2 3 4 5 6 8 9 dochkrshp4
 |-  ( ph -> ( ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) <-> ( ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= V \/ ( L ` G ) = V ) ) )
12 10 11 bitrd
 |-  ( ph -> ( G e. C <-> ( ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= V \/ ( L ` G ) = V ) ) )