Metamath Proof Explorer

Theorem lcfrvalsnN

Description: Reconstruction from the dual space span of a singleton. (Contributed by NM, 19-Feb-2015) (New usage is discouraged.)

Ref Expression
Hypotheses lcfrvalsn.h 
|- H = ( LHyp ` K )
lcfrvalsn.o 
|- ._|_ = ( ( ocH ` K ) ` W )
lcfrvalsn.u 
|- U = ( ( DVecH ` K ) ` W )
lcfrvalsn.f 
|- F = ( LFnl ` U )
lcfrvalsn.l 
|- L = ( LKer ` U )
lcfrvalsn.d 
|- D = ( LDual ` U )
lcfrvalsn.n 
|- N = ( LSpan ` D )
lcfrvalsn.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
lcfrvalsn.g 
|- ( ph -> G e. F )
lcfrvalsn.q 
|- Q = U_ f e. R ( ._|_ ` ( L ` f ) )
lcfrvalsn.r 
|- R = ( N ` { G } )
Assertion lcfrvalsnN 
|- ( ph -> Q = ( ._|_ ` ( L ` G ) ) )

Proof

Step Hyp Ref Expression
1 lcfrvalsn.h 
 |-  H = ( LHyp ` K )
2 lcfrvalsn.o 
 |-  ._|_ = ( ( ocH ` K ) ` W )
3 lcfrvalsn.u 
 |-  U = ( ( DVecH ` K ) ` W )
4 lcfrvalsn.f 
 |-  F = ( LFnl ` U )
5 lcfrvalsn.l 
 |-  L = ( LKer ` U )
6 lcfrvalsn.d 
 |-  D = ( LDual ` U )
7 lcfrvalsn.n 
 |-  N = ( LSpan ` D )
8 lcfrvalsn.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
9 lcfrvalsn.g 
 |-  ( ph -> G e. F )
10 lcfrvalsn.q 
 |-  Q = U_ f e. R ( ._|_ ` ( L ` f ) )
11 lcfrvalsn.r 
 |-  R = ( N ` { G } )
12 eliun 
 |-  ( x e. U_ f e. R ( ._|_ ` ( L ` f ) ) <-> E. f e. R x e. ( ._|_ ` ( L ` f ) ) )
13 11 eleq2i 
 |-  ( f e. R <-> f e. ( N ` { G } ) )
14 8 adantr 
 |-  ( ( ph /\ f e. ( N ` { G } ) ) -> ( K e. HL /\ W e. H ) )
15 eqid 
 |-  ( Base ` U ) = ( Base ` U )
16 1 3 8 dvhlmod 
 |-  ( ph -> U e. LMod )
17 16 adantr 
 |-  ( ( ph /\ f e. ( N ` { G } ) ) -> U e. LMod )
18 6 16 lduallmod 
 |-  ( ph -> D e. LMod )
19 eqid 
 |-  ( Base ` D ) = ( Base ` D )
20 4 6 19 16 9 ldualelvbase 
 |-  ( ph -> G e. ( Base ` D ) )
21 eqid 
 |-  ( LSubSp ` D ) = ( LSubSp ` D )
22 19 21 7 lspsncl 
 |-  ( ( D e. LMod /\ G e. ( Base ` D ) ) -> ( N ` { G } ) e. ( LSubSp ` D ) )
23 18 20 22 syl2anc 
 |-  ( ph -> ( N ` { G } ) e. ( LSubSp ` D ) )
24 19 21 lssel 
 |-  ( ( ( N ` { G } ) e. ( LSubSp ` D ) /\ f e. ( N ` { G } ) ) -> f e. ( Base ` D ) )
25 23 24 sylan 
 |-  ( ( ph /\ f e. ( N ` { G } ) ) -> f e. ( Base ` D ) )
26 4 6 19 16 ldualvbase 
 |-  ( ph -> ( Base ` D ) = F )
27 26 adantr 
 |-  ( ( ph /\ f e. ( N ` { G } ) ) -> ( Base ` D ) = F )
28 25 27 eleqtrd 
 |-  ( ( ph /\ f e. ( N ` { G } ) ) -> f e. F )
29 15 4 5 17 28 lkrssv 
 |-  ( ( ph /\ f e. ( N ` { G } ) ) -> ( L ` f ) C_ ( Base ` U ) )
30 eqid 
 |-  ( Scalar ` D ) = ( Scalar ` D )
31 eqid 
 |-  ( Base ` ( Scalar ` D ) ) = ( Base ` ( Scalar ` D ) )
32 eqid 
 |-  ( .s ` D ) = ( .s ` D )
33 30 31 19 32 7 lspsnel 
 |-  ( ( D e. LMod /\ G e. ( Base ` D ) ) -> ( f e. ( N ` { G } ) <-> E. k e. ( Base ` ( Scalar ` D ) ) f = ( k ( .s ` D ) G ) ) )
34 18 20 33 syl2anc 
 |-  ( ph -> ( f e. ( N ` { G } ) <-> E. k e. ( Base ` ( Scalar ` D ) ) f = ( k ( .s ` D ) G ) ) )
35 eqid 
 |-  ( Scalar ` U ) = ( Scalar ` U )
36 eqid 
 |-  ( Base ` ( Scalar ` U ) ) = ( Base ` ( Scalar ` U ) )
37 35 36 6 30 31 16 ldualsbase 
 |-  ( ph -> ( Base ` ( Scalar ` D ) ) = ( Base ` ( Scalar ` U ) ) )
38 37 rexeqdv 
 |-  ( ph -> ( E. k e. ( Base ` ( Scalar ` D ) ) f = ( k ( .s ` D ) G ) <-> E. k e. ( Base ` ( Scalar ` U ) ) f = ( k ( .s ` D ) G ) ) )
39 34 38 bitrd 
 |-  ( ph -> ( f e. ( N ` { G } ) <-> E. k e. ( Base ` ( Scalar ` U ) ) f = ( k ( .s ` D ) G ) ) )
40 39 biimpa 
 |-  ( ( ph /\ f e. ( N ` { G } ) ) -> E. k e. ( Base ` ( Scalar ` U ) ) f = ( k ( .s ` D ) G ) )
41 1 3 8 dvhlvec 
 |-  ( ph -> U e. LVec )
42 41 adantr 
 |-  ( ( ph /\ f e. ( N ` { G } ) ) -> U e. LVec )
43 9 adantr 
 |-  ( ( ph /\ f e. ( N ` { G } ) ) -> G e. F )
44 35 36 4 5 6 32 42 43 28 lkrss2N 
 |-  ( ( ph /\ f e. ( N ` { G } ) ) -> ( ( L ` G ) C_ ( L ` f ) <-> E. k e. ( Base ` ( Scalar ` U ) ) f = ( k ( .s ` D ) G ) ) )
45 40 44 mpbird 
 |-  ( ( ph /\ f e. ( N ` { G } ) ) -> ( L ` G ) C_ ( L ` f ) )
46 1 3 15 2 dochss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( L ` f ) C_ ( Base ` U ) /\ ( L ` G ) C_ ( L ` f ) ) -> ( ._|_ ` ( L ` f ) ) C_ ( ._|_ ` ( L ` G ) ) )
47 14 29 45 46 syl3anc 
 |-  ( ( ph /\ f e. ( N ` { G } ) ) -> ( ._|_ ` ( L ` f ) ) C_ ( ._|_ ` ( L ` G ) ) )
48 47 sseld 
 |-  ( ( ph /\ f e. ( N ` { G } ) ) -> ( x e. ( ._|_ ` ( L ` f ) ) -> x e. ( ._|_ ` ( L ` G ) ) ) )
49 48 ex 
 |-  ( ph -> ( f e. ( N ` { G } ) -> ( x e. ( ._|_ ` ( L ` f ) ) -> x e. ( ._|_ ` ( L ` G ) ) ) ) )
50 13 49 syl5bi 
 |-  ( ph -> ( f e. R -> ( x e. ( ._|_ ` ( L ` f ) ) -> x e. ( ._|_ ` ( L ` G ) ) ) ) )
51 50 rexlimdv 
 |-  ( ph -> ( E. f e. R x e. ( ._|_ ` ( L ` f ) ) -> x e. ( ._|_ ` ( L ` G ) ) ) )
52 19 7 lspsnid 
 |-  ( ( D e. LMod /\ G e. ( Base ` D ) ) -> G e. ( N ` { G } ) )
53 18 20 52 syl2anc 
 |-  ( ph -> G e. ( N ` { G } ) )
54 53 11 eleqtrrdi 
 |-  ( ph -> G e. R )
55 2fveq3 
 |-  ( f = G -> ( ._|_ ` ( L ` f ) ) = ( ._|_ ` ( L ` G ) ) )
56 55 eleq2d 
 |-  ( f = G -> ( x e. ( ._|_ ` ( L ` f ) ) <-> x e. ( ._|_ ` ( L ` G ) ) ) )
57 56 rspcev 
 |-  ( ( G e. R /\ x e. ( ._|_ ` ( L ` G ) ) ) -> E. f e. R x e. ( ._|_ ` ( L ` f ) ) )
58 54 57 sylan 
 |-  ( ( ph /\ x e. ( ._|_ ` ( L ` G ) ) ) -> E. f e. R x e. ( ._|_ ` ( L ` f ) ) )
59 58 ex 
 |-  ( ph -> ( x e. ( ._|_ ` ( L ` G ) ) -> E. f e. R x e. ( ._|_ ` ( L ` f ) ) ) )
60 51 59 impbid 
 |-  ( ph -> ( E. f e. R x e. ( ._|_ ` ( L ` f ) ) <-> x e. ( ._|_ ` ( L ` G ) ) ) )
61 12 60 syl5bb 
 |-  ( ph -> ( x e. U_ f e. R ( ._|_ ` ( L ` f ) ) <-> x e. ( ._|_ ` ( L ` G ) ) ) )
62 61 eqrdv 
 |-  ( ph -> U_ f e. R ( ._|_ ` ( L ` f ) ) = ( ._|_ ` ( L ` G ) ) )
63 10 62 syl5eq 
 |-  ( ph -> Q = ( ._|_ ` ( L ` G ) ) )