Step
*
2
of Lemma
generated-subspace-is-subspace
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)))
BY
{ (OrRight THENA Auto) }
1
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|
⊢ ∃t:l_tree(x:Point(vs) × P[x];|K|). (k * w + y = vs-tree-val(vs;t) ∈ Point(vs))
Latex:
Latex:
1. K : Rng
2. vs : VectorSpace(K)
3. [P] : Point(vs) {}\mrightarrow{} \mBbbP{}
4. w : Point(vs)
5. y : Point(vs)
6. t : l\_tree(x:Point(vs) \mtimes{} P[x];|K|)
7. w = vs-tree-val(vs;t)
8. y = 0
9. k : |K|
\mvdash{} (k * w + y = 0) \mvee{} (\mexists{}t:l\_tree(x:Point(vs) \mtimes{} P[x];|K|). (k * w + y = vs-tree-val(vs;t)))
By
Latex:
(OrRight THENA Auto)
Home
Index