Step * 1 of Lemma rv-sub-sep


1. rv RealVectorSpace
2. Point
3. x' Point
4. Point
5. y' Point
6. -y x' -y'
7. -y -y'
⊢ y'
BY
(Unfold `rv-minus` -1 THEN (FLemma `rv-mul-sep` [-1] THENA Auto) THEN -1 THEN Auto) }

1
1. rv RealVectorSpace
2. Point
3. x' Point
4. Point
5. y' Point
6. -y x' -y'
7. r(-1)*y r(-1)*y'
8. r(-1) ≠ r(-1)
⊢ y'


Latex:


Latex:

1.  rv  :  RealVectorSpace
2.  x  :  Point
3.  x'  :  Point
4.  y  :  Point
5.  y'  :  Point
6.  x  +  -y  \#  x'  +  -y'
7.  -y  \#  -y'
\mvdash{}  y  \#  y'


By


Latex:
(Unfold  `rv-minus`  -1  THEN  (FLemma  `rv-mul-sep`  [-1]  THENA  Auto)  THEN  D  -1  THEN  Auto)




Home Index