---

Step * 1 1 1 1 1 4 1 of Lemma implies-isometry-lemma3


1. rv : InnerProductSpace
2. m : ℕ+
3. x : Point(rv)
4. y : Point(rv)
5. s : ℝ
6. r0 < s
7. ||x - y|| = s
8. u : {p:Point(rv)| xx + r(m)*y - x=xp ∧ yy + r(m)*x - y=yp} 
⊢ (||u - x|| = (r(m) * s)) ∧ (||u - y|| = (r(m) * s))
BY
{ (D -1 THEN (Unhide THENA Auto) THEN ParallelLast THEN Unfold `ip-congruent` -1) }

1
1. rv : InnerProductSpace
2. m : ℕ+
3. x : Point(rv)
4. y : Point(rv)
5. s : ℝ
6. r0 < s
7. ||x - y|| = s
8. u : Point(rv)
9. yy + r(m)*x - y=yu
10. ||x - x + r(m)*y - x|| = ||x - u||
⊢ ||u - x|| = (r(m) * s)

2
1. rv : InnerProductSpace
2. m : ℕ+
3. x : Point(rv)
4. y : Point(rv)
5. s : ℝ
6. r0 < s
7. ||x - y|| = s
8. u : Point(rv)
9. xx + r(m)*y - x=xu
10. ||y - y + r(m)*x - y|| = ||y - u||
⊢ ||u - y|| = (r(m) * s)

---

Latex:

---

Latex:

1.  rv  :  InnerProductSpace
2.  m  :  \mBbbN{}\msupplus{}
3.  x  :  Point(rv)
4.  y  :  Point(rv)
5.  s  :  \mBbbR{}
6.  r0  <  s
7.  ||x  -  y||  =  s
8.  u  :  \{p:Point(rv)|  xx  +  r(m)*y  -  x=xp  \mwedge{}  yy  +  r(m)*x  -  y=yp\} 
\mvdash{}  (||u  -  x||  =  (r(m)  *  s))  \mwedge{}  (||u  -  y||  =  (r(m)  *  s))


By

---

Latex:
(D  -1  THEN  (Unhide  THENA  Auto)  THEN  ParallelLast  THEN  Unfold  `ip-congruent`  -1)

---

Home Index