---

Step * of Lemma free-vs-subspace

∀[S:Type]. ∀[K:CRng]. ∀[P:formal-sum(K;S) ⟶ ℙ].
  ((P[{}]
  ∧ (∀fs,y:formal-sum(K;S).  (P[fs] ⇒ P[y] ⇒ P[fs + y]))
  ∧ (∀fs:formal-sum(K;S). ∀a:|K|.  (P[fs] ⇒ P[a * fs])))
  ⇒ vs-subspace(K;free-vs(K;S);fs.P[fs]))
BY
{ (Auto THEN RepUR ``vs-subspace vs-point free-vs mk-vs vs-add vs-mul vs-0`` 0 THEN Auto) }

1
1. S : Type
2. K : CRng
3. P : formal-sum(K;S) ⟶ ℙ
⊢ {} ∈ formal-sum(K;S)

---

Latex:

---

Latex:
\mforall{}[S:Type].  \mforall{}[K:CRng].  \mforall{}[P:formal-sum(K;S)  {}\mrightarrow{}  \mBbbP{}].
    ((P[\{\}]
    \mwedge{}  (\mforall{}fs,y:formal-sum(K;S).    (P[fs]  {}\mRightarrow{}  P[y]  {}\mRightarrow{}  P[fs  +  y]))
    \mwedge{}  (\mforall{}fs:formal-sum(K;S).  \mforall{}a:|K|.    (P[fs]  {}\mRightarrow{}  P[a  *  fs])))
    {}\mRightarrow{}  vs-subspace(K;free-vs(K;S);fs.P[fs]))


By

---

Latex:
(Auto  THEN  RepUR  ``vs-subspace  vs-point  free-vs  mk-vs  vs-add  vs-mul  vs-0``  0  THEN  Auto)

---

Home Index