Metamath Proof Explorer

Theorem lcd0v

Description: The zero functional in the set of functionals with closed kernels. (Contributed by NM, 20-Mar-2015)

Ref Expression
Hypotheses lcd0v.h 
|- H = ( LHyp ` K )
lcd0v.u 
|- U = ( ( DVecH ` K ) ` W )
lcd0v.v 
|- V = ( Base ` U )
lcd0v.r 
|- R = ( Scalar ` U )
lcd0v.z 
|- .0. = ( 0g ` R )
lcd0v.c 
|- C = ( ( LCDual ` K ) ` W )
lcd0v.o 
|- O = ( 0g ` C )
lcd0v.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
Assertion lcd0v 
|- ( ph -> O = ( V X. { .0. } ) )

Proof

Step Hyp Ref Expression
1 lcd0v.h 
 |-  H = ( LHyp ` K )
2 lcd0v.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 lcd0v.v 
 |-  V = ( Base ` U )
4 lcd0v.r 
 |-  R = ( Scalar ` U )
5 lcd0v.z 
 |-  .0. = ( 0g ` R )
6 lcd0v.c 
 |-  C = ( ( LCDual ` K ) ` W )
7 lcd0v.o 
 |-  O = ( 0g ` C )
8 lcd0v.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
9 eqid 
 |-  ( ( ocH ` K ) ` W ) = ( ( ocH ` K ) ` W )
10 eqid 
 |-  ( LFnl ` U ) = ( LFnl ` U )
11 eqid 
 |-  ( LKer ` U ) = ( LKer ` U )
12 eqid 
 |-  ( LDual ` U ) = ( LDual ` U )
13 1 9 6 2 10 11 12 8 lcdval 
 |-  ( ph -> C = ( ( LDual ` U ) |`s { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } ) )
14 13 fveq2d 
 |-  ( ph -> ( 0g ` C ) = ( 0g ` ( ( LDual ` U ) |`s { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } ) ) )
15 7 14 syl5eq 
 |-  ( ph -> O = ( 0g ` ( ( LDual ` U ) |`s { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } ) ) )
16 1 2 8 dvhlmod 
 |-  ( ph -> U e. LMod )
17 12 16 lduallmod 
 |-  ( ph -> ( LDual ` U ) e. LMod )
18 eqid 
 |-  ( LSubSp ` ( LDual ` U ) ) = ( LSubSp ` ( LDual ` U ) )
19 eqid 
 |-  { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } = { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) }
20 1 2 9 10 11 12 18 19 8 lclkr 
 |-  ( ph -> { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } e. ( LSubSp ` ( LDual ` U ) ) )
21 eqid 
 |-  ( ( LDual ` U ) |`s { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } ) = ( ( LDual ` U ) |`s { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } )
22 eqid 
 |-  ( 0g ` ( LDual ` U ) ) = ( 0g ` ( LDual ` U ) )
23 eqid 
 |-  ( 0g ` ( ( LDual ` U ) |`s { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } ) ) = ( 0g ` ( ( LDual ` U ) |`s { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } ) )
24 21 22 23 18 lss0v 
 |-  ( ( ( LDual ` U ) e. LMod /\ { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } e. ( LSubSp ` ( LDual ` U ) ) ) -> ( 0g ` ( ( LDual ` U ) |`s { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } ) ) = ( 0g ` ( LDual ` U ) ) )
25 17 20 24 syl2anc 
 |-  ( ph -> ( 0g ` ( ( LDual ` U ) |`s { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } ) ) = ( 0g ` ( LDual ` U ) ) )
26 3 4 5 12 22 16 ldual0v 
 |-  ( ph -> ( 0g ` ( LDual ` U ) ) = ( V X. { .0. } ) )
27 15 25 26 3eqtrd 
 |-  ( ph -> O = ( V X. { .0. } ) )