Metamath Proof Explorer

Theorem lfl1dim

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

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 lfl1dim 
|- ( ph -> { g e. F | ( L ` G ) C_ ( L ` g ) } = { g | 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 df-rab 
 |-  { g e. F | ( L ` G ) C_ ( L ` g ) } = { g | ( g e. F /\ ( L ` G ) C_ ( L ` g ) ) }
10 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
11 7 10 syl 
 |-  ( ph -> W e. LMod )
12 eqid 
 |-  ( 0g ` D ) = ( 0g ` D )
13 2 5 12 lmod0cl 
 |-  ( W e. LMod -> ( 0g ` D ) e. K )
14 11 13 syl 
 |-  ( ph -> ( 0g ` D ) e. K )
15 14 ad2antrr 
 |-  ( ( ( ph /\ g e. F ) /\ g = ( V X. { ( 0g ` D ) } ) ) -> ( 0g ` D ) e. K )
16 simpr 
 |-  ( ( ( ph /\ g e. F ) /\ g = ( V X. { ( 0g ` D ) } ) ) -> g = ( V X. { ( 0g ` D ) } ) )
17 11 ad2antrr 
 |-  ( ( ( ph /\ g e. F ) /\ g = ( V X. { ( 0g ` D ) } ) ) -> W e. LMod )
18 8 ad2antrr 
 |-  ( ( ( ph /\ g e. F ) /\ g = ( V X. { ( 0g ` D ) } ) ) -> G e. F )
19 1 2 3 5 6 12 17 18 lfl0sc 
 |-  ( ( ( ph /\ g e. F ) /\ g = ( V X. { ( 0g ` D ) } ) ) -> ( G oF .x. ( V X. { ( 0g ` D ) } ) ) = ( V X. { ( 0g ` D ) } ) )
20 16 19 eqtr4d 
 |-  ( ( ( ph /\ g e. F ) /\ g = ( V X. { ( 0g ` D ) } ) ) -> g = ( G oF .x. ( V X. { ( 0g ` D ) } ) ) )
21 sneq 
 |-  ( k = ( 0g ` D ) -> { k } = { ( 0g ` D ) } )
22 21 xpeq2d 
 |-  ( k = ( 0g ` D ) -> ( V X. { k } ) = ( V X. { ( 0g ` D ) } ) )
23 22 oveq2d 
 |-  ( k = ( 0g ` D ) -> ( G oF .x. ( V X. { k } ) ) = ( G oF .x. ( V X. { ( 0g ` D ) } ) ) )
24 23 rspceeqv 
 |-  ( ( ( 0g ` D ) e. K /\ g = ( G oF .x. ( V X. { ( 0g ` D ) } ) ) ) -> E. k e. K g = ( G oF .x. ( V X. { k } ) ) )
25 15 20 24 syl2anc 
 |-  ( ( ( ph /\ g e. F ) /\ g = ( V X. { ( 0g ` D ) } ) ) -> E. k e. K g = ( G oF .x. ( V X. { k } ) ) )
26 25 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 } ) ) ) )
27 14 ad3antrrr 
 |-  ( ( ( ( ph /\ g e. F ) /\ G = ( V X. { ( 0g ` D ) } ) ) /\ ( L ` G ) C_ ( L ` g ) ) -> ( 0g ` D ) e. K )
28 11 ad3antrrr 
 |-  ( ( ( ( ph /\ g e. F ) /\ G = ( V X. { ( 0g ` D ) } ) ) /\ ( L ` G ) C_ ( L ` g ) ) -> W e. LMod )
29 simpllr 
 |-  ( ( ( ( ph /\ g e. F ) /\ G = ( V X. { ( 0g ` D ) } ) ) /\ ( L ` G ) C_ ( L ` g ) ) -> g e. F )
30 1 3 4 28 29 lkrssv 
 |-  ( ( ( ( ph /\ g e. F ) /\ G = ( V X. { ( 0g ` D ) } ) ) /\ ( L ` G ) C_ ( L ` g ) ) -> ( L ` g ) C_ V )
31 11 adantr 
 |-  ( ( ph /\ g e. F ) -> W e. LMod )
32 8 adantr 
 |-  ( ( ph /\ g e. F ) -> G e. F )
33 2 12 1 3 4 lkr0f 
 |-  ( ( W e. LMod /\ G e. F ) -> ( ( L ` G ) = V <-> G = ( V X. { ( 0g ` D ) } ) ) )
34 31 32 33 syl2anc 
 |-  ( ( ph /\ g e. F ) -> ( ( L ` G ) = V <-> G = ( V X. { ( 0g ` D ) } ) ) )
35 34 biimpar 
 |-  ( ( ( ph /\ g e. F ) /\ G = ( V X. { ( 0g ` D ) } ) ) -> ( L ` G ) = V )
36 35 sseq1d 
 |-  ( ( ( ph /\ g e. F ) /\ G = ( V X. { ( 0g ` D ) } ) ) -> ( ( L ` G ) C_ ( L ` g ) <-> V C_ ( L ` g ) ) )
37 36 biimpa 
 |-  ( ( ( ( ph /\ g e. F ) /\ G = ( V X. { ( 0g ` D ) } ) ) /\ ( L ` G ) C_ ( L ` g ) ) -> V C_ ( L ` g ) )
38 30 37 eqssd 
 |-  ( ( ( ( ph /\ g e. F ) /\ G = ( V X. { ( 0g ` D ) } ) ) /\ ( L ` G ) C_ ( L ` g ) ) -> ( L ` g ) = V )
39 2 12 1 3 4 lkr0f 
 |-  ( ( W e. LMod /\ g e. F ) -> ( ( L ` g ) = V <-> g = ( V X. { ( 0g ` D ) } ) ) )
40 28 29 39 syl2anc 
 |-  ( ( ( ( ph /\ g e. F ) /\ G = ( V X. { ( 0g ` D ) } ) ) /\ ( L ` G ) C_ ( L ` g ) ) -> ( ( L ` g ) = V <-> g = ( V X. { ( 0g ` D ) } ) ) )
41 38 40 mpbid 
 |-  ( ( ( ( ph /\ g e. F ) /\ G = ( V X. { ( 0g ` D ) } ) ) /\ ( L ` G ) C_ ( L ` g ) ) -> g = ( V X. { ( 0g ` D ) } ) )
42 8 ad3antrrr 
 |-  ( ( ( ( ph /\ g e. F ) /\ G = ( V X. { ( 0g ` D ) } ) ) /\ ( L ` G ) C_ ( L ` g ) ) -> G e. F )
43 1 2 3 5 6 12 28 42 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 ) } ) )
44 41 43 eqtr4d 
 |-  ( ( ( ( ph /\ g e. F ) /\ G = ( V X. { ( 0g ` D ) } ) ) /\ ( L ` G ) C_ ( L ` g ) ) -> g = ( G oF .x. ( V X. { ( 0g ` D ) } ) ) )
45 27 44 24 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 } ) ) )
46 45 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 } ) ) ) )
47 eqid 
 |-  ( LSHyp ` W ) = ( LSHyp ` W )
48 7 ad2antrr 
 |-  ( ( ( ph /\ g e. F ) /\ ( g =/= ( V X. { ( 0g ` D ) } ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) ) -> W e. LVec )
49 8 ad2antrr 
 |-  ( ( ( ph /\ g e. F ) /\ ( g =/= ( V X. { ( 0g ` D ) } ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) ) -> G e. F )
50 simprr 
 |-  ( ( ( ph /\ g e. F ) /\ ( g =/= ( V X. { ( 0g ` D ) } ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) ) -> G =/= ( V X. { ( 0g ` D ) } ) )
51 1 2 12 47 3 4 lkrshp 
 |-  ( ( W e. LVec /\ G e. F /\ G =/= ( V X. { ( 0g ` D ) } ) ) -> ( L ` G ) e. ( LSHyp ` W ) )
52 48 49 50 51 syl3anc 
 |-  ( ( ( ph /\ g e. F ) /\ ( g =/= ( V X. { ( 0g ` D ) } ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) ) -> ( L ` G ) e. ( LSHyp ` W ) )
53 simplr 
 |-  ( ( ( ph /\ g e. F ) /\ ( g =/= ( V X. { ( 0g ` D ) } ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) ) -> g e. F )
54 simprl 
 |-  ( ( ( ph /\ g e. F ) /\ ( g =/= ( V X. { ( 0g ` D ) } ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) ) -> g =/= ( V X. { ( 0g ` D ) } ) )
55 1 2 12 47 3 4 lkrshp 
 |-  ( ( W e. LVec /\ g e. F /\ g =/= ( V X. { ( 0g ` D ) } ) ) -> ( L ` g ) e. ( LSHyp ` W ) )
56 48 53 54 55 syl3anc 
 |-  ( ( ( ph /\ g e. F ) /\ ( g =/= ( V X. { ( 0g ` D ) } ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) ) -> ( L ` g ) e. ( LSHyp ` W ) )
57 47 48 52 56 lshpcmp 
 |-  ( ( ( ph /\ g e. F ) /\ ( g =/= ( V X. { ( 0g ` D ) } ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) ) -> ( ( L ` G ) C_ ( L ` g ) <-> ( L ` G ) = ( L ` g ) ) )
58 7 ad3antrrr 
 |-  ( ( ( ( ph /\ g e. F ) /\ ( g =/= ( V X. { ( 0g ` D ) } ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) ) /\ ( L ` G ) = ( L ` g ) ) -> W e. LVec )
59 8 ad3antrrr 
 |-  ( ( ( ( ph /\ g e. F ) /\ ( g =/= ( V X. { ( 0g ` D ) } ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) ) /\ ( L ` G ) = ( L ` g ) ) -> G e. F )
60 simpllr 
 |-  ( ( ( ( ph /\ g e. F ) /\ ( g =/= ( V X. { ( 0g ` D ) } ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) ) /\ ( L ` G ) = ( L ` g ) ) -> g e. F )
61 simpr 
 |-  ( ( ( ( ph /\ g e. F ) /\ ( g =/= ( V X. { ( 0g ` D ) } ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) ) /\ ( L ` G ) = ( L ` g ) ) -> ( L ` G ) = ( L ` g ) )
62 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 } ) ) )
63 58 59 60 61 62 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 } ) ) )
64 63 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 } ) ) ) )
65 57 64 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 } ) ) ) )
66 26 46 65 pm2.61da2ne 
 |-  ( ( ph /\ g e. F ) -> ( ( L ` G ) C_ ( L ` g ) -> E. k e. K g = ( G oF .x. ( V X. { k } ) ) ) )
67 7 ad2antrr 
 |-  ( ( ( ph /\ g e. F ) /\ k e. K ) -> W e. LVec )
68 8 ad2antrr 
 |-  ( ( ( ph /\ g e. F ) /\ k e. K ) -> G e. F )
69 simpr 
 |-  ( ( ( ph /\ g e. F ) /\ k e. K ) -> k e. K )
70 1 2 5 6 3 4 67 68 69 lkrscss 
 |-  ( ( ( ph /\ g e. F ) /\ k e. K ) -> ( L ` G ) C_ ( L ` ( G oF .x. ( V X. { k } ) ) ) )
71 70 ex 
 |-  ( ( ph /\ g e. F ) -> ( k e. K -> ( L ` G ) C_ ( L ` ( G oF .x. ( V X. { k } ) ) ) ) )
72 fveq2 
 |-  ( g = ( G oF .x. ( V X. { k } ) ) -> ( L ` g ) = ( L ` ( G oF .x. ( V X. { k } ) ) ) )
73 72 sseq2d 
 |-  ( g = ( G oF .x. ( V X. { k } ) ) -> ( ( L ` G ) C_ ( L ` g ) <-> ( L ` G ) C_ ( L ` ( G oF .x. ( V X. { k } ) ) ) ) )
74 73 biimprcd 
 |-  ( ( L ` G ) C_ ( L ` ( G oF .x. ( V X. { k } ) ) ) -> ( g = ( G oF .x. ( V X. { k } ) ) -> ( L ` G ) C_ ( L ` g ) ) )
75 71 74 syl6 
 |-  ( ( ph /\ g e. F ) -> ( k e. K -> ( g = ( G oF .x. ( V X. { k } ) ) -> ( L ` G ) C_ ( L ` g ) ) ) )
76 75 rexlimdv 
 |-  ( ( ph /\ g e. F ) -> ( E. k e. K g = ( G oF .x. ( V X. { k } ) ) -> ( L ` G ) C_ ( L ` g ) ) )
77 66 76 impbid 
 |-  ( ( ph /\ g e. F ) -> ( ( L ` G ) C_ ( L ` g ) <-> E. k e. K g = ( G oF .x. ( V X. { k } ) ) ) )
78 77 pm5.32da 
 |-  ( ph -> ( ( g e. F /\ ( L ` G ) C_ ( L ` g ) ) <-> ( g e. F /\ E. k e. K g = ( G oF .x. ( V X. { k } ) ) ) ) )
79 11 adantr 
 |-  ( ( ph /\ k e. K ) -> W e. LMod )
80 8 adantr 
 |-  ( ( ph /\ k e. K ) -> G e. F )
81 simpr 
 |-  ( ( ph /\ k e. K ) -> k e. K )
82 1 2 5 6 3 79 80 81 lflvscl 
 |-  ( ( ph /\ k e. K ) -> ( G oF .x. ( V X. { k } ) ) e. F )
83 eleq1a 
 |-  ( ( G oF .x. ( V X. { k } ) ) e. F -> ( g = ( G oF .x. ( V X. { k } ) ) -> g e. F ) )
84 82 83 syl 
 |-  ( ( ph /\ k e. K ) -> ( g = ( G oF .x. ( V X. { k } ) ) -> g e. F ) )
85 84 pm4.71rd 
 |-  ( ( ph /\ k e. K ) -> ( g = ( G oF .x. ( V X. { k } ) ) <-> ( g e. F /\ g = ( G oF .x. ( V X. { k } ) ) ) ) )
86 85 rexbidva 
 |-  ( ph -> ( E. k e. K g = ( G oF .x. ( V X. { k } ) ) <-> E. k e. K ( g e. F /\ g = ( G oF .x. ( V X. { k } ) ) ) ) )
87 r19.42v 
 |-  ( E. k e. K ( g e. F /\ g = ( G oF .x. ( V X. { k } ) ) ) <-> ( g e. F /\ E. k e. K g = ( G oF .x. ( V X. { k } ) ) ) )
88 86 87 bitr2di 
 |-  ( ph -> ( ( g e. F /\ E. k e. K g = ( G oF .x. ( V X. { k } ) ) ) <-> E. k e. K g = ( G oF .x. ( V X. { k } ) ) ) )
89 78 88 bitrd 
 |-  ( ph -> ( ( g e. F /\ ( L ` G ) C_ ( L ` g ) ) <-> E. k e. K g = ( G oF .x. ( V X. { k } ) ) ) )
90 89 abbidv 
 |-  ( ph -> { g | ( g e. F /\ ( L ` G ) C_ ( L ` g ) ) } = { g | E. k e. K g = ( G oF .x. ( V X. { k } ) ) } )
91 9 90 syl5eq 
 |-  ( ph -> { g e. F | ( L ` G ) C_ ( L ` g ) } = { g | E. k e. K g = ( G oF .x. ( V X. { k } ) ) } )