---

Step * 1 of Lemma vs-tree-val_wf_subspace


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]} 
BY
{ (MemTypeCD THEN Auto) }

1
.....set predicate..... 
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]
⊢ P[k * v + w]

---

Latex:

---

Latex:

1.  K  :  RngSig
2.  vs  :  VectorSpace(K)
3.  P  :  Point(vs)  {}\mrightarrow{}  \mBbbP{}
4.  vs-subspace(K;vs;x.P[x])
5.  t  :  l\_tree(v:Point(vs)  \mtimes{}  P[v];|K|)
6.  k  :  |K|
7.  l  :  l\_tree(v:Point(vs)  \mtimes{}  P[v];|K|)
8.  r  :  l\_tree(v:Point(vs)  \mtimes{}  P[v];|K|)
9.  \mforall{}v:Point(vs).  (P[v]  \mmember{}  Type)
10.  v  :  Point(vs)
11.  P[v]
12.  \mforall{}v:Point(vs).  (P[v]  \mmember{}  Type)
13.  w  :  Point(vs)
14.  P[w]
\mvdash{}  k  *  v  +  w  \mmember{}  \{v:Point(vs)|  P[v]\} 


By

---

Latex:
(MemTypeCD  THEN  Auto)

---

Home Index