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 ) ) ) |
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 ) ) ) |