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