This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dochflcl

Description: Closure of the explicit functional G determined by a nonzero vector X . Compare the more general lshpkrcl . (Contributed by NM, 27-Oct-2014)

Ref Expression
Hypotheses dochflcl.h ⊢ H = LHyp ⁡ K
dochflcl.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
dochflcl.u ⊢ U = DVecH ⁡ K ⁡ W
dochflcl.v ⊢ V = Base U
dochflcl.z ⊢ 0 ˙ = 0 U
dochflcl.a ⊢ + ˙ = + U
dochflcl.t ⊢ · ˙ = ⋅ U
dochflcl.f ⊢ F = LFnl ⁡ U
dochflcl.d ⊢ D = Scalar ⁡ U
dochflcl.r ⊢ R = Base D
dochflcl.g ⊢ G = v ∈ V ⟼ ι k ∈ R | ∃ w ∈ ⊥ ˙ ⁡ X v = w + ˙ k · ˙ X
dochflcl.k ⊢ φ → K ∈ HL ∧ W ∈ H
dochflcl.x ⊢ φ → X ∈ V ∖ 0 ˙
Assertion dochflcl ⊢ φ → G ∈ F

Proof

Step Hyp Ref Expression
1 dochflcl.h ⊢ H = LHyp ⁡ K
2 dochflcl.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
3 dochflcl.u ⊢ U = DVecH ⁡ K ⁡ W
4 dochflcl.v ⊢ V = Base U
5 dochflcl.z ⊢ 0 ˙ = 0 U
6 dochflcl.a ⊢ + ˙ = + U
7 dochflcl.t ⊢ · ˙ = ⋅ U
8 dochflcl.f ⊢ F = LFnl ⁡ U
9 dochflcl.d ⊢ D = Scalar ⁡ U
10 dochflcl.r ⊢ R = Base D
11 dochflcl.g ⊢ G = v ∈ V ⟼ ι k ∈ R | ∃ w ∈ ⊥ ˙ ⁡ X v = w + ˙ k · ˙ X
12 dochflcl.k ⊢ φ → K ∈ HL ∧ W ∈ H
13 dochflcl.x ⊢ φ → X ∈ V ∖ 0 ˙
14 eqid ⊢ LSpan ⁡ U = LSpan ⁡ U
15 eqid ⊢ LSSum ⁡ U = LSSum ⁡ U
16 eqid ⊢ LSHyp ⁡ U = LSHyp ⁡ U
17 1 3 12 dvhlvec ⊢ φ → U ∈ LVec
18 1 2 3 4 5 16 12 13 dochsnshp ⊢ φ → ⊥ ˙ ⁡ X ∈ LSHyp ⁡ U
19 13 eldifad ⊢ φ → X ∈ V
20 1 2 3 4 5 14 15 12 13 dochexmidat ⊢ φ → ⊥ ˙ ⁡ X LSSum ⁡ U LSpan ⁡ U ⁡ X = V
21 4 6 14 15 16 17 18 19 20 9 10 7 11 8 lshpkrcl ⊢ φ → G ∈ F