---

Step * 1 1 1 1 1 1 2 of Lemma Degree-implies-BrowerFPT


1. n : ℕ
2. ind : sphere-map(n) ⟶ ℤ
3. ∀f,g:sphere-map(n).  (sphere-map-eq(n;f;g) ⇒ ((ind f) = (ind g) ∈ ℤ))
4. ∀p:S(n). ((ind const-sphere-map(p)) = 0 ∈ ℤ)
5. (ind id-sphere-map()) = 1 ∈ ℤ
6. g : B(n + 1) ⟶ B(n + 1)
7. ∀x,y:B(n + 1).  (req-vec(n + 1;x;y) ⇒ req-vec(n + 1;g x;g y))
8. ∀x:B(n + 1). (||g x|| = r1)
9. ∀x:B(n + 1). ((||x|| = r1) ⇒ req-vec(n + 1;g x;x))
10. ∀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)\000C)
11. ∀t:{t:ℝ| t ∈ [r0, r1]} . ∀p:B(n + 1).  (t*p ∈ B(n + 1))
12. ∀t:{t:ℝ| t ∈ [r0, r1]} . (λp.t*p ∈ B(n + 1) ⟶ B(n + 1))
13. ∀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))} )
14. ∀t:{t:ℝ| t ∈ [r0, r1]} . (g o (λp.t*p) ∈ sphere-map(n))
15. ∀t,s:{t:ℝ| t ∈ [r0, r1]} .  ((t = s) ⇒ sphere-map-eq(n;g o (λp.t*p);g o (λp.s*p)))
16. ∀t,s:{t:ℝ| t ∈ [r0, r1]} .  ((t = s) ⇒ ((ind (g o (λp.t*p))) = (ind (g o (λp.s*p))) ∈ ℤ))
17. ∀t,s:{t:ℝ| (r0 ≤ t) ∧ (t ≤ r1)} .  ((t = s) ⇒ ((ind (g o (λp.t*p))) = (ind (g o (λp.s*p))) ∈ ℤ))
18. (ind (g o (λp.r0*p))) = 0 ∈ ℤ
⊢ (ind (λx.(g r1*x))) = 1 ∈ ℤ
BY
{ ((Assert sphere-map-eq(n;λx.(g r1*x);id-sphere-map()) BY
          (D 0
           THEN RepUR ``id-sphere-map`` 0
           THEN Auto
           THEN (Assert req-vec(n + 1;g r1*p;g p) BY
                       (BackThruSomeHyp THEN D 0 THEN Auto THEN RepUR ``real-vec-mul`` 0 THEN Auto))
           THEN (RWO "-1" 0 THENA Auto)
           THEN BackThruSomeHyp
           THEN DVar `p'
           THEN Unhide
           THEN Auto))
   THEN FHyp 3 [-1]
   THEN Auto) }

1
.....wf..... 
1. n : ℕ
2. ind : sphere-map(n) ⟶ ℤ
3. ∀f,g:sphere-map(n).  (sphere-map-eq(n;f;g) ⇒ ((ind f) = (ind g) ∈ ℤ))
4. ∀p:S(n). ((ind const-sphere-map(p)) = 0 ∈ ℤ)
5. (ind id-sphere-map()) = 1 ∈ ℤ
6. g : B(n + 1) ⟶ B(n + 1)
7. ∀x,y:B(n + 1).  (req-vec(n + 1;x;y) ⇒ req-vec(n + 1;g x;g y))
8. ∀x:B(n + 1). (||g x|| = r1)
9. ∀x:B(n + 1). ((||x|| = r1) ⇒ req-vec(n + 1;g x;x))
10. ∀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)\000C)
11. ∀t:{t:ℝ| t ∈ [r0, r1]} . ∀p:B(n + 1).  (t*p ∈ B(n + 1))
12. ∀t:{t:ℝ| t ∈ [r0, r1]} . (λp.t*p ∈ B(n + 1) ⟶ B(n + 1))
13. ∀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))} )
14. ∀t:{t:ℝ| t ∈ [r0, r1]} . (g o (λp.t*p) ∈ sphere-map(n))
15. ∀t,s:{t:ℝ| t ∈ [r0, r1]} .  ((t = s) ⇒ sphere-map-eq(n;g o (λp.t*p);g o (λp.s*p)))
16. ∀t,s:{t:ℝ| t ∈ [r0, r1]} .  ((t = s) ⇒ ((ind (g o (λp.t*p))) = (ind (g o (λp.s*p))) ∈ ℤ))
17. ∀t,s:{t:ℝ| (r0 ≤ t) ∧ (t ≤ r1)} .  ((t = s) ⇒ ((ind (g o (λp.t*p))) = (ind (g o (λp.s*p))) ∈ ℤ))
18. (ind (g o (λp.r0*p))) = 0 ∈ ℤ
19. sphere-map-eq(n;λx.(g r1*x);id-sphere-map())
⊢ λx.(g r1*x) ∈ sphere-map(n)

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  ind  :  sphere-map(n)  {}\mrightarrow{}  \mBbbZ{}
3.  \mforall{}f,g:sphere-map(n).    (sphere-map-eq(n;f;g)  {}\mRightarrow{}  ((ind  f)  =  (ind  g)))
4.  \mforall{}p:S(n).  ((ind  const-sphere-map(p))  =  0)
5.  (ind  id-sphere-map())  =  1
6.  g  :  B(n  +  1)  {}\mrightarrow{}  B(n  +  1)
7.  \mforall{}x,y:B(n  +  1).    (req-vec(n  +  1;x;y)  {}\mRightarrow{}  req-vec(n  +  1;g  x;g  y))
8.  \mforall{}x:B(n  +  1).  (||g  x||  =  r1)
9.  \mforall{}x:B(n  +  1).  ((||x||  =  r1)  {}\mRightarrow{}  req-vec(n  +  1;g  x;x))
10.  \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))
11.  \mforall{}t:\{t:\mBbbR{}|  t  \mmember{}  [r0,  r1]\}  .  \mforall{}p:B(n  +  1).    (t*p  \mmember{}  B(n  +  1))
12.  \mforall{}t:\{t:\mBbbR{}|  t  \mmember{}  [r0,  r1]\}  .  (\mlambda{}p.t*p  \mmember{}  B(n  +  1)  {}\mrightarrow{}  B(n  +  1))
13.  \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))\}  )
14.  \mforall{}t:\{t:\mBbbR{}|  t  \mmember{}  [r0,  r1]\}  .  (g  o  (\mlambda{}p.t*p)  \mmember{}  sphere-map(n))
15.  \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)))
16.  \mforall{}t,s:\{t:\mBbbR{}|  t  \mmember{}  [r0,  r1]\}  .    ((t  =  s)  {}\mRightarrow{}  ((ind  (g  o  (\mlambda{}p.t*p)))  =  (ind  (g  o  (\mlambda{}p.s*p)))))
17.  \mforall{}t,s:\{t:\mBbbR{}|  (r0  \mleq{}  t)  \mwedge{}  (t  \mleq{}  r1)\}  .    ((t  =  s)  {}\mRightarrow{}  ((ind  (g  o  (\mlambda{}p.t*p)))  =  (ind  (g  o  (\mlambda{}p.s*p)))))
18.  (ind  (g  o  (\mlambda{}p.r0*p)))  =  0
\mvdash{}  (ind  (\mlambda{}x.(g  r1*x)))  =  1


By

---

Latex:
((Assert  sphere-map-eq(n;\mlambda{}x.(g  r1*x);id-sphere-map())  BY
                (D  0
                  THEN  RepUR  ``id-sphere-map``  0
                  THEN  Auto
                  THEN  (Assert  req-vec(n  +  1;g  r1*p;g  p)  BY
                                          (BackThruSomeHyp  THEN  D  0  THEN  Auto  THEN  RepUR  ``real-vec-mul``  0  THEN  Auto))
                  THEN  (RWO  "-1"  0  THENA  Auto)
                  THEN  BackThruSomeHyp
                  THEN  DVar  `p'
                  THEN  Unhide
                  THEN  Auto))
  THEN  FHyp  3  [-1]
  THEN  Auto)

---

Home Index