Metamath Proof Explorer

Theorem lcdlsp

Description: Span in the set of functionals with closed kernels. (Contributed by NM, 28-Mar-2015)

Ref Expression
Hypotheses lcdlsp.h 
|- H = ( LHyp ` K )
lcdlsp.u 
|- U = ( ( DVecH ` K ) ` W )
lcdlsp.d 
|- D = ( LDual ` U )
lcdlsp.m 
|- M = ( LSpan ` D )
lcdlsp.c 
|- C = ( ( LCDual ` K ) ` W )
lcdlsp.f 
|- F = ( Base ` C )
lcdlsp.n 
|- N = ( LSpan ` C )
lcdlsp.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
lcdlsp.g 
|- ( ph -> G C_ F )
Assertion lcdlsp 
|- ( ph -> ( N ` G ) = ( M ` G ) )

Proof

Step Hyp Ref Expression
1 lcdlsp.h 
 |-  H = ( LHyp ` K )
2 lcdlsp.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 lcdlsp.d 
 |-  D = ( LDual ` U )
4 lcdlsp.m 
 |-  M = ( LSpan ` D )
5 lcdlsp.c 
 |-  C = ( ( LCDual ` K ) ` W )
6 lcdlsp.f 
 |-  F = ( Base ` C )
7 lcdlsp.n 
 |-  N = ( LSpan ` C )
8 lcdlsp.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
9 lcdlsp.g 
 |-  ( ph -> G C_ F )
10 eqid 
 |-  ( ( ocH ` K ) ` W ) = ( ( ocH ` K ) ` W )
11 eqid 
 |-  ( LFnl ` U ) = ( LFnl ` U )
12 eqid 
 |-  ( LKer ` U ) = ( LKer ` U )
13 1 10 5 2 11 12 3 8 lcdval 
 |-  ( ph -> C = ( D |`s { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } ) )
14 13 fveq2d 
 |-  ( ph -> ( LSpan ` C ) = ( LSpan ` ( D |`s { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } ) ) )
15 7 14 syl5eq 
 |-  ( ph -> N = ( LSpan ` ( D |`s { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } ) ) )
16 15 fveq1d 
 |-  ( ph -> ( N ` G ) = ( ( LSpan ` ( D |`s { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } ) ) ` G ) )
17 1 2 8 dvhlmod 
 |-  ( ph -> U e. LMod )
18 3 17 lduallmod 
 |-  ( ph -> D e. LMod )
19 eqid 
 |-  ( LSubSp ` D ) = ( LSubSp ` D )
20 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 ) }
21 1 2 10 11 12 3 19 20 8 lclkr 
 |-  ( ph -> { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } e. ( LSubSp ` D ) )
22 1 10 5 6 2 11 12 20 8 lcdvbase 
 |-  ( ph -> F = { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } )
23 9 22 sseqtrd 
 |-  ( ph -> G C_ { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } )
24 eqid 
 |-  ( D |`s { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } ) = ( D |`s { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } )
25 eqid 
 |-  ( LSpan ` ( D |`s { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } ) ) = ( LSpan ` ( D |`s { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } ) )
26 24 4 25 19 lsslsp 
 |-  ( ( D e. LMod /\ { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } e. ( LSubSp ` D ) /\ G C_ { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } ) -> ( M ` G ) = ( ( LSpan ` ( D |`s { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } ) ) ` G ) )
27 18 21 23 26 syl3anc 
 |-  ( ph -> ( M ` G ) = ( ( LSpan ` ( D |`s { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } ) ) ` G ) )
28 16 27 eqtr4d 
 |-  ( ph -> ( N ` G ) = ( M ` G ) )