Metamath Proof Explorer

Theorem lcdvs

Description: Scalar product for the closed kernel vector space dual. (Contributed by NM, 28-Mar-2015)

Ref Expression
Hypotheses lcdvs.h 
|- H = ( LHyp ` K )
lcdvs.u 
|- U = ( ( DVecH ` K ) ` W )
lcdvs.d 
|- D = ( LDual ` U )
lcdvs.t 
|- .x. = ( .s ` D )
lcdvs.c 
|- C = ( ( LCDual ` K ) ` W )
lcdvs.m 
|- .xb = ( .s ` C )
lcdvs.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
Assertion lcdvs 
|- ( ph -> .xb = .x. )

Proof

Step Hyp Ref Expression
1 lcdvs.h 
 |-  H = ( LHyp ` K )
2 lcdvs.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 lcdvs.d 
 |-  D = ( LDual ` U )
4 lcdvs.t 
 |-  .x. = ( .s ` D )
5 lcdvs.c 
 |-  C = ( ( LCDual ` K ) ` W )
6 lcdvs.m 
 |-  .xb = ( .s ` C )
7 lcdvs.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
8 eqid 
 |-  ( ( ocH ` K ) ` W ) = ( ( ocH ` K ) ` W )
9 eqid 
 |-  ( LFnl ` U ) = ( LFnl ` U )
10 eqid 
 |-  ( LKer ` U ) = ( LKer ` U )
11 1 8 5 2 9 10 3 7 lcdval 
 |-  ( ph -> C = ( D |`s { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } ) )
12 11 fveq2d 
 |-  ( ph -> ( .s ` C ) = ( .s ` ( D |`s { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } ) ) )
13 fvex 
 |-  ( LFnl ` U ) e. _V
14 13 rabex 
 |-  { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } e. _V
15 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 ) } )
16 15 4 ressvsca 
 |-  ( { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } e. _V -> .x. = ( .s ` ( D |`s { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } ) ) )
17 14 16 ax-mp 
 |-  .x. = ( .s ` ( D |`s { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } ) )
18 12 6 17 3eqtr4g 
 |-  ( ph -> .xb = .x. )