Metamath Proof Explorer

Theorem lcdsca

Description: The ring of scalars of the closed kernel dual space. (Contributed by NM, 16-Mar-2015) (Revised by Mario Carneiro, 6-May-2015)

Ref Expression
Hypotheses lcdsca.h 
|- H = ( LHyp ` K )
lcdsca.u 
|- U = ( ( DVecH ` K ) ` W )
lcdsca.f 
|- F = ( Scalar ` U )
lcdsca.o 
|- O = ( oppR ` F )
lcdsca.c 
|- C = ( ( LCDual ` K ) ` W )
lcdsca.r 
|- R = ( Scalar ` C )
lcdsca.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
Assertion lcdsca 
|- ( ph -> R = O )

Proof

Step Hyp Ref Expression
1 lcdsca.h 
 |-  H = ( LHyp ` K )
2 lcdsca.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 lcdsca.f 
 |-  F = ( Scalar ` U )
4 lcdsca.o 
 |-  O = ( oppR ` F )
5 lcdsca.c 
 |-  C = ( ( LCDual ` K ) ` W )
6 lcdsca.r 
 |-  R = ( Scalar ` C )
7 lcdsca.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 eqid 
 |-  ( LDual ` U ) = ( LDual ` U )
12 1 8 5 2 9 10 11 7 lcdval 
 |-  ( ph -> C = ( ( LDual ` U ) |`s { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } ) )
13 12 fveq2d 
 |-  ( ph -> ( Scalar ` C ) = ( Scalar ` ( ( LDual ` U ) |`s { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } ) ) )
14 fvex 
 |-  ( LFnl ` U ) e. _V
15 14 rabex 
 |-  { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } e. _V
16 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 ) } )
17 eqid 
 |-  ( Scalar ` ( LDual ` U ) ) = ( Scalar ` ( LDual ` U ) )
18 16 17 resssca 
 |-  ( { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } e. _V -> ( Scalar ` ( LDual ` U ) ) = ( Scalar ` ( ( LDual ` U ) |`s { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } ) ) )
19 15 18 ax-mp 
 |-  ( Scalar ` ( LDual ` U ) ) = ( Scalar ` ( ( LDual ` U ) |`s { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } ) )
20 13 19 eqtr4di 
 |-  ( ph -> ( Scalar ` C ) = ( Scalar ` ( LDual ` U ) ) )
21 1 2 7 dvhlmod 
 |-  ( ph -> U e. LMod )
22 3 4 11 17 21 ldualsca 
 |-  ( ph -> ( Scalar ` ( LDual ` U ) ) = O )
23 20 22 eqtrd 
 |-  ( ph -> ( Scalar ` C ) = O )
24 6 23 syl5eq 
 |-  ( ph -> R = O )