---

Step * 2 2 1 1 1 1 1 of Lemma implies-isometry-lemma2


1. rv : InnerProductSpace
2. x : Point
3. y : Point
4. J : ℝ
⊢ (||x + J - r1*y - x - x + J*y - x|| = ||x - y||)
∧ (||x + J*y - x - x + J - r(2)*y - x|| = (r(2) * ||x - y||))
∧ (||x + J - r1*y - x - x + J - r(2)*y - x|| = ||x - y||)
BY
{ Auto }

1
1. rv : InnerProductSpace
2. x : Point
3. y : Point
4. J : ℝ
⊢ ||x + J - r1*y - x - x + J*y - x|| = ||x - y||

2
1. rv : InnerProductSpace
2. x : Point
3. y : Point
4. J : ℝ
5. ||x + J - r1*y - x - x + J*y - x|| = ||x - y||
⊢ ||x + J*y - x - x + J - r(2)*y - x|| = (r(2) * ||x - y||)

3
1. rv : InnerProductSpace
2. x : Point
3. y : Point
4. J : ℝ
5. ||x + J - r1*y - x - x + J*y - x|| = ||x - y||
6. ||x + J*y - x - x + J - r(2)*y - x|| = (r(2) * ||x - y||)
⊢ ||x + J - r1*y - x - x + J - r(2)*y - x|| = ||x - y||

---

Latex:

---

Latex:

1.  rv  :  InnerProductSpace
2.  x  :  Point
3.  y  :  Point
4.  J  :  \mBbbR{}
\mvdash{}  (||x  +  J  -  r1*y  -  x  -  x  +  J*y  -  x||  =  ||x  -  y||)
\mwedge{}  (||x  +  J*y  -  x  -  x  +  J  -  r(2)*y  -  x||  =  (r(2)  *  ||x  -  y||))
\mwedge{}  (||x  +  J  -  r1*y  -  x  -  x  +  J  -  r(2)*y  -  x||  =  ||x  -  y||)


By

---

Latex:
Auto

---

Home Index