---

Step * 1 4 of Lemma path-comp-prod


1. A : SeparationSpace
2. B : SeparationSpace
3. ∀f,g:{f:{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)}  ⟶ Point(A)| ∀t,t':{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} .  (t ≡ t' ⇒ f t ≡ f t')} .
     (f r1 ≡ g r0
     ⇒ (∃h:{f:{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)}  ⟶ Point(A)| ∀t,t':{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} .  (t ≡ t' ⇒ f t ≡ f t')} 
          path-comp-rel(A;f;g;h)))
4. ∀f,g:{f:{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)}  ⟶ Point(B)| ∀t,t':{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} .  (t ≡ t' ⇒ f t ≡ f t')} .
     (f r1 ≡ g r0
     ⇒ (∃h:{f:{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)}  ⟶ Point(B)| ∀t,t':{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} .  (t ≡ t' ⇒ f t ≡ f t')} 
          path-comp-rel(B;f;g;h)))
5. f : {x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)}  ⟶ (Point(A) × Point(B))@i
6. ∀t,t':{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} .  (t ≡ t' ⇒ f t ≡ f t')
7. g : {x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)}  ⟶ (Point(A) × Point(B))@i
8. ∀t,t':{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} .  (t ≡ t' ⇒ g t ≡ g t')
9. f r1 ≡ g r0
10. λt.(fst((f t))) ∈ {f:{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)}  ⟶ Point(A)| 
                       ∀t,t':{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} .  (t ≡ t' ⇒ f t ≡ f t')} 
11. λt.(fst((g t))) ∈ {f:{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)}  ⟶ Point(A)| 
                       ∀t,t':{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} .  (t ≡ t' ⇒ f t ≡ f t')} 
12. λt.(snd((f t))) ∈ {f:{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)}  ⟶ Point(B)| 
                       ∀t,t':{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} .  (t ≡ t' ⇒ f t ≡ f t')} 
13. t : {x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} @i
14. t' : {x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} @i
15. t ≡ t'
⊢ snd((g t)) ≡ snd((g t'))
BY
{ ((All (RWO "prod-ss-point<") THENA Auto) THEN (Assert g t ≡ g t' BY Auto) THEN RWO "prod-ss-eq" (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  SeparationSpace
2.  B  :  SeparationSpace
3.  \mforall{}f,g:\{f:\{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}    {}\mrightarrow{}  Point(A)| 
                  \mforall{}t,t':\{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}  .    (t  \mequiv{}  t'  {}\mRightarrow{}  f  t  \mequiv{}  f  t')\}  .
          (f  r1  \mequiv{}  g  r0
          {}\mRightarrow{}  (\mexists{}h:\{f:\{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}    {}\mrightarrow{}  Point(A)| 
                          \mforall{}t,t':\{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}  .    (t  \mequiv{}  t'  {}\mRightarrow{}  f  t  \mequiv{}  f  t')\} 
                    path-comp-rel(A;f;g;h)))
4.  \mforall{}f,g:\{f:\{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}    {}\mrightarrow{}  Point(B)| 
                  \mforall{}t,t':\{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}  .    (t  \mequiv{}  t'  {}\mRightarrow{}  f  t  \mequiv{}  f  t')\}  .
          (f  r1  \mequiv{}  g  r0
          {}\mRightarrow{}  (\mexists{}h:\{f:\{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}    {}\mrightarrow{}  Point(B)| 
                          \mforall{}t,t':\{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}  .    (t  \mequiv{}  t'  {}\mRightarrow{}  f  t  \mequiv{}  f  t')\} 
                    path-comp-rel(B;f;g;h)))
5.  f  :  \{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}    {}\mrightarrow{}  (Point(A)  \mtimes{}  Point(B))@i
6.  \mforall{}t,t':\{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}  .    (t  \mequiv{}  t'  {}\mRightarrow{}  f  t  \mequiv{}  f  t')
7.  g  :  \{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}    {}\mrightarrow{}  (Point(A)  \mtimes{}  Point(B))@i
8.  \mforall{}t,t':\{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}  .    (t  \mequiv{}  t'  {}\mRightarrow{}  g  t  \mequiv{}  g  t')
9.  f  r1  \mequiv{}  g  r0
10.  \mlambda{}t.(fst((f  t)))  \mmember{}  \{f:\{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}    {}\mrightarrow{}  Point(A)| 
                                              \mforall{}t,t':\{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}  .    (t  \mequiv{}  t'  {}\mRightarrow{}  f  t  \mequiv{}  f  t')\} 
11.  \mlambda{}t.(fst((g  t)))  \mmember{}  \{f:\{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}    {}\mrightarrow{}  Point(A)| 
                                              \mforall{}t,t':\{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}  .    (t  \mequiv{}  t'  {}\mRightarrow{}  f  t  \mequiv{}  f  t')\} 
12.  \mlambda{}t.(snd((f  t)))  \mmember{}  \{f:\{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}    {}\mrightarrow{}  Point(B)| 
                                              \mforall{}t,t':\{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}  .    (t  \mequiv{}  t'  {}\mRightarrow{}  f  t  \mequiv{}  f  t')\} 
13.  t  :  \{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}  @i
14.  t'  :  \{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}  @i
15.  t  \mequiv{}  t'
\mvdash{}  snd((g  t))  \mequiv{}  snd((g  t'))


By

---

Latex:
((All  (RWO  "prod-ss-point<")  THENA  Auto)
  THEN  (Assert  g  t  \mequiv{}  g  t'  BY
                          Auto)
  THEN  RWO  "prod-ss-eq"  (-1)
  THEN  Auto)

---

Home Index