---

Step * of Lemma vs-tree-val_wf_subspace

∀[K:RngSig]. ∀[vs:VectorSpace(K)]. ∀[P:Point(vs) ⟶ ℙ].
  ∀[t:l_tree(v:Point(vs) × P[v];|K|)]. (vs-tree-val(vs;t) ∈ {v:Point(vs)| P[v]} ) supposing vs-subspace(K;vs;x.P[x])
BY
{ ProveWfLemma }

1
1. K : RngSig
2. vs : VectorSpace(K)
3. P : Point(vs) ⟶ ℙ
4. vs-subspace(K;vs;x.P[x])
5. t : l_tree(v:Point(vs) × P[v];|K|)
6. k : |K|
7. l : l_tree(v:Point(vs) × P[v];|K|)
8. r : l_tree(v:Point(vs) × P[v];|K|)
9. ∀v:Point(vs). (P[v] ∈ Type)
10. v : Point(vs)
11. P[v]
12. ∀v:Point(vs). (P[v] ∈ Type)
13. w : Point(vs)
14. P[w]
⊢ k * v + w ∈ {v:Point(vs)| P[v]} 

---

Latex:

---

Latex:
\mforall{}[K:RngSig].  \mforall{}[vs:VectorSpace(K)].  \mforall{}[P:Point(vs)  {}\mrightarrow{}  \mBbbP{}].
    \mforall{}[t:l\_tree(v:Point(vs)  \mtimes{}  P[v];|K|)].  (vs-tree-val(vs;t)  \mmember{}  \{v:Point(vs)|  P[v]\}  )  supposing  vs-subsp\000Cace(K;vs;x.P[x])


By

---

Latex:
ProveWfLemma

---

Home Index