Metamath Proof Explorer

Theorem lcdlvec

Description: The dual vector space of functionals with closed kernels is a left vector space. (Contributed by NM, 14-Mar-2015)

Ref Expression
Hypotheses lcdlmod.h 
|- H = ( LHyp ` K )
lcdlmod.c 
|- C = ( ( LCDual ` K ) ` W )
lcdlmod.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
Assertion lcdlvec 
|- ( ph -> C e. LVec )

Proof

Step Hyp Ref Expression
1 lcdlmod.h 
 |-  H = ( LHyp ` K )
2 lcdlmod.c 
 |-  C = ( ( LCDual ` K ) ` W )
3 lcdlmod.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
4 eqid 
 |-  ( ( ocH ` K ) ` W ) = ( ( ocH ` K ) ` W )
5 eqid 
 |-  ( ( DVecH ` K ) ` W ) = ( ( DVecH ` K ) ` W )
6 eqid 
 |-  ( LFnl ` ( ( DVecH ` K ) ` W ) ) = ( LFnl ` ( ( DVecH ` K ) ` W ) )
7 eqid 
 |-  ( LKer ` ( ( DVecH ` K ) ` W ) ) = ( LKer ` ( ( DVecH ` K ) ` W ) )
8 eqid 
 |-  ( LDual ` ( ( DVecH ` K ) ` W ) ) = ( LDual ` ( ( DVecH ` K ) ` W ) )
9 1 4 2 5 6 7 8 3 lcdval 
 |-  ( ph -> C = ( ( LDual ` ( ( DVecH ` K ) ` W ) ) |`s { f e. ( LFnl ` ( ( DVecH ` K ) ` W ) ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` ( ( DVecH ` K ) ` W ) ) ` f ) ) ) = ( ( LKer ` ( ( DVecH ` K ) ` W ) ) ` f ) } ) )
10 1 5 3 dvhlvec 
 |-  ( ph -> ( ( DVecH ` K ) ` W ) e. LVec )
11 8 10 lduallvec 
 |-  ( ph -> ( LDual ` ( ( DVecH ` K ) ` W ) ) e. LVec )
12 eqid 
 |-  ( LSubSp ` ( LDual ` ( ( DVecH ` K ) ` W ) ) ) = ( LSubSp ` ( LDual ` ( ( DVecH ` K ) ` W ) ) )
13 eqid 
 |-  { f e. ( LFnl ` ( ( DVecH ` K ) ` W ) ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` ( ( DVecH ` K ) ` W ) ) ` f ) ) ) = ( ( LKer ` ( ( DVecH ` K ) ` W ) ) ` f ) } = { f e. ( LFnl ` ( ( DVecH ` K ) ` W ) ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` ( ( DVecH ` K ) ` W ) ) ` f ) ) ) = ( ( LKer ` ( ( DVecH ` K ) ` W ) ) ` f ) }
14 1 5 4 6 7 8 12 13 3 lclkr 
 |-  ( ph -> { f e. ( LFnl ` ( ( DVecH ` K ) ` W ) ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` ( ( DVecH ` K ) ` W ) ) ` f ) ) ) = ( ( LKer ` ( ( DVecH ` K ) ` W ) ) ` f ) } e. ( LSubSp ` ( LDual ` ( ( DVecH ` K ) ` W ) ) ) )
15 eqid 
 |-  ( ( LDual ` ( ( DVecH ` K ) ` W ) ) |`s { f e. ( LFnl ` ( ( DVecH ` K ) ` W ) ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` ( ( DVecH ` K ) ` W ) ) ` f ) ) ) = ( ( LKer ` ( ( DVecH ` K ) ` W ) ) ` f ) } ) = ( ( LDual ` ( ( DVecH ` K ) ` W ) ) |`s { f e. ( LFnl ` ( ( DVecH ` K ) ` W ) ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` ( ( DVecH ` K ) ` W ) ) ` f ) ) ) = ( ( LKer ` ( ( DVecH ` K ) ` W ) ) ` f ) } )
16 15 12 lsslvec 
 |-  ( ( ( LDual ` ( ( DVecH ` K ) ` W ) ) e. LVec /\ { f e. ( LFnl ` ( ( DVecH ` K ) ` W ) ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` ( ( DVecH ` K ) ` W ) ) ` f ) ) ) = ( ( LKer ` ( ( DVecH ` K ) ` W ) ) ` f ) } e. ( LSubSp ` ( LDual ` ( ( DVecH ` K ) ` W ) ) ) ) -> ( ( LDual ` ( ( DVecH ` K ) ` W ) ) |`s { f e. ( LFnl ` ( ( DVecH ` K ) ` W ) ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` ( ( DVecH ` K ) ` W ) ) ` f ) ) ) = ( ( LKer ` ( ( DVecH ` K ) ` W ) ) ` f ) } ) e. LVec )
17 11 14 16 syl2anc 
 |-  ( ph -> ( ( LDual ` ( ( DVecH ` K ) ` W ) ) |`s { f e. ( LFnl ` ( ( DVecH ` K ) ` W ) ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` ( ( DVecH ` K ) ` W ) ) ` f ) ) ) = ( ( LKer ` ( ( DVecH ` K ) ` W ) ) ` f ) } ) e. LVec )
18 9 17 eqeltrd 
 |-  ( ph -> C e. LVec )