---

Step * of Lemma generated-subspace-is-subspace

∀K:Rng. ∀vs:VectorSpace(K).  ∀[P:Point(vs) ⟶ ℙ]. vs-subspace(K;vs;w.Subspace(x.P[x]) w)
BY
{ (Auto
   THEN (BLemma `implies-vs-subspace` THEN Auto)
   THEN All (RepUR ``generated-subspace``)
   THEN Auto
   THEN SplitOrHyps
   THEN ExRepD) }

1
1. K : Rng
2. vs : VectorSpace(K)
3. [P] : Point(vs) ⟶ ℙ
4. w : Point(vs)
5. y : Point(vs)
6. w = 0 ∈ Point(vs)
7. y = 0 ∈ Point(vs)
8. k : |K|
⊢ (k * w + y = 0 ∈ Point(vs)) ∨ (∃t:l_tree(x:Point(vs) × P[x];|K|). (k * w + y = vs-tree-val(vs;t) ∈ Point(vs)))

2
1. K : Rng
2. vs : VectorSpace(K)
3. [P] : Point(vs) ⟶ ℙ
4. w : Point(vs)
5. y : Point(vs)
6. t : l_tree(x:Point(vs) × P[x];|K|)
7. w = vs-tree-val(vs;t) ∈ Point(vs)
8. y = 0 ∈ Point(vs)
9. k : |K|
⊢ (k * w + y = 0 ∈ Point(vs)) ∨ (∃t:l_tree(x:Point(vs) × P[x];|K|). (k * w + y = vs-tree-val(vs;t) ∈ Point(vs)))

3
1. K : Rng
2. vs : VectorSpace(K)
3. [P] : Point(vs) ⟶ ℙ
4. w : Point(vs)
5. y : Point(vs)
6. w = 0 ∈ Point(vs)
7. t : l_tree(x:Point(vs) × P[x];|K|)
8. y = vs-tree-val(vs;t) ∈ Point(vs)
9. k : |K|
⊢ (k * w + y = 0 ∈ Point(vs)) ∨ (∃t:l_tree(x:Point(vs) × P[x];|K|). (k * w + y = vs-tree-val(vs;t) ∈ Point(vs)))

4
1. K : Rng
2. vs : VectorSpace(K)
3. [P] : Point(vs) ⟶ ℙ
4. w : Point(vs)
5. y : Point(vs)
6. t1 : l_tree(x:Point(vs) × P[x];|K|)
7. w = vs-tree-val(vs;t1) ∈ Point(vs)
8. t : l_tree(x:Point(vs) × P[x];|K|)
9. y = vs-tree-val(vs;t) ∈ Point(vs)
10. k : |K|
⊢ (k * w + y = 0 ∈ Point(vs)) ∨ (∃t:l_tree(x:Point(vs) × P[x];|K|). (k * w + y = vs-tree-val(vs;t) ∈ Point(vs)))

---

Latex:

---

Latex:
\mforall{}K:Rng.  \mforall{}vs:VectorSpace(K).    \mforall{}[P:Point(vs)  {}\mrightarrow{}  \mBbbP{}].  vs-subspace(K;vs;w.Subspace(x.P[x])  w)


By

---

Latex:
(Auto
  THEN  (BLemma  `implies-vs-subspace`  THEN  Auto)
  THEN  All  (RepUR  ``generated-subspace``)
  THEN  Auto
  THEN  SplitOrHyps
  THEN  ExRepD)

---

Home Index