---

Step * of Lemma sub-vs_wf

∀[K:Rng]. ∀[vs:VectorSpace(K)]. ∀[P:Point(vs) ⟶ ℙ].  (v:vs | P[v]) ∈ VectorSpace(K) supposing vs-subspace(K;vs;x.P[x])
BY
{ (Unfold `vs-subspace` 0
   THEN ProveWfLemma
   THEN Try ((DSetVars THEN EqTypeCD THEN Auto THEN BackThruSomeHyp THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[K:Rng].  \mforall{}[vs:VectorSpace(K)].  \mforall{}[P:Point(vs)  {}\mrightarrow{}  \mBbbP{}].
    (v:vs  |  P[v])  \mmember{}  VectorSpace(K)  supposing  vs-subspace(K;vs;x.P[x])


By

---

Latex:
(Unfold  `vs-subspace`  0
  THEN  ProveWfLemma
  THEN  Try  ((DSetVars  THEN  EqTypeCD  THEN  Auto  THEN  BackThruSomeHyp  THEN  Auto)))

---

Home Index