---

Step * 1 of Lemma relative-vs_wf


1. K : CRng
2. vs : VectorSpace(K)
3. A : Point(vs) ⟶ ℙ
4. B : Point(vs) ⟶ ℙ
5. vs-subspace(K;vs;a.A[a])
6. vs-subspace(K;vs;b.B[b])
7. ∀v:Point(vs). (B[v] ⇒ A[v])
8. b : Point((a:vs | A[a]))
9. y : Point((a:vs | A[a]))
10. B[b]
11. B[y]
12. k : |K|
⊢ B[k * b + y]
BY
{ (D 6 THEN Auto) }

---

Latex:

---

Latex:

1.  K  :  CRng
2.  vs  :  VectorSpace(K)
3.  A  :  Point(vs)  {}\mrightarrow{}  \mBbbP{}
4.  B  :  Point(vs)  {}\mrightarrow{}  \mBbbP{}
5.  vs-subspace(K;vs;a.A[a])
6.  vs-subspace(K;vs;b.B[b])
7.  \mforall{}v:Point(vs).  (B[v]  {}\mRightarrow{}  A[v])
8.  b  :  Point((a:vs  |  A[a]))
9.  y  :  Point((a:vs  |  A[a]))
10.  B[b]
11.  B[y]
12.  k  :  |K|
\mvdash{}  B[k  *  b  +  y]


By

---

Latex:
(D  6  THEN  Auto)

---

Home Index