Metamath Proof Explorer

Theorem ldual1dim

Description: Equivalent expressions for a 1-dim subspace (ray) of functionals. (Contributed by NM, 24-Oct-2014)

Ref Expression
Hypotheses ldual1dim.f 
|- F = ( LFnl ` W )
ldual1dim.l 
|- L = ( LKer ` W )
ldual1dim.d 
|- D = ( LDual ` W )
ldual1dim.n 
|- N = ( LSpan ` D )
ldual1dim.w 
|- ( ph -> W e. LVec )
ldual1dim.g 
|- ( ph -> G e. F )
Assertion ldual1dim 
|- ( ph -> ( N ` { G } ) = { g e. F | ( L ` G ) C_ ( L ` g ) } )

Proof

Step Hyp Ref Expression
1 ldual1dim.f 
 |-  F = ( LFnl ` W )
2 ldual1dim.l 
 |-  L = ( LKer ` W )
3 ldual1dim.d 
 |-  D = ( LDual ` W )
4 ldual1dim.n 
 |-  N = ( LSpan ` D )
5 ldual1dim.w 
 |-  ( ph -> W e. LVec )
6 ldual1dim.g 
 |-  ( ph -> G e. F )
7 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
8 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
9 eqid 
 |-  ( Scalar ` D ) = ( Scalar ` D )
10 eqid 
 |-  ( Base ` ( Scalar ` D ) ) = ( Base ` ( Scalar ` D ) )
11 7 8 3 9 10 5 ldualsbase 
 |-  ( ph -> ( Base ` ( Scalar ` D ) ) = ( Base ` ( Scalar ` W ) ) )
12 11 eleq2d 
 |-  ( ph -> ( k e. ( Base ` ( Scalar ` D ) ) <-> k e. ( Base ` ( Scalar ` W ) ) ) )
13 12 anbi1d 
 |-  ( ph -> ( ( k e. ( Base ` ( Scalar ` D ) ) /\ g = ( k ( .s ` D ) G ) ) <-> ( k e. ( Base ` ( Scalar ` W ) ) /\ g = ( k ( .s ` D ) G ) ) ) )
14 eqid 
 |-  ( Base ` W ) = ( Base ` W )
15 eqid 
 |-  ( .r ` ( Scalar ` W ) ) = ( .r ` ( Scalar ` W ) )
16 eqid 
 |-  ( .s ` D ) = ( .s ` D )
17 5 adantr 
 |-  ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) ) -> W e. LVec )
18 simpr 
 |-  ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) ) -> k e. ( Base ` ( Scalar ` W ) ) )
19 6 adantr 
 |-  ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) ) -> G e. F )
20 1 14 7 8 15 3 16 17 18 19 ldualvs 
 |-  ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) ) -> ( k ( .s ` D ) G ) = ( G oF ( .r ` ( Scalar ` W ) ) ( ( Base ` W ) X. { k } ) ) )
21 20 eqeq2d 
 |-  ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) ) -> ( g = ( k ( .s ` D ) G ) <-> g = ( G oF ( .r ` ( Scalar ` W ) ) ( ( Base ` W ) X. { k } ) ) ) )
22 21 pm5.32da 
 |-  ( ph -> ( ( k e. ( Base ` ( Scalar ` W ) ) /\ g = ( k ( .s ` D ) G ) ) <-> ( k e. ( Base ` ( Scalar ` W ) ) /\ g = ( G oF ( .r ` ( Scalar ` W ) ) ( ( Base ` W ) X. { k } ) ) ) ) )
23 13 22 bitrd 
 |-  ( ph -> ( ( k e. ( Base ` ( Scalar ` D ) ) /\ g = ( k ( .s ` D ) G ) ) <-> ( k e. ( Base ` ( Scalar ` W ) ) /\ g = ( G oF ( .r ` ( Scalar ` W ) ) ( ( Base ` W ) X. { k } ) ) ) ) )
24 23 rexbidv2 
 |-  ( ph -> ( E. k e. ( Base ` ( Scalar ` D ) ) g = ( k ( .s ` D ) G ) <-> E. k e. ( Base ` ( Scalar ` W ) ) g = ( G oF ( .r ` ( Scalar ` W ) ) ( ( Base ` W ) X. { k } ) ) ) )
25 24 abbidv 
 |-  ( ph -> { g | E. k e. ( Base ` ( Scalar ` D ) ) g = ( k ( .s ` D ) G ) } = { g | E. k e. ( Base ` ( Scalar ` W ) ) g = ( G oF ( .r ` ( Scalar ` W ) ) ( ( Base ` W ) X. { k } ) ) } )
26 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
27 3 26 lduallmod 
 |-  ( W e. LVec -> D e. LMod )
28 5 27 syl 
 |-  ( ph -> D e. LMod )
29 eqid 
 |-  ( Base ` D ) = ( Base ` D )
30 1 3 29 5 6 ldualelvbase 
 |-  ( ph -> G e. ( Base ` D ) )
31 9 10 29 16 4 lspsn 
 |-  ( ( D e. LMod /\ G e. ( Base ` D ) ) -> ( N ` { G } ) = { g | E. k e. ( Base ` ( Scalar ` D ) ) g = ( k ( .s ` D ) G ) } )
32 28 30 31 syl2anc 
 |-  ( ph -> ( N ` { G } ) = { g | E. k e. ( Base ` ( Scalar ` D ) ) g = ( k ( .s ` D ) G ) } )
33 14 7 1 2 8 15 5 6 lfl1dim 
 |-  ( ph -> { g e. F | ( L ` G ) C_ ( L ` g ) } = { g | E. k e. ( Base ` ( Scalar ` W ) ) g = ( G oF ( .r ` ( Scalar ` W ) ) ( ( Base ` W ) X. { k } ) ) } )
34 25 32 33 3eqtr4d 
 |-  ( ph -> ( N ` { G } ) = { g e. F | ( L ` G ) C_ ( L ` g ) } )