Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dochflcl Structured version   Visualization version   GIF version

Theorem dochflcl 35782
 Description: Closure of the explicit functional 𝐺 determined by a nonzero vector 𝑋. Compare the more general lshpkrcl 33421. (Contributed by NM, 27-Oct-2014.)
Hypotheses
Ref Expression
dochflcl.h 𝐻 = (LHyp‘𝐾)
dochflcl.o = ((ocH‘𝐾)‘𝑊)
dochflcl.u 𝑈 = ((DVecH‘𝐾)‘𝑊)
dochflcl.v 𝑉 = (Base‘𝑈)
dochflcl.z 0 = (0g𝑈)
dochflcl.a + = (+g𝑈)
dochflcl.t · = ( ·𝑠𝑈)
dochflcl.f 𝐹 = (LFnl‘𝑈)
dochflcl.d 𝐷 = (Scalar‘𝑈)
dochflcl.r 𝑅 = (Base‘𝐷)
dochflcl.g 𝐺 = (𝑣𝑉 ↦ (𝑘𝑅𝑤 ∈ ( ‘{𝑋})𝑣 = (𝑤 + (𝑘 · 𝑋))))
dochflcl.k (𝜑 → (𝐾 ∈ HL ∧ 𝑊𝐻))
dochflcl.x (𝜑𝑋 ∈ (𝑉 ∖ { 0 }))
Assertion
Ref Expression
dochflcl (𝜑𝐺𝐹)
Distinct variable groups:   𝑣,𝑘,𝑤, +   𝐷,𝑘   ,𝑘,𝑣,𝑤   𝑅,𝑘,𝑣   · ,𝑘,𝑣,𝑤   𝑣,𝑉   𝑘,𝑋,𝑣,𝑤
Allowed substitution hints:   𝜑(𝑤,𝑣,𝑘)   𝐷(𝑤,𝑣)   𝑅(𝑤)   𝑈(𝑤,𝑣,𝑘)   𝐹(𝑤,𝑣,𝑘)   𝐺(𝑤,𝑣,𝑘)   𝐻(𝑤,𝑣,𝑘)   𝐾(𝑤,𝑣,𝑘)   𝑉(𝑤,𝑘)   𝑊(𝑤,𝑣,𝑘)   0 (𝑤,𝑣,𝑘)

Proof of Theorem dochflcl
StepHypRef Expression
1 dochflcl.v . 2 𝑉 = (Base‘𝑈)
2 dochflcl.a . 2 + = (+g𝑈)
3 eqid 2610 . 2 (LSpan‘𝑈) = (LSpan‘𝑈)
4 eqid 2610 . 2 (LSSum‘𝑈) = (LSSum‘𝑈)
5 eqid 2610 . 2 (LSHyp‘𝑈) = (LSHyp‘𝑈)
6 dochflcl.h . . 3 𝐻 = (LHyp‘𝐾)
7 dochflcl.u . . 3 𝑈 = ((DVecH‘𝐾)‘𝑊)
8 dochflcl.k . . 3 (𝜑 → (𝐾 ∈ HL ∧ 𝑊𝐻))
96, 7, 8dvhlvec 35416 . 2 (𝜑𝑈 ∈ LVec)
10 dochflcl.o . . 3 = ((ocH‘𝐾)‘𝑊)
11 dochflcl.z . . 3 0 = (0g𝑈)
12 dochflcl.x . . 3 (𝜑𝑋 ∈ (𝑉 ∖ { 0 }))
136, 10, 7, 1, 11, 5, 8, 12dochsnshp 35760 . 2 (𝜑 → ( ‘{𝑋}) ∈ (LSHyp‘𝑈))