---

Step * 1 5 1 1 1 1 2 1 of Lemma path-comp-prod


1. [A] : SeparationSpace
2. [B] : SeparationSpace
3. ∀f,g:Point(Path(A)).
     (f@r1 ≡ g@r0
     ⇒ (∃h:Point(Path(A))
          ((∀t:{x:ℝ| (r0 ≤ x) ∧ (x ≤ (r1/r(2)))} . h@t ≡ f@r(2) * t)
          ∧ (∀t:{x:ℝ| ((r1/r(2)) ≤ x) ∧ (x ≤ r1)} . h@t ≡ g@(r(2) * t) - r1))))
4. ∀f,g:Point(Path(B)).
     (f@r1 ≡ g@r0
     ⇒ (∃h:Point(Path(B))
          ((∀t:{x:ℝ| (r0 ≤ x) ∧ (x ≤ (r1/r(2)))} . h@t ≡ f@r(2) * t)
          ∧ (∀t:{x:ℝ| ((r1/r(2)) ≤ x) ∧ (x ≤ r1)} . h@t ≡ g@(r(2) * t) - r1))))
5. f : Point(Path(A × B))@i
6. g : Point(Path(A × B))@i
7. f@r1 ≡ g@r0
8. λt.(fst(f@t)) ∈ Point(Path(A))
9. λt.(fst(g@t)) ∈ Point(Path(A))
10. λt.(snd(f@t)) ∈ Point(Path(B))
11. λt.(snd(g@t)) ∈ Point(Path(B))
12. ∀f,t:Top.  (snd(f@t) ~ λt.(snd(f@t))@t)
13. ∀f,t:Top.  (fst(f@t) ~ λt.(fst(f@t))@t)
14. λt.(fst(f@t))@r1 ≡ λt.(fst(g@t))@r0
15. λt.(snd(f@t))@r1 ≡ λt.(snd(g@t))@r0
16. ha : Point(Path(A))
17. ∀t:{x:ℝ| (r0 ≤ x) ∧ (x ≤ (r1/r(2)))} . ha@t ≡ λt.(fst(f@t))@r(2) * t
18. ∀t:{x:ℝ| ((r1/r(2)) ≤ x) ∧ (x ≤ r1)} . ha@t ≡ λt.(fst(g@t))@(r(2) * t) - r1
19. hb : Point(Path(B))
20. ∀t:{x:ℝ| (r0 ≤ x) ∧ (x ≤ (r1/r(2)))} . hb@t ≡ λt.(snd(f@t))@r(2) * t
21. ∀t:{x:ℝ| ((r1/r(2)) ≤ x) ∧ (x ≤ r1)} . hb@t ≡ λt.(snd(g@t))@(r(2) * t) - r1
22. λt.<ha@t, hb@t> ∈ Point(Path(A × B))
23. t : {x:ℝ| ((r1/r(2)) ≤ x) ∧ (x ≤ r1)} @i
24. hb@t ≡ snd(g@(r(2) * t) - r1)
25. ha@t ≡ fst(g@(r(2) * t) - r1)
26. ∀t@0:Top. (fst(t@t@0) ~ fst(t@t@0))
27. ∀t@0:Top. (snd(t@t@0) ~ snd(t@t@0))
28. (r(2) * t) - r1 ∈ {x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} 
⊢ λt.<ha@t, hb@t>@t ≡ g@(r(2) * t) - r1
BY
{ (RWO "prod-ss-eq" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  [A]  :  SeparationSpace
2.  [B]  :  SeparationSpace
3.  \mforall{}f,g:Point(Path(A)).
          (f@r1  \mequiv{}  g@r0
          {}\mRightarrow{}  (\mexists{}h:Point(Path(A))
                    ((\mforall{}t:\{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  (r1/r(2)))\}  .  h@t  \mequiv{}  f@r(2)  *  t)
                    \mwedge{}  (\mforall{}t:\{x:\mBbbR{}|  ((r1/r(2))  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}  .  h@t  \mequiv{}  g@(r(2)  *  t)  -  r1))))
4.  \mforall{}f,g:Point(Path(B)).
          (f@r1  \mequiv{}  g@r0
          {}\mRightarrow{}  (\mexists{}h:Point(Path(B))
                    ((\mforall{}t:\{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  (r1/r(2)))\}  .  h@t  \mequiv{}  f@r(2)  *  t)
                    \mwedge{}  (\mforall{}t:\{x:\mBbbR{}|  ((r1/r(2))  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}  .  h@t  \mequiv{}  g@(r(2)  *  t)  -  r1))))
5.  f  :  Point(Path(A  \mtimes{}  B))@i
6.  g  :  Point(Path(A  \mtimes{}  B))@i
7.  f@r1  \mequiv{}  g@r0
8.  \mlambda{}t.(fst(f@t))  \mmember{}  Point(Path(A))
9.  \mlambda{}t.(fst(g@t))  \mmember{}  Point(Path(A))
10.  \mlambda{}t.(snd(f@t))  \mmember{}  Point(Path(B))
11.  \mlambda{}t.(snd(g@t))  \mmember{}  Point(Path(B))
12.  \mforall{}f,t:Top.    (snd(f@t)  \msim{}  \mlambda{}t.(snd(f@t))@t)
13.  \mforall{}f,t:Top.    (fst(f@t)  \msim{}  \mlambda{}t.(fst(f@t))@t)
14.  \mlambda{}t.(fst(f@t))@r1  \mequiv{}  \mlambda{}t.(fst(g@t))@r0
15.  \mlambda{}t.(snd(f@t))@r1  \mequiv{}  \mlambda{}t.(snd(g@t))@r0
16.  ha  :  Point(Path(A))
17.  \mforall{}t:\{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  (r1/r(2)))\}  .  ha@t  \mequiv{}  \mlambda{}t.(fst(f@t))@r(2)  *  t
18.  \mforall{}t:\{x:\mBbbR{}|  ((r1/r(2))  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}  .  ha@t  \mequiv{}  \mlambda{}t.(fst(g@t))@(r(2)  *  t)  -  r1
19.  hb  :  Point(Path(B))
20.  \mforall{}t:\{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  (r1/r(2)))\}  .  hb@t  \mequiv{}  \mlambda{}t.(snd(f@t))@r(2)  *  t
21.  \mforall{}t:\{x:\mBbbR{}|  ((r1/r(2))  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}  .  hb@t  \mequiv{}  \mlambda{}t.(snd(g@t))@(r(2)  *  t)  -  r1
22.  \mlambda{}t.<ha@t,  hb@t>  \mmember{}  Point(Path(A  \mtimes{}  B))
23.  t  :  \{x:\mBbbR{}|  ((r1/r(2))  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}  @i
24.  hb@t  \mequiv{}  snd(g@(r(2)  *  t)  -  r1)
25.  ha@t  \mequiv{}  fst(g@(r(2)  *  t)  -  r1)
26.  \mforall{}t@0:Top.  (fst(t@t@0)  \msim{}  fst(t@t@0))
27.  \mforall{}t@0:Top.  (snd(t@t@0)  \msim{}  snd(t@t@0))
28.  (r(2)  *  t)  -  r1  \mmember{}  \{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\} 
\mvdash{}  \mlambda{}t.<ha@t,  hb@t>@t  \mequiv{}  g@(r(2)  *  t)  -  r1


By

---

Latex:
(RWO  "prod-ss-eq"  0  THEN  Auto)

---

Home Index