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=BaseW
lfl1dim.d D=ScalarW
lfl1dim.f F=LFnlW
lfl1dim.l L=LKerW
lfl1dim.k K=BaseD
lfl1dim.t ·˙=D
lfl1dim.w φWLVec
lfl1dim.g φGF
Assertion lfl1dim φgF|LGLg=g|kKg=G·˙fV×k

Proof

Step Hyp Ref Expression
1 lfl1dim.v V=BaseW
2 lfl1dim.d D=ScalarW
3 lfl1dim.f F=LFnlW
4 lfl1dim.l L=LKerW
5 lfl1dim.k K=BaseD
6 lfl1dim.t ·˙=D
7 lfl1dim.w φWLVec
8 lfl1dim.g φGF
9 df-rab gF|LGLg=g|gFLGLg
10 lveclmod WLVecWLMod
11 7 10 syl φWLMod
12 eqid 0D=0D
13 2 5 12 lmod0cl WLMod0DK
14 11 13 syl φ0DK
15 14 ad2antrr φgFg=V×0D0DK
16 simpr φgFg=V×0Dg=V×0D
17 11 ad2antrr φgFg=V×0DWLMod
18 8 ad2antrr φgFg=V×0DGF
19 1 2 3 5 6 12 17 18 lfl0sc φgFg=V×0DG·˙fV×0D=V×0D
20 16 19 eqtr4d φgFg=V×0Dg=G·˙fV×0D
21 sneq k=0Dk=0D
22 21 xpeq2d k=0DV×k=V×0D
23 22 oveq2d k=0DG·˙fV×k=G·˙fV×0D
24 23 rspceeqv 0DKg=G·˙fV×0DkKg=G·˙fV×k
25 15 20 24 syl2anc φgFg=V×0DkKg=G·˙fV×k
26 25 a1d φgFg=V×0DLGLgkKg=G·˙fV×k
27 14 ad3antrrr φgFG=V×0DLGLg0DK
28 11 ad3antrrr φgFG=V×0DLGLgWLMod
29 simpllr φgFG=V×0DLGLggF
30 1 3 4 28 29 lkrssv φgFG=V×0DLGLgLgV
31 11 adantr φgFWLMod
32 8 adantr φgFGF
33 2 12 1 3 4 lkr0f WLModGFLG=VG=V×0D
34 31 32 33 syl2anc φgFLG=VG=V×0D
35 34 biimpar φgFG=V×0DLG=V
36 35 sseq1d φgFG=V×0DLGLgVLg
37 36 biimpa φgFG=V×0DLGLgVLg
38 30 37 eqssd φgFG=V×0DLGLgLg=V
39 2 12 1 3 4 lkr0f WLModgFLg=Vg=V×0D
40 28 29 39 syl2anc φgFG=V×0DLGLgLg=Vg=V×0D
41 38 40 mpbid φgFG=V×0DLGLgg=V×0D
42 8 ad3antrrr φgFG=V×0DLGLgGF
43 1 2 3 5 6 12 28 42 lfl0sc φgFG=V×0DLGLgG·˙fV×0D=V×0D
44 41 43 eqtr4d φgFG=V×0DLGLgg=G·˙fV×0D
45 27 44 24 syl2anc φgFG=V×0DLGLgkKg=G·˙fV×k
46 45 ex φgFG=V×0DLGLgkKg=G·˙fV×k
47 eqid LSHypW=LSHypW
48 7 ad2antrr φgFgV×0DGV×0DWLVec
49 8 ad2antrr φgFgV×0DGV×0DGF
50 simprr φgFgV×0DGV×0DGV×0D
51 1 2 12 47 3 4 lkrshp WLVecGFGV×0DLGLSHypW
52 48 49 50 51 syl3anc φgFgV×0DGV×0DLGLSHypW
53 simplr φgFgV×0DGV×0DgF
54 simprl φgFgV×0DGV×0DgV×0D
55 1 2 12 47 3 4 lkrshp WLVecgFgV×0DLgLSHypW
56 48 53 54 55 syl3anc φgFgV×0DGV×0DLgLSHypW
57 47 48 52 56 lshpcmp φgFgV×0DGV×0DLGLgLG=Lg
58 7 ad3antrrr φgFgV×0DGV×0DLG=LgWLVec
59 8 ad3antrrr φgFgV×0DGV×0DLG=LgGF
60 simpllr φgFgV×0DGV×0DLG=LggF
61 simpr φgFgV×0DGV×0DLG=LgLG=Lg
62 2 5 6 1 3 4 eqlkr2 WLVecGFgFLG=LgkKg=G·˙fV×k
63 58 59 60 61 62 syl121anc φgFgV×0DGV×0DLG=LgkKg=G·˙fV×k
64 63 ex φgFgV×0DGV×0DLG=LgkKg=G·˙fV×k
65 57 64 sylbid φgFgV×0DGV×0DLGLgkKg=G·˙fV×k
66 26 46 65 pm2.61da2ne φgFLGLgkKg=G·˙fV×k
67 7 ad2antrr φgFkKWLVec
68 8 ad2antrr φgFkKGF
69 simpr φgFkKkK
70 1 2 5 6 3 4 67 68 69 lkrscss φgFkKLGLG·˙fV×k
71 70 ex φgFkKLGLG·˙fV×k
72 fveq2 g=G·˙fV×kLg=LG·˙fV×k
73 72 sseq2d g=G·˙fV×kLGLgLGLG·˙fV×k
74 73 biimprcd LGLG·˙fV×kg=G·˙fV×kLGLg
75 71 74 syl6 φgFkKg=G·˙fV×kLGLg
76 75 rexlimdv φgFkKg=G·˙fV×kLGLg
77 66 76 impbid φgFLGLgkKg=G·˙fV×k
78 77 pm5.32da φgFLGLggFkKg=G·˙fV×k
79 11 adantr φkKWLMod
80 8 adantr φkKGF
81 simpr φkKkK
82 1 2 5 6 3 79 80 81 lflvscl φkKG·˙fV×kF
83 eleq1a G·˙fV×kFg=G·˙fV×kgF
84 82 83 syl φkKg=G·˙fV×kgF
85 84 pm4.71rd φkKg=G·˙fV×kgFg=G·˙fV×k
86 85 rexbidva φkKg=G·˙fV×kkKgFg=G·˙fV×k
87 r19.42v kKgFg=G·˙fV×kgFkKg=G·˙fV×k
88 86 87 bitr2di φgFkKg=G·˙fV×kkKg=G·˙fV×k
89 78 88 bitrd φgFLGLgkKg=G·˙fV×k
90 89 abbidv φg|gFLGLg=g|kKg=G·˙fV×k
91 9 90 eqtrid φgF|LGLg=g|kKg=G·˙fV×k