Metamath Proof Explorer

Theorem lclkrlem2

Description: The set of functionals having closed kernels is closed under vector (functional) addition. Lemmas lclkrlem2a through lclkrlem2y are used for the proof. Here we express lclkrlem2y in terms of membership in the set C of functionals with closed kernels. (Contributed by NM, 18-Jan-2015)

Ref Expression
Hypotheses lclkrlem2.h 
|- H = ( LHyp ` K )
lclkrlem2.o 
|- ._|_ = ( ( ocH ` K ) ` W )
lclkrlem2.u 
|- U = ( ( DVecH ` K ) ` W )
lclkrlem2.f 
|- F = ( LFnl ` U )
lclkrlem2.l 
|- L = ( LKer ` U )
lclkrlem2.d 
|- D = ( LDual ` U )
lclkrlem2.p 
|- .+ = ( +g ` D )
lclkrlem2.c 
|- C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }
lclkrlem2.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
lclkrlem2.e 
|- ( ph -> E e. C )
lclkrlem2.g 
|- ( ph -> G e. C )
Assertion lclkrlem2 
|- ( ph -> ( E .+ G ) e. C )

Proof

Step Hyp Ref Expression
1 lclkrlem2.h 
 |-  H = ( LHyp ` K )
2 lclkrlem2.o 
 |-  ._|_ = ( ( ocH ` K ) ` W )
3 lclkrlem2.u 
 |-  U = ( ( DVecH ` K ) ` W )
4 lclkrlem2.f 
 |-  F = ( LFnl ` U )
5 lclkrlem2.l 
 |-  L = ( LKer ` U )
6 lclkrlem2.d 
 |-  D = ( LDual ` U )
7 lclkrlem2.p 
 |-  .+ = ( +g ` D )
8 lclkrlem2.c 
 |-  C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }
9 lclkrlem2.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
10 lclkrlem2.e 
 |-  ( ph -> E e. C )
11 lclkrlem2.g 
 |-  ( ph -> G e. C )
12 8 lcfl1lem 
 |-  ( E e. C <-> ( E e. F /\ ( ._|_ ` ( ._|_ ` ( L ` E ) ) ) = ( L ` E ) ) )
13 12 simplbi 
 |-  ( E e. C -> E e. F )
14 10 13 syl 
 |-  ( ph -> E e. F )
15 8 lcfl1lem 
 |-  ( G e. C <-> ( G e. F /\ ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) ) )
16 15 simplbi 
 |-  ( G e. C -> G e. F )
17 11 16 syl 
 |-  ( ph -> G e. F )
18 8 14 lcfl1 
 |-  ( ph -> ( E e. C <-> ( ._|_ ` ( ._|_ ` ( L ` E ) ) ) = ( L ` E ) ) )
19 10 18 mpbid 
 |-  ( ph -> ( ._|_ ` ( ._|_ ` ( L ` E ) ) ) = ( L ` E ) )
20 8 17 lcfl1 
 |-  ( ph -> ( G e. C <-> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) ) )
21 11 20 mpbid 
 |-  ( ph -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) )
22 5 1 2 3 4 6 7 9 14 17 19 21 lclkrlem2y 
 |-  ( ph -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) )
23 1 3 9 dvhlmod 
 |-  ( ph -> U e. LMod )
24 4 6 7 23 14 17 ldualvaddcl 
 |-  ( ph -> ( E .+ G ) e. F )
25 8 24 lcfl1 
 |-  ( ph -> ( ( E .+ G ) e. C <-> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) ) )
26 22 25 mpbird 
 |-  ( ph -> ( E .+ G ) e. C )