---

Step * 1 5 1 1 1 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)). path-comp-rel(A;f;g;h)))
4. ∀f,g:Point(Path(B)).  (f@r1 ≡ g@r0 ⇒ (∃h:Point(Path(B)). path-comp-rel(B;f;g;h)))
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. path-comp-rel(A;λt.(fst(f@t));λt.(fst(g@t));ha)
18. hb : Point(Path(B))
19. path-comp-rel(B;λt.(snd(f@t));λt.(snd(g@t));hb)
20. λt.<ha@t, hb@t> ∈ Point(Path(A × B))
⊢ path-comp-rel(A × B;f;g;λt.<ha@t, hb@t>)
BY
{ (All (RepUR ``path-comp-rel``)
   THEN ExRepD
   THEN D 0
   THEN Intros
   THEN ∀h:hyp. ((InstHyp [⌜t⌝] h⋅ THENA Trivial) THEN (RWO "12< 13<" (-1) THENA Complete (Auto))) ) }

1
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:ℝ| (r0 ≤ x) ∧ (x ≤ (r1/r(2)))} @i
24. hb@t ≡ snd(f@r(2) * t)
25. ha@t ≡ fst(f@r(2) * t)
26. ∀t@0:Top. (fst(t@t@0) ~ fst(t@t@0))
27. ∀t@0:Top. (snd(t@t@0) ~ snd(t@t@0))
⊢ λt.<ha@t, hb@t>@t ≡ f@r(2) * t

2
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))
⊢ λt.<ha@t, hb@t>@t ≡ g@(r(2) * t) - r1

---

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)).  path-comp-rel(A;f;g;h)))
4.  \mforall{}f,g:Point(Path(B)).    (f@r1  \mequiv{}  g@r0  {}\mRightarrow{}  (\mexists{}h:Point(Path(B)).  path-comp-rel(B;f;g;h)))
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.  path-comp-rel(A;\mlambda{}t.(fst(f@t));\mlambda{}t.(fst(g@t));ha)
18.  hb  :  Point(Path(B))
19.  path-comp-rel(B;\mlambda{}t.(snd(f@t));\mlambda{}t.(snd(g@t));hb)
20.  \mlambda{}t.<ha@t,  hb@t>  \mmember{}  Point(Path(A  \mtimes{}  B))
\mvdash{}  path-comp-rel(A  \mtimes{}  B;f;g;\mlambda{}t.<ha@t,  hb@t>)


By

---

Latex:
(All  (RepUR  ``path-comp-rel``)
  THEN  ExRepD
  THEN  D  0
  THEN  Intros
  THEN  \mforall{}h:hyp.  ((InstHyp  [\mkleeneopen{}t\mkleeneclose{}]  h\mcdot{}  THENA  Trivial)  THEN  (RWO  "12<  13<"  (-1)  THENA  Complete  (Auto)))  )

---

Home Index