Metamath Proof Explorer


Theorem lfl1dim2N

Description: Equivalent expressions for a 1-dim subspace (ray) of functionals. TODO: delete this if not useful; lfl1dim may be more compatible with lspsn . (Contributed by NM, 24-Oct-2014) (New usage is discouraged.)

Ref Expression
Hypotheses lfl1dim.v
|- V = ( Base ` W )
lfl1dim.d
|- D = ( Scalar ` W )
lfl1dim.f
|- F = ( LFnl ` W )
lfl1dim.l
|- L = ( LKer ` W )
lfl1dim.k
|- K = ( Base ` D )
lfl1dim.t
|- .x. = ( .r ` D )
lfl1dim.w
|- ( ph -> W e. LVec )
lfl1dim.g
|- ( ph -> G e. F )
Assertion lfl1dim2N
|- ( ph -> { g e. F | ( L ` G ) C_ ( L ` g ) } = { g e. F | E. k e. K g = ( G oF .x. ( V X. { k } ) ) } )

Proof

Step Hyp Ref Expression
1 lfl1dim.v
 |-  V = ( Base ` W )
2 lfl1dim.d
 |-  D = ( Scalar ` W )
3 lfl1dim.f
 |-  F = ( LFnl ` W )
4 lfl1dim.l
 |-  L = ( LKer ` W )
5 lfl1dim.k
 |-  K = ( Base ` D )
6 lfl1dim.t
 |-  .x. = ( .r ` D )
7 lfl1dim.w
 |-  ( ph -> W e. LVec )
8 lfl1dim.g
 |-  ( ph -> G e. F )
9 lveclmod
 |-  ( W e. LVec -> W e. LMod )
10 7 9 syl
 |-  ( ph -> W e. LMod )
11 eqid
 |-  ( 0g ` D ) = ( 0g ` D )
12 2 5 11 lmod0cl
 |-  ( W e. LMod -> ( 0g ` D ) e. K )
13 10 12 syl
 |-  ( ph -> ( 0g ` D ) e. K )
14 13 ad2antrr
 |-  ( ( ( ph /\ g e. F ) /\ g = ( V X. { ( 0g ` D ) } ) ) -> ( 0g ` D ) e. K )
15 simpr
 |-  ( ( ( ph /\ g e. F ) /\ g = ( V X. { ( 0g ` D ) } ) ) -> g = ( V X. { ( 0g ` D ) } ) )
16 10 ad2antrr
 |-  ( ( ( ph /\ g e. F ) /\ g = ( V X. { ( 0g ` D ) } ) ) -> W e. LMod )
17 8 ad2antrr
 |-  ( ( ( ph /\ g e. F ) /\ g = ( V X. { ( 0g ` D ) } ) ) -> G e. F )
18 1 2 3 5 6 11 16 17 lfl0sc
 |-  ( ( ( ph /\ g e. F ) /\ g = ( V X. { ( 0g ` D ) } ) ) -> ( G oF .x. ( V X. { ( 0g ` D ) } ) ) = ( V X. { ( 0g ` D ) } ) )
19 15 18 eqtr4d
 |-  ( ( ( ph /\ g e. F ) /\ g = ( V X. { ( 0g ` D ) } ) ) -> g = ( G oF .x. ( V X. { ( 0g ` D ) } ) ) )
20 sneq
 |-  ( k = ( 0g ` D ) -> { k } = { ( 0g ` D ) } )
21 20 xpeq2d
 |-  ( k = ( 0g ` D ) -> ( V X. { k } ) = ( V X. { ( 0g ` D ) } ) )
22 21 oveq2d
 |-  ( k = ( 0g ` D ) -> ( G oF .x. ( V X. { k } ) ) = ( G oF .x. ( V X. { ( 0g ` D ) } ) ) )
23 22 rspceeqv
 |-  ( ( ( 0g ` D ) e. K /\ g = ( G oF .x. ( V X. { ( 0g ` D ) } ) ) ) -> E. k e. K g = ( G oF .x. ( V X. { k } ) ) )
24 14 19 23 syl2anc
 |-  ( ( ( ph /\ g e. F ) /\ g = ( V X. { ( 0g ` D ) } ) ) -> E. k e. K g = ( G oF .x. ( V X. { k } ) ) )
25 24 a1d
 |-  ( ( ( ph /\ g e. F ) /\ g = ( V X. { ( 0g ` D ) } ) ) -> ( ( L ` G ) C_ ( L ` g ) -> E. k e. K g = ( G oF .x. ( V X. { k } ) ) ) )
26 13 ad3antrrr
 |-  ( ( ( ( ph /\ g e. F ) /\ G = ( V X. { ( 0g ` D ) } ) ) /\ ( L ` G ) C_ ( L ` g ) ) -> ( 0g ` D ) e. K )
27 10 ad3antrrr
 |-  ( ( ( ( ph /\ g e. F ) /\ G = ( V X. { ( 0g ` D ) } ) ) /\ ( L ` G ) C_ ( L ` g ) ) -> W e. LMod )
28 simpllr
 |-  ( ( ( ( ph /\ g e. F ) /\ G = ( V X. { ( 0g ` D ) } ) ) /\ ( L ` G ) C_ ( L ` g ) ) -> g e. F )
29 1 3 4 27 28 lkrssv
 |-  ( ( ( ( ph /\ g e. F ) /\ G = ( V X. { ( 0g ` D ) } ) ) /\ ( L ` G ) C_ ( L ` g ) ) -> ( L ` g ) C_ V )
30 10 adantr
 |-  ( ( ph /\ g e. F ) -> W e. LMod )
31 8 adantr
 |-  ( ( ph /\ g e. F ) -> G e. F )
32 2 11 1 3 4 lkr0f
 |-  ( ( W e. LMod /\ G e. F ) -> ( ( L ` G ) = V <-> G = ( V X. { ( 0g ` D ) } ) ) )
33 30 31 32 syl2anc
 |-  ( ( ph /\ g e. F ) -> ( ( L ` G ) = V <-> G = ( V X. { ( 0g ` D ) } ) ) )
34 33 biimpar
 |-  ( ( ( ph /\ g e. F ) /\ G = ( V X. { ( 0g ` D ) } ) ) -> ( L ` G ) = V )
35 34 sseq1d
 |-  ( ( ( ph /\ g e. F ) /\ G = ( V X. { ( 0g ` D ) } ) ) -> ( ( L ` G ) C_ ( L ` g ) <-> V C_ ( L ` g ) ) )
36 35 biimpa
 |-  ( ( ( ( ph /\ g e. F ) /\ G = ( V X. { ( 0g ` D ) } ) ) /\ ( L ` G ) C_ ( L ` g ) ) -> V C_ ( L ` g ) )
37 29 36 eqssd
 |-  ( ( ( ( ph /\ g e. F ) /\ G = ( V X. { ( 0g ` D ) } ) ) /\ ( L ` G ) C_ ( L ` g ) ) -> ( L ` g ) = V )
38 2 11 1 3 4 lkr0f
 |-  ( ( W e. LMod /\ g e. F ) -> ( ( L ` g ) = V <-> g = ( V X. { ( 0g ` D ) } ) ) )
39 27 28 38 syl2anc
 |-  ( ( ( ( ph /\ g e. F ) /\ G = ( V X. { ( 0g ` D ) } ) ) /\ ( L ` G ) C_ ( L ` g ) ) -> ( ( L ` g ) = V <-> g = ( V X. { ( 0g ` D ) } ) ) )
40 37 39 mpbid
 |-  ( ( ( ( ph /\ g e. F ) /\ G = ( V X. { ( 0g ` D ) } ) ) /\ ( L ` G ) C_ ( L ` g ) ) -> g = ( V X. { ( 0g ` D ) } ) )
41 8 ad3antrrr
 |-  ( ( ( ( ph /\ g e. F ) /\ G = ( V X. { ( 0g ` D ) } ) ) /\ ( L ` G ) C_ ( L ` g ) ) -> G e. F )
42 1 2 3 5 6 11 27 41 lfl0sc
 |-  ( ( ( ( ph /\ g e. F ) /\ G = ( V X. { ( 0g ` D ) } ) ) /\ ( L ` G ) C_ ( L ` g ) ) -> ( G oF .x. ( V X. { ( 0g ` D ) } ) ) = ( V X. { ( 0g ` D ) } ) )
43 40 42 eqtr4d
 |-  ( ( ( ( ph /\ g e. F ) /\ G = ( V X. { ( 0g ` D ) } ) ) /\ ( L ` G ) C_ ( L ` g ) ) -> g = ( G oF .x. ( V X. { ( 0g ` D ) } ) ) )
44 26 43 23 syl2anc
 |-  ( ( ( ( ph /\ g e. F ) /\ G = ( V X. { ( 0g ` D ) } ) ) /\ ( L ` G ) C_ ( L ` g ) ) -> E. k e. K g = ( G oF .x. ( V X. { k } ) ) )
45 44 ex
 |-  ( ( ( ph /\ g e. F ) /\ G = ( V X. { ( 0g ` D ) } ) ) -> ( ( L ` G ) C_ ( L ` g ) -> E. k e. K g = ( G oF .x. ( V X. { k } ) ) ) )
46 eqid
 |-  ( LSHyp ` W ) = ( LSHyp ` W )
47 7 ad2antrr
 |-  ( ( ( ph /\ g e. F ) /\ ( g =/= ( V X. { ( 0g ` D ) } ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) ) -> W e. LVec )
48 8 ad2antrr
 |-  ( ( ( ph /\ g e. F ) /\ ( g =/= ( V X. { ( 0g ` D ) } ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) ) -> G e. F )
49 simprr
 |-  ( ( ( ph /\ g e. F ) /\ ( g =/= ( V X. { ( 0g ` D ) } ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) ) -> G =/= ( V X. { ( 0g ` D ) } ) )
50 1 2 11 46 3 4 lkrshp
 |-  ( ( W e. LVec /\ G e. F /\ G =/= ( V X. { ( 0g ` D ) } ) ) -> ( L ` G ) e. ( LSHyp ` W ) )
51 47 48 49 50 syl3anc
 |-  ( ( ( ph /\ g e. F ) /\ ( g =/= ( V X. { ( 0g ` D ) } ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) ) -> ( L ` G ) e. ( LSHyp ` W ) )
52 simplr
 |-  ( ( ( ph /\ g e. F ) /\ ( g =/= ( V X. { ( 0g ` D ) } ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) ) -> g e. F )
53 simprl
 |-  ( ( ( ph /\ g e. F ) /\ ( g =/= ( V X. { ( 0g ` D ) } ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) ) -> g =/= ( V X. { ( 0g ` D ) } ) )
54 1 2 11 46 3 4 lkrshp
 |-  ( ( W e. LVec /\ g e. F /\ g =/= ( V X. { ( 0g ` D ) } ) ) -> ( L ` g ) e. ( LSHyp ` W ) )
55 47 52 53 54 syl3anc
 |-  ( ( ( ph /\ g e. F ) /\ ( g =/= ( V X. { ( 0g ` D ) } ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) ) -> ( L ` g ) e. ( LSHyp ` W ) )
56 46 47 51 55 lshpcmp
 |-  ( ( ( ph /\ g e. F ) /\ ( g =/= ( V X. { ( 0g ` D ) } ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) ) -> ( ( L ` G ) C_ ( L ` g ) <-> ( L ` G ) = ( L ` g ) ) )
57 7 ad3antrrr
 |-  ( ( ( ( ph /\ g e. F ) /\ ( g =/= ( V X. { ( 0g ` D ) } ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) ) /\ ( L ` G ) = ( L ` g ) ) -> W e. LVec )
58 8 ad3antrrr
 |-  ( ( ( ( ph /\ g e. F ) /\ ( g =/= ( V X. { ( 0g ` D ) } ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) ) /\ ( L ` G ) = ( L ` g ) ) -> G e. F )
59 simpllr
 |-  ( ( ( ( ph /\ g e. F ) /\ ( g =/= ( V X. { ( 0g ` D ) } ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) ) /\ ( L ` G ) = ( L ` g ) ) -> g e. F )
60 simpr
 |-  ( ( ( ( ph /\ g e. F ) /\ ( g =/= ( V X. { ( 0g ` D ) } ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) ) /\ ( L ` G ) = ( L ` g ) ) -> ( L ` G ) = ( L ` g ) )
61 2 5 6 1 3 4 eqlkr2
 |-  ( ( W e. LVec /\ ( G e. F /\ g e. F ) /\ ( L ` G ) = ( L ` g ) ) -> E. k e. K g = ( G oF .x. ( V X. { k } ) ) )
62 57 58 59 60 61 syl121anc
 |-  ( ( ( ( ph /\ g e. F ) /\ ( g =/= ( V X. { ( 0g ` D ) } ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) ) /\ ( L ` G ) = ( L ` g ) ) -> E. k e. K g = ( G oF .x. ( V X. { k } ) ) )
63 62 ex
 |-  ( ( ( ph /\ g e. F ) /\ ( g =/= ( V X. { ( 0g ` D ) } ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) ) -> ( ( L ` G ) = ( L ` g ) -> E. k e. K g = ( G oF .x. ( V X. { k } ) ) ) )
64 56 63 sylbid
 |-  ( ( ( ph /\ g e. F ) /\ ( g =/= ( V X. { ( 0g ` D ) } ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) ) -> ( ( L ` G ) C_ ( L ` g ) -> E. k e. K g = ( G oF .x. ( V X. { k } ) ) ) )
65 25 45 64 pm2.61da2ne
 |-  ( ( ph /\ g e. F ) -> ( ( L ` G ) C_ ( L ` g ) -> E. k e. K g = ( G oF .x. ( V X. { k } ) ) ) )
66 7 ad2antrr
 |-  ( ( ( ph /\ g e. F ) /\ k e. K ) -> W e. LVec )
67 8 ad2antrr
 |-  ( ( ( ph /\ g e. F ) /\ k e. K ) -> G e. F )
68 simpr
 |-  ( ( ( ph /\ g e. F ) /\ k e. K ) -> k e. K )
69 1 2 5 6 3 4 66 67 68 lkrscss
 |-  ( ( ( ph /\ g e. F ) /\ k e. K ) -> ( L ` G ) C_ ( L ` ( G oF .x. ( V X. { k } ) ) ) )
70 69 ex
 |-  ( ( ph /\ g e. F ) -> ( k e. K -> ( L ` G ) C_ ( L ` ( G oF .x. ( V X. { k } ) ) ) ) )
71 fveq2
 |-  ( g = ( G oF .x. ( V X. { k } ) ) -> ( L ` g ) = ( L ` ( G oF .x. ( V X. { k } ) ) ) )
72 71 sseq2d
 |-  ( g = ( G oF .x. ( V X. { k } ) ) -> ( ( L ` G ) C_ ( L ` g ) <-> ( L ` G ) C_ ( L ` ( G oF .x. ( V X. { k } ) ) ) ) )
73 72 biimprcd
 |-  ( ( L ` G ) C_ ( L ` ( G oF .x. ( V X. { k } ) ) ) -> ( g = ( G oF .x. ( V X. { k } ) ) -> ( L ` G ) C_ ( L ` g ) ) )
74 70 73 syl6
 |-  ( ( ph /\ g e. F ) -> ( k e. K -> ( g = ( G oF .x. ( V X. { k } ) ) -> ( L ` G ) C_ ( L ` g ) ) ) )
75 74 rexlimdv
 |-  ( ( ph /\ g e. F ) -> ( E. k e. K g = ( G oF .x. ( V X. { k } ) ) -> ( L ` G ) C_ ( L ` g ) ) )
76 65 75 impbid
 |-  ( ( ph /\ g e. F ) -> ( ( L ` G ) C_ ( L ` g ) <-> E. k e. K g = ( G oF .x. ( V X. { k } ) ) ) )
77 76 rabbidva
 |-  ( ph -> { g e. F | ( L ` G ) C_ ( L ` g ) } = { g e. F | E. k e. K g = ( G oF .x. ( V X. { k } ) ) } )