---

Step * 1 1 1 1 1 1 1 1 of Lemma IdNotHomotopicConst-implies-BrowerFPT

.....aux..... 
1. n : ℕ
2. g : B(n + 1) ⟶ B(n + 1)
3. ∀x,y:B(n + 1).  (req-vec(n + 1;x;y) ⇒ req-vec(n + 1;g x;g y))
4. ∀x:B(n + 1). (||g x|| = r1)
5. ∀x:B(n + 1). ((||x|| = r1) ⇒ req-vec(n + 1;g x;x))
6. ∀h:{h:B(n + 1) ⟶ B(n + 1)| ∀p,q:B(n + 1).  (req-vec(n + 1;p;q) ⇒ req-vec(n + 1;h p;h q))} . (g o h ∈ sphere-map(n))
7. ∀t:{t:ℝ| t ∈ [r0, r1]} . ∀p:B(n + 1).  (t*p ∈ B(n + 1))
8. ∀t:{t:ℝ| t ∈ [r0, r1]} . (λp.t*p ∈ B(n + 1) ⟶ B(n + 1))
9. ∀t:{t:ℝ| t ∈ [r0, r1]} 
     (λp.t*p ∈ {h:B(n + 1) ⟶ B(n + 1)| ∀p,q:B(n + 1).  (req-vec(n + 1;p;q) ⇒ req-vec(n + 1;h p;h q))} )
10. ∀t:{t:ℝ| t ∈ [r0, r1]} . (g o (λp.t*p) ∈ sphere-map(n))
11. ∀t,s:{t:ℝ| t ∈ [r0, r1]} .  ((t = s) ⇒ sphere-map-eq(n;g o (λp.t*p);g o (λp.s*p)))
12. λi.r0 ∈ B(n + 1)
13. p : S(n)
⊢ ||r1*p|| = r1
BY
{ (D -1 THEN (Unhide THENA Auto) THEN RWW  "real-vec-norm-mul -1" 0 THEN Auto) }

1
1. n : ℕ
2. g : B(n + 1) ⟶ B(n + 1)
3. ∀x,y:B(n + 1).  (req-vec(n + 1;x;y) ⇒ req-vec(n + 1;g x;g y))
4. ∀x:B(n + 1). (||g x|| = r1)
5. ∀x:B(n + 1). ((||x|| = r1) ⇒ req-vec(n + 1;g x;x))
6. ∀h:{h:B(n + 1) ⟶ B(n + 1)| ∀p,q:B(n + 1).  (req-vec(n + 1;p;q) ⇒ req-vec(n + 1;h p;h q))} . (g o h ∈ sphere-map(n))
7. ∀t:{t:ℝ| t ∈ [r0, r1]} . ∀p:B(n + 1).  (t*p ∈ B(n + 1))
8. ∀t:{t:ℝ| t ∈ [r0, r1]} . (λp.t*p ∈ B(n + 1) ⟶ B(n + 1))
9. ∀t:{t:ℝ| t ∈ [r0, r1]} 
     (λp.t*p ∈ {h:B(n + 1) ⟶ B(n + 1)| ∀p,q:B(n + 1).  (req-vec(n + 1;p;q) ⇒ req-vec(n + 1;h p;h q))} )
10. ∀t:{t:ℝ| t ∈ [r0, r1]} . (g o (λp.t*p) ∈ sphere-map(n))
11. ∀t,s:{t:ℝ| t ∈ [r0, r1]} .  ((t = s) ⇒ sphere-map-eq(n;g o (λp.t*p);g o (λp.s*p)))
12. λi.r0 ∈ B(n + 1)
13. p : ℝ^n + 1
14. ||p|| = r1
⊢ (|r1| * r1) = r1

---

Latex:

---

Latex:
.....aux..... 
1.  n  :  \mBbbN{}
2.  g  :  B(n  +  1)  {}\mrightarrow{}  B(n  +  1)
3.  \mforall{}x,y:B(n  +  1).    (req-vec(n  +  1;x;y)  {}\mRightarrow{}  req-vec(n  +  1;g  x;g  y))
4.  \mforall{}x:B(n  +  1).  (||g  x||  =  r1)
5.  \mforall{}x:B(n  +  1).  ((||x||  =  r1)  {}\mRightarrow{}  req-vec(n  +  1;g  x;x))
6.  \mforall{}h:\{h:B(n  +  1)  {}\mrightarrow{}  B(n  +  1)|  \mforall{}p,q:B(n  +  1).    (req-vec(n  +  1;p;q)  {}\mRightarrow{}  req-vec(n  +  1;h  p;h  q))\} 
          (g  o  h  \mmember{}  sphere-map(n))
7.  \mforall{}t:\{t:\mBbbR{}|  t  \mmember{}  [r0,  r1]\}  .  \mforall{}p:B(n  +  1).    (t*p  \mmember{}  B(n  +  1))
8.  \mforall{}t:\{t:\mBbbR{}|  t  \mmember{}  [r0,  r1]\}  .  (\mlambda{}p.t*p  \mmember{}  B(n  +  1)  {}\mrightarrow{}  B(n  +  1))
9.  \mforall{}t:\{t:\mBbbR{}|  t  \mmember{}  [r0,  r1]\} 
          (\mlambda{}p.t*p  \mmember{}  \{h:B(n  +  1)  {}\mrightarrow{}  B(n  +  1)| 
                                \mforall{}p,q:B(n  +  1).    (req-vec(n  +  1;p;q)  {}\mRightarrow{}  req-vec(n  +  1;h  p;h  q))\}  )
10.  \mforall{}t:\{t:\mBbbR{}|  t  \mmember{}  [r0,  r1]\}  .  (g  o  (\mlambda{}p.t*p)  \mmember{}  sphere-map(n))
11.  \mforall{}t,s:\{t:\mBbbR{}|  t  \mmember{}  [r0,  r1]\}  .    ((t  =  s)  {}\mRightarrow{}  sphere-map-eq(n;g  o  (\mlambda{}p.t*p);g  o  (\mlambda{}p.s*p)))
12.  \mlambda{}i.r0  \mmember{}  B(n  +  1)
13.  p  :  S(n)
\mvdash{}  ||r1*p||  =  r1


By

---

Latex:
(D  -1  THEN  (Unhide  THENA  Auto)  THEN  RWW    "real-vec-norm-mul  -1"  0  THEN  Auto)

---

Home Index