---

Step * of Lemma relative-vs_wf

∀[K:CRng]. ∀[vs:VectorSpace(K)]. ∀[A,B:Point(vs) ⟶ ℙ].
  a.A[a]//b.B[b] ∈ VectorSpace(K) 
  supposing vs-subspace(K;vs;a.A[a]) ∧ vs-subspace(K;vs;b.B[b]) ∧ (∀v:Point(vs). (B[v] ⇒ A[v]))
BY
{ (ProveWfLemma
   THEN BLemma `implies-vs-subspace`
   THEN Auto
   THEN RepUR ``sub-vs mk-vs vs-0 vs-add vs-mul`` 0
   THEN Folds ``vs-0 vs-add vs-mul`` 0
   THEN Auto) }

1
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]

---

Latex:

---

Latex:
\mforall{}[K:CRng].  \mforall{}[vs:VectorSpace(K)].  \mforall{}[A,B:Point(vs)  {}\mrightarrow{}  \mBbbP{}].
    a.A[a]//b.B[b]  \mmember{}  VectorSpace(K) 
    supposing  vs-subspace(K;vs;a.A[a])  \mwedge{}  vs-subspace(K;vs;b.B[b])  \mwedge{}  (\mforall{}v:Point(vs).  (B[v]  {}\mRightarrow{}  A[v]))


By

---

Latex:
(ProveWfLemma
  THEN  BLemma  `implies-vs-subspace`
  THEN  Auto
  THEN  RepUR  ``sub-vs  mk-vs  vs-0  vs-add  vs-mul``  0
  THEN  Folds  ``vs-0  vs-add  vs-mul``  0
  THEN  Auto)

---

Home Index