Metamath Proof Explorer

Theorem lclkrlem1

Description: The set of functionals having closed kernels is closed under scalar product. (Contributed by NM, 28-Dec-2014)

Ref Expression
Hypotheses lclkrlem1.h 
|- H = ( LHyp ` K )
lclkrlem1.o 
|- ._|_ = ( ( ocH ` K ) ` W )
lclkrlem1.u 
|- U = ( ( DVecH ` K ) ` W )
lclkrlem1.f 
|- F = ( LFnl ` U )
lclkrlem1.l 
|- L = ( LKer ` U )
lclkrlem1.d 
|- D = ( LDual ` U )
lclkrlem1.r 
|- R = ( Scalar ` U )
lclkrlem1.b 
|- B = ( Base ` R )
lclkrlem1.t 
|- .x. = ( .s ` D )
lclkrlem1.c 
|- C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }
lclkrlem1.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
lclkrlem1.x 
|- ( ph -> X e. B )
lclkrlem1.g 
|- ( ph -> G e. C )
Assertion lclkrlem1 
|- ( ph -> ( X .x. G ) e. C )

Proof

Step Hyp Ref Expression
1 lclkrlem1.h 
 |-  H = ( LHyp ` K )
2 lclkrlem1.o 
 |-  ._|_ = ( ( ocH ` K ) ` W )
3 lclkrlem1.u 
 |-  U = ( ( DVecH ` K ) ` W )
4 lclkrlem1.f 
 |-  F = ( LFnl ` U )
5 lclkrlem1.l 
 |-  L = ( LKer ` U )
6 lclkrlem1.d 
 |-  D = ( LDual ` U )
7 lclkrlem1.r 
 |-  R = ( Scalar ` U )
8 lclkrlem1.b 
 |-  B = ( Base ` R )
9 lclkrlem1.t 
 |-  .x. = ( .s ` D )
10 lclkrlem1.c 
 |-  C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }
11 lclkrlem1.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
12 lclkrlem1.x 
 |-  ( ph -> X e. B )
13 lclkrlem1.g 
 |-  ( ph -> G e. C )
14 1 3 11 dvhlmod 
 |-  ( ph -> U e. LMod )
15 10 lcfl1lem 
 |-  ( G e. C <-> ( G e. F /\ ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) ) )
16 13 15 sylib 
 |-  ( ph -> ( G e. F /\ ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) ) )
17 16 simpld 
 |-  ( ph -> G e. F )
18 4 7 8 6 9 14 12 17 ldualvscl 
 |-  ( ph -> ( X .x. G ) e. F )
19 eqid 
 |-  ( Base ` U ) = ( Base ` U )
20 1 3 2 19 11 dochoc1 
 |-  ( ph -> ( ._|_ ` ( ._|_ ` ( Base ` U ) ) ) = ( Base ` U ) )
21 20 adantr 
 |-  ( ( ph /\ X = ( 0g ` R ) ) -> ( ._|_ ` ( ._|_ ` ( Base ` U ) ) ) = ( Base ` U ) )
22 fvoveq1 
 |-  ( X = ( 0g ` R ) -> ( L ` ( X .x. G ) ) = ( L ` ( ( 0g ` R ) .x. G ) ) )
23 6 14 lduallmod 
 |-  ( ph -> D e. LMod )
24 eqid 
 |-  ( Base ` D ) = ( Base ` D )
25 4 6 24 14 17 ldualelvbase 
 |-  ( ph -> G e. ( Base ` D ) )
26 eqid 
 |-  ( Scalar ` D ) = ( Scalar ` D )
27 eqid 
 |-  ( 0g ` ( Scalar ` D ) ) = ( 0g ` ( Scalar ` D ) )
28 eqid 
 |-  ( 0g ` D ) = ( 0g ` D )
29 24 26 9 27 28 lmod0vs 
 |-  ( ( D e. LMod /\ G e. ( Base ` D ) ) -> ( ( 0g ` ( Scalar ` D ) ) .x. G ) = ( 0g ` D ) )
30 23 25 29 syl2anc 
 |-  ( ph -> ( ( 0g ` ( Scalar ` D ) ) .x. G ) = ( 0g ` D ) )
31 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
32 7 31 6 26 27 14 ldual0 
 |-  ( ph -> ( 0g ` ( Scalar ` D ) ) = ( 0g ` R ) )
33 32 oveq1d 
 |-  ( ph -> ( ( 0g ` ( Scalar ` D ) ) .x. G ) = ( ( 0g ` R ) .x. G ) )
34 19 7 31 6 28 14 ldual0v 
 |-  ( ph -> ( 0g ` D ) = ( ( Base ` U ) X. { ( 0g ` R ) } ) )
35 30 33 34 3eqtr3d 
 |-  ( ph -> ( ( 0g ` R ) .x. G ) = ( ( Base ` U ) X. { ( 0g ` R ) } ) )
36 35 fveq2d 
 |-  ( ph -> ( L ` ( ( 0g ` R ) .x. G ) ) = ( L ` ( ( Base ` U ) X. { ( 0g ` R ) } ) ) )
37 eqid 
 |-  ( ( Base ` U ) X. { ( 0g ` R ) } ) = ( ( Base ` U ) X. { ( 0g ` R ) } )
38 7 31 19 4 lfl0f 
 |-  ( U e. LMod -> ( ( Base ` U ) X. { ( 0g ` R ) } ) e. F )
39 7 31 19 4 5 lkr0f 
 |-  ( ( U e. LMod /\ ( ( Base ` U ) X. { ( 0g ` R ) } ) e. F ) -> ( ( L ` ( ( Base ` U ) X. { ( 0g ` R ) } ) ) = ( Base ` U ) <-> ( ( Base ` U ) X. { ( 0g ` R ) } ) = ( ( Base ` U ) X. { ( 0g ` R ) } ) ) )
40 14 38 39 syl2anc2 
 |-  ( ph -> ( ( L ` ( ( Base ` U ) X. { ( 0g ` R ) } ) ) = ( Base ` U ) <-> ( ( Base ` U ) X. { ( 0g ` R ) } ) = ( ( Base ` U ) X. { ( 0g ` R ) } ) ) )
41 37 40 mpbiri 
 |-  ( ph -> ( L ` ( ( Base ` U ) X. { ( 0g ` R ) } ) ) = ( Base ` U ) )
42 36 41 eqtrd 
 |-  ( ph -> ( L ` ( ( 0g ` R ) .x. G ) ) = ( Base ` U ) )
43 22 42 sylan9eqr 
 |-  ( ( ph /\ X = ( 0g ` R ) ) -> ( L ` ( X .x. G ) ) = ( Base ` U ) )
44 43 fveq2d 
 |-  ( ( ph /\ X = ( 0g ` R ) ) -> ( ._|_ ` ( L ` ( X .x. G ) ) ) = ( ._|_ ` ( Base ` U ) ) )
45 44 fveq2d 
 |-  ( ( ph /\ X = ( 0g ` R ) ) -> ( ._|_ ` ( ._|_ ` ( L ` ( X .x. G ) ) ) ) = ( ._|_ ` ( ._|_ ` ( Base ` U ) ) ) )
46 21 45 43 3eqtr4d 
 |-  ( ( ph /\ X = ( 0g ` R ) ) -> ( ._|_ ` ( ._|_ ` ( L ` ( X .x. G ) ) ) ) = ( L ` ( X .x. G ) ) )
47 16 simprd 
 |-  ( ph -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) )
48 47 adantr 
 |-  ( ( ph /\ X =/= ( 0g ` R ) ) -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) )
49 1 3 11 dvhlvec 
 |-  ( ph -> U e. LVec )
50 49 adantr 
 |-  ( ( ph /\ X =/= ( 0g ` R ) ) -> U e. LVec )
51 17 adantr 
 |-  ( ( ph /\ X =/= ( 0g ` R ) ) -> G e. F )
52 12 adantr 
 |-  ( ( ph /\ X =/= ( 0g ` R ) ) -> X e. B )
53 simpr 
 |-  ( ( ph /\ X =/= ( 0g ` R ) ) -> X =/= ( 0g ` R ) )
54 7 8 31 4 5 6 9 50 51 52 53 ldualkrsc 
 |-  ( ( ph /\ X =/= ( 0g ` R ) ) -> ( L ` ( X .x. G ) ) = ( L ` G ) )
55 54 fveq2d 
 |-  ( ( ph /\ X =/= ( 0g ` R ) ) -> ( ._|_ ` ( L ` ( X .x. G ) ) ) = ( ._|_ ` ( L ` G ) ) )
56 55 fveq2d 
 |-  ( ( ph /\ X =/= ( 0g ` R ) ) -> ( ._|_ ` ( ._|_ ` ( L ` ( X .x. G ) ) ) ) = ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) )
57 48 56 54 3eqtr4d 
 |-  ( ( ph /\ X =/= ( 0g ` R ) ) -> ( ._|_ ` ( ._|_ ` ( L ` ( X .x. G ) ) ) ) = ( L ` ( X .x. G ) ) )
58 46 57 pm2.61dane 
 |-  ( ph -> ( ._|_ ` ( ._|_ ` ( L ` ( X .x. G ) ) ) ) = ( L ` ( X .x. G ) ) )
59 10 lcfl1lem 
 |-  ( ( X .x. G ) e. C <-> ( ( X .x. G ) e. F /\ ( ._|_ ` ( ._|_ ` ( L ` ( X .x. G ) ) ) ) = ( L ` ( X .x. G ) ) ) )
60 18 58 59 sylanbrc 
 |-  ( ph -> ( X .x. G ) e. C )