Step * 1 of Lemma vs-subtract-self

.....assertion..... 
1. Rng
2. vs VectorSpace(K)
3. Point(vs)
4. -K 0 ∈ Point(vs)
⊢ -K (x x) ∈ Point(vs)
BY
((Unfold `vs-subtract` THEN EqCDA) THEN Auto) }


Latex:


Latex:
.....assertion..... 
1.  K  :  Rng
2.  vs  :  VectorSpace(K)
3.  x  :  Point(vs)
4.  1  *  x  +  -K  1  *  x  =  0
\mvdash{}  1  *  x  +  -K  1  *  x  =  (x  -  x)


By


Latex:
((Unfold  `vs-subtract`  0  THEN  EqCDA)  THEN  Auto)




Home Index