---

Step * 1 1 of Lemma vs-lift-neg-bfs

.....subterm..... T:t
2:n
1. K : CRng
2. S : Type
3. fs : basic-formal-sum(K;S)
4. vs : VectorSpace(K)
5. f : S ⟶ Point(vs)
6. p1 : |K|
7. p2 : S
⊢ (-K p1) = ((-K 1) * p1) ∈ |K|
BY
{ (RW  RngNormC 0 THEN Auto) }

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  K  :  CRng
2.  S  :  Type
3.  fs  :  basic-formal-sum(K;S)
4.  vs  :  VectorSpace(K)
5.  f  :  S  {}\mrightarrow{}  Point(vs)
6.  p1  :  |K|
7.  p2  :  S
\mvdash{}  (-K  p1)  =  ((-K  1)  *  p1)


By

---

Latex:
(RW    RngNormC  0  THEN  Auto)

---

Home Index