Metamath Proof Explorer

Theorem lcfr

Description: Reconstruction of a subspace from a dual subspace of functionals with closed kernels. Our proof was suggested by Mario Carneiro, 20-Feb-2015. (Contributed by NM, 5-Mar-2015)

Ref Expression
Hypotheses lcfr.h 
|- H = ( LHyp ` K )
lcfr.o 
|- ._|_ = ( ( ocH ` K ) ` W )
lcfr.u 
|- U = ( ( DVecH ` K ) ` W )
lcfr.s 
|- S = ( LSubSp ` U )
lcfr.f 
|- F = ( LFnl ` U )
lcfr.l 
|- L = ( LKer ` U )
lcfr.d 
|- D = ( LDual ` U )
lcfr.t 
|- T = ( LSubSp ` D )
lcfr.c 
|- C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }
lcfr.q 
|- Q = U_ g e. R ( ._|_ ` ( L ` g ) )
lcfr.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
lcfr.r 
|- ( ph -> R e. T )
lcfr.rs 
|- ( ph -> R C_ C )
Assertion lcfr 
|- ( ph -> Q e. S )

Proof

Step Hyp Ref Expression
1 lcfr.h 
 |-  H = ( LHyp ` K )
2 lcfr.o 
 |-  ._|_ = ( ( ocH ` K ) ` W )
3 lcfr.u 
 |-  U = ( ( DVecH ` K ) ` W )
4 lcfr.s 
 |-  S = ( LSubSp ` U )
5 lcfr.f 
 |-  F = ( LFnl ` U )
6 lcfr.l 
 |-  L = ( LKer ` U )
7 lcfr.d 
 |-  D = ( LDual ` U )
8 lcfr.t 
 |-  T = ( LSubSp ` D )
9 lcfr.c 
 |-  C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }
10 lcfr.q 
 |-  Q = U_ g e. R ( ._|_ ` ( L ` g ) )
11 lcfr.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
12 lcfr.r 
 |-  ( ph -> R e. T )
13 lcfr.rs 
 |-  ( ph -> R C_ C )
14 2fveq3 
 |-  ( g = h -> ( ._|_ ` ( L ` g ) ) = ( ._|_ ` ( L ` h ) ) )
15 14 cbviunv 
 |-  U_ g e. R ( ._|_ ` ( L ` g ) ) = U_ h e. R ( ._|_ ` ( L ` h ) )
16 10 15 eqtri 
 |-  Q = U_ h e. R ( ._|_ ` ( L ` h ) )
17 11 adantr 
 |-  ( ( ph /\ h e. R ) -> ( K e. HL /\ W e. H ) )
18 eqid 
 |-  ( Base ` U ) = ( Base ` U )
19 1 3 11 dvhlmod 
 |-  ( ph -> U e. LMod )
20 19 adantr 
 |-  ( ( ph /\ h e. R ) -> U e. LMod )
21 eqid 
 |-  ( Base ` D ) = ( Base ` D )
22 21 8 lssss 
 |-  ( R e. T -> R C_ ( Base ` D ) )
23 12 22 syl 
 |-  ( ph -> R C_ ( Base ` D ) )
24 5 7 21 19 ldualvbase 
 |-  ( ph -> ( Base ` D ) = F )
25 23 24 sseqtrd 
 |-  ( ph -> R C_ F )
26 25 sselda 
 |-  ( ( ph /\ h e. R ) -> h e. F )
27 18 5 6 20 26 lkrssv 
 |-  ( ( ph /\ h e. R ) -> ( L ` h ) C_ ( Base ` U ) )
28 1 3 18 2 dochssv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( L ` h ) C_ ( Base ` U ) ) -> ( ._|_ ` ( L ` h ) ) C_ ( Base ` U ) )
29 17 27 28 syl2anc 
 |-  ( ( ph /\ h e. R ) -> ( ._|_ ` ( L ` h ) ) C_ ( Base ` U ) )
30 29 ralrimiva 
 |-  ( ph -> A. h e. R ( ._|_ ` ( L ` h ) ) C_ ( Base ` U ) )
31 iunss 
 |-  ( U_ h e. R ( ._|_ ` ( L ` h ) ) C_ ( Base ` U ) <-> A. h e. R ( ._|_ ` ( L ` h ) ) C_ ( Base ` U ) )
32 30 31 sylibr 
 |-  ( ph -> U_ h e. R ( ._|_ ` ( L ` h ) ) C_ ( Base ` U ) )
33 16 32 eqsstrid 
 |-  ( ph -> Q C_ ( Base ` U ) )
34 16 a1i 
 |-  ( ph -> Q = U_ h e. R ( ._|_ ` ( L ` h ) ) )
35 7 19 lduallmod 
 |-  ( ph -> D e. LMod )
36 eqid 
 |-  ( 0g ` D ) = ( 0g ` D )
37 36 8 lss0cl 
 |-  ( ( D e. LMod /\ R e. T ) -> ( 0g ` D ) e. R )
38 35 12 37 syl2anc 
 |-  ( ph -> ( 0g ` D ) e. R )
39 5 7 36 19 ldual0vcl 
 |-  ( ph -> ( 0g ` D ) e. F )
40 18 5 6 19 39 lkrssv 
 |-  ( ph -> ( L ` ( 0g ` D ) ) C_ ( Base ` U ) )
41 1 3 18 4 2 dochlss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( L ` ( 0g ` D ) ) C_ ( Base ` U ) ) -> ( ._|_ ` ( L ` ( 0g ` D ) ) ) e. S )
42 11 40 41 syl2anc 
 |-  ( ph -> ( ._|_ ` ( L ` ( 0g ` D ) ) ) e. S )
43 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
44 43 4 lss0cl 
 |-  ( ( U e. LMod /\ ( ._|_ ` ( L ` ( 0g ` D ) ) ) e. S ) -> ( 0g ` U ) e. ( ._|_ ` ( L ` ( 0g ` D ) ) ) )
45 19 42 44 syl2anc 
 |-  ( ph -> ( 0g ` U ) e. ( ._|_ ` ( L ` ( 0g ` D ) ) ) )
46 2fveq3 
 |-  ( h = ( 0g ` D ) -> ( ._|_ ` ( L ` h ) ) = ( ._|_ ` ( L ` ( 0g ` D ) ) ) )
47 46 eleq2d 
 |-  ( h = ( 0g ` D ) -> ( ( 0g ` U ) e. ( ._|_ ` ( L ` h ) ) <-> ( 0g ` U ) e. ( ._|_ ` ( L ` ( 0g ` D ) ) ) ) )
48 47 rspcev 
 |-  ( ( ( 0g ` D ) e. R /\ ( 0g ` U ) e. ( ._|_ ` ( L ` ( 0g ` D ) ) ) ) -> E. h e. R ( 0g ` U ) e. ( ._|_ ` ( L ` h ) ) )
49 38 45 48 syl2anc 
 |-  ( ph -> E. h e. R ( 0g ` U ) e. ( ._|_ ` ( L ` h ) ) )
50 eliun 
 |-  ( ( 0g ` U ) e. U_ h e. R ( ._|_ ` ( L ` h ) ) <-> E. h e. R ( 0g ` U ) e. ( ._|_ ` ( L ` h ) ) )
51 49 50 sylibr 
 |-  ( ph -> ( 0g ` U ) e. U_ h e. R ( ._|_ ` ( L ` h ) ) )
52 51 ne0d 
 |-  ( ph -> U_ h e. R ( ._|_ ` ( L ` h ) ) =/= (/) )
53 34 52 eqnetrd 
 |-  ( ph -> Q =/= (/) )
54 eqid 
 |-  ( +g ` U ) = ( +g ` U )
55 rabeq 
 |-  ( F = ( LFnl ` U ) -> { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) } = { f e. ( LFnl ` U ) | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) } )
56 5 55 ax-mp 
 |-  { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) } = { f e. ( LFnl ` U ) | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }
57 9 56 eqtri 
 |-  C = { f e. ( LFnl ` U ) | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }
58 11 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` U ) ) /\ a e. Q /\ b e. Q ) ) -> ( K e. HL /\ W e. H ) )
59 12 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` U ) ) /\ a e. Q /\ b e. Q ) ) -> R e. T )
60 13 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` U ) ) /\ a e. Q /\ b e. Q ) ) -> R C_ C )
61 simpr2 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` U ) ) /\ a e. Q /\ b e. Q ) ) -> a e. Q )
62 eqid 
 |-  ( Scalar ` U ) = ( Scalar ` U )
63 eqid 
 |-  ( Base ` ( Scalar ` U ) ) = ( Base ` ( Scalar ` U ) )
64 eqid 
 |-  ( .s ` U ) = ( .s ` U )
65 simpr1 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` U ) ) /\ a e. Q /\ b e. Q ) ) -> x e. ( Base ` ( Scalar ` U ) ) )
66 1 2 3 18 5 6 7 8 58 59 16 61 62 63 64 65 lcfrlem5 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` U ) ) /\ a e. Q /\ b e. Q ) ) -> ( x ( .s ` U ) a ) e. Q )
67 simpr3 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` U ) ) /\ a e. Q /\ b e. Q ) ) -> b e. Q )
68 1 2 3 54 5 6 7 8 57 16 58 59 60 66 67 lcfrlem42 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` U ) ) /\ a e. Q /\ b e. Q ) ) -> ( ( x ( .s ` U ) a ) ( +g ` U ) b ) e. Q )
69 68 ralrimivvva 
 |-  ( ph -> A. x e. ( Base ` ( Scalar ` U ) ) A. a e. Q A. b e. Q ( ( x ( .s ` U ) a ) ( +g ` U ) b ) e. Q )
70 62 63 18 54 64 4 islss 
 |-  ( Q e. S <-> ( Q C_ ( Base ` U ) /\ Q =/= (/) /\ A. x e. ( Base ` ( Scalar ` U ) ) A. a e. Q A. b e. Q ( ( x ( .s ` U ) a ) ( +g ` U ) b ) e. Q ) )
71 33 53 69 70 syl3anbrc 
 |-  ( ph -> Q e. S )