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 ⊢φ→W∈LVec
ldual1dim.g ⊢φ→G∈F
Assertion ldual1dim ⊢φ→N⁡G=g∈F|L⁡G⊆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 ⊢φ→W∈LVec
6 ldual1dim.g ⊢φ→G∈F
7 eqid ⊢Scalar⁡W=Scalar⁡W
8 eqid ⊢BaseScalar⁡W=BaseScalar⁡W
9 eqid ⊢Scalar⁡D=Scalar⁡D
10 eqid ⊢BaseScalar⁡D=BaseScalar⁡D
11 7 8 3 9 10 5 ldualsbase ⊢φ→BaseScalar⁡D=BaseScalar⁡W
12 11 eleq2d ⊢φ→k∈BaseScalar⁡D↔k∈BaseScalar⁡W
13 12 anbi1d ⊢φ→k∈BaseScalar⁡D∧g=k⋅DG↔k∈BaseScalar⁡W∧g=k⋅DG
14 eqid ⊢BaseW=BaseW
15 eqid ⊢⋅Scalar⁡W=⋅Scalar⁡W
16 eqid ⊢⋅D=⋅D
17 5 adantr ⊢φ∧k∈BaseScalar⁡W→W∈LVec
18 simpr ⊢φ∧k∈BaseScalar⁡W→k∈BaseScalar⁡W
19 6 adantr ⊢φ∧k∈BaseScalar⁡W→G∈F
20 1 14 7 8 15 3 16 17 18 19 ldualvs ⊢φ∧k∈BaseScalar⁡W→k⋅DG=G⋅Scalar⁡WfBaseW×k
21 20 eqeq2d ⊢φ∧k∈BaseScalar⁡W→g=k⋅DG↔g=G⋅Scalar⁡WfBaseW×k
22 21 pm5.32da ⊢φ→k∈BaseScalar⁡W∧g=k⋅DG↔k∈BaseScalar⁡W∧g=G⋅Scalar⁡WfBaseW×k
23 13 22 bitrd ⊢φ→k∈BaseScalar⁡D∧g=k⋅DG↔k∈BaseScalar⁡W∧g=G⋅Scalar⁡WfBaseW×k
24 23 rexbidv2 ⊢φ→∃k∈BaseScalar⁡Dg=k⋅DG↔∃k∈BaseScalar⁡Wg=G⋅Scalar⁡WfBaseW×k
25 24 abbidv ⊢φ→g|∃k∈BaseScalar⁡Dg=k⋅DG=g|∃k∈BaseScalar⁡Wg=G⋅Scalar⁡WfBaseW×k
26 lveclmod ⊢W∈LVec→W∈LMod
27 3 26 lduallmod ⊢W∈LVec→D∈LMod
28 5 27 syl ⊢φ→D∈LMod
29 eqid ⊢BaseD=BaseD
30 1 3 29 5 6 ldualelvbase ⊢φ→G∈BaseD
31 9 10 29 16 4 lspsn ⊢D∈LMod∧G∈BaseD→N⁡G=g|∃k∈BaseScalar⁡Dg=k⋅DG
32 28 30 31 syl2anc ⊢φ→N⁡G=g|∃k∈BaseScalar⁡Dg=k⋅DG
33 14 7 1 2 8 15 5 6 lfl1dim ⊢φ→g∈F|L⁡G⊆L⁡g=g|∃k∈BaseScalar⁡Wg=G⋅Scalar⁡WfBaseW×k
34 25 32 33 3eqtr4d ⊢φ→N⁡G=g∈F|L⁡G⊆L⁡g