Step
*
2
2
1
1
1
1
1
of Lemma
groupoid-edges-commute
.....antecedent.....
1. G : Groupoid
2. I : Cname List
3. J : nameset(I) List
4. x : nameset(I)
5. i : ℕ2
6. box : open_box(cubical-nerve(fst(G));I;J;x;i)
7. (∃j1∈J. (∃j2∈J. ¬(j1 = j2 ∈ Cname)))
8. f : name-morph(I;[])
9. a : nameset(I)
10. (f a) = 0 ∈ ℕ2
11. b : nameset(I)
12. (f b) = 0 ∈ ℕ2
13. ¬(a = b ∈ nameset(I))
14. ¬(∃v∈box. (¬(dimension(v) = b ∈ Cname)) ∧ (¬(dimension(v) = a ∈ Cname)) ∧ (direction(v) = (f dimension(v)) ∈ ℕ2))
15. (∀j∈J.(j = a ∈ Cname) ∨ (j = b ∈ Cname))
16. (a ∈ J)
17. (b ∈ J)
18. ¬(x = a ∈ Cname)
19. ¬(x = b ∈ Cname)
20. ¬((f x) = i ∈ ℕ2)
21. eq-cname(a;b) ~ ff
22. eq-cname(b;a) ~ eq-cname(a;b)
23. (flip(f;x) a) = 0 ∈ ℕ2
24. (flip(f;b) a) = 0 ∈ ℕ2
25. (flip(f;x) b) = 0 ∈ ℕ2
26. (flip(f;a) b) = 0 ∈ ℕ2
27. (flip(flip(f;x);b) a) = 0 ∈ ℕ2
28. (flip(flip(f;x);a) b) = 0 ∈ ℕ2
⊢ (∃i:cat-arrow(cat(G)) nerve_box_label(box;f) nerve_box_label(box;flip(f;x))
∃j:cat-arrow(cat(G)) nerve_box_label(box;flip(f;b)) nerve_box_label(box;flip(flip(f;x);b))
∃k:cat-arrow(cat(G)) nerve_box_label(box;flip(flip(f;a);b)) nerve_box_label(box;flip(flip(flip(f;x);a);b))
∃l:cat-arrow(cat(G)) nerve_box_label(box;flip(f;a)) nerve_box_label(box;flip(flip(f;x);a))
(nerve_box_edge(box;f;b) o j = i o nerve_box_edge(box;flip(f;x);b)
∧ nerve_box_edge(box;flip(f;b);a) o k = j o nerve_box_edge(box;flip(flip(f;x);b);a)
∧ l o nerve_box_edge(box;flip(flip(f;x);a);b) = nerve_box_edge(box;flip(f;a);b) o k
∧ i o nerve_box_edge(box;flip(f;x);a) = nerve_box_edge(box;f;a) o l))
∨ (∃i:cat-arrow(cat(G)) nerve_box_label(box;flip(f;x)) nerve_box_label(box;f)
∃j:cat-arrow(cat(G)) nerve_box_label(box;flip(flip(f;x);b)) nerve_box_label(box;flip(f;b))
∃k:cat-arrow(cat(G)) nerve_box_label(box;flip(flip(flip(f;x);a);b)) nerve_box_label(box;flip(flip(f;a);b))
∃l:cat-arrow(cat(G)) nerve_box_label(box;flip(flip(f;x);a)) nerve_box_label(box;flip(f;a))
(nerve_box_edge(box;flip(f;x);b) o j = i o nerve_box_edge(box;f;b)
∧ nerve_box_edge(box;flip(flip(f;x);b);a) o k = j o nerve_box_edge(box;flip(f;b);a)
∧ nerve_box_edge(box;flip(flip(f;x);a);b) o k = l o nerve_box_edge(box;flip(f;a);b)
∧ i o nerve_box_edge(box;f;a) = nerve_box_edge(box;flip(f;x);a) o l))
BY
{ (RepeatFor 2 (Thin (-7))
THEN (Assert ((i = 1 ∈ ℕ2) ∧ ((f x) = 0 ∈ ℕ2)) ∨ ((i = 0 ∈ ℕ2) ∧ ((f x) = 1 ∈ ℕ2)) BY
(MoveToConcl 20
THEN (GenConcl ⌜(f x) = u ∈ ℕ2⌝⋅ THENA Auto)
THEN All Thin
THEN IntSegCases 2
THEN IntSegCases 1
THEN Auto))
) }
1
1. G : Groupoid
2. I : Cname List
3. J : nameset(I) List
4. x : nameset(I)
5. i : ℕ2
6. box : open_box(cubical-nerve(fst(G));I;J;x;i)
7. (∃j1∈J. (∃j2∈J. ¬(j1 = j2 ∈ Cname)))
8. f : name-morph(I;[])
9. a : nameset(I)
10. (f a) = 0 ∈ ℕ2
11. b : nameset(I)
12. (f b) = 0 ∈ ℕ2
13. ¬(a = b ∈ nameset(I))
14. ¬(∃v∈box. (¬(dimension(v) = b ∈ Cname)) ∧ (¬(dimension(v) = a ∈ Cname)) ∧ (direction(v) = (f dimension(v)) ∈ ℕ2))
15. (∀j∈J.(j = a ∈ Cname) ∨ (j = b ∈ Cname))
16. (a ∈ J)
17. (b ∈ J)
18. ¬(x = a ∈ Cname)
19. ¬(x = b ∈ Cname)
20. ¬((f x) = i ∈ ℕ2)
21. (flip(f;x) a) = 0 ∈ ℕ2
22. (flip(f;b) a) = 0 ∈ ℕ2
23. (flip(f;x) b) = 0 ∈ ℕ2
24. (flip(f;a) b) = 0 ∈ ℕ2
25. (flip(flip(f;x);b) a) = 0 ∈ ℕ2
26. (flip(flip(f;x);a) b) = 0 ∈ ℕ2
27. ((i = 1 ∈ ℕ2) ∧ ((f x) = 0 ∈ ℕ2)) ∨ ((i = 0 ∈ ℕ2) ∧ ((f x) = 1 ∈ ℕ2))
⊢ (∃i:cat-arrow(cat(G)) nerve_box_label(box;f) nerve_box_label(box;flip(f;x))
∃j:cat-arrow(cat(G)) nerve_box_label(box;flip(f;b)) nerve_box_label(box;flip(flip(f;x);b))
∃k:cat-arrow(cat(G)) nerve_box_label(box;flip(flip(f;a);b)) nerve_box_label(box;flip(flip(flip(f;x);a);b))
∃l:cat-arrow(cat(G)) nerve_box_label(box;flip(f;a)) nerve_box_label(box;flip(flip(f;x);a))
(nerve_box_edge(box;f;b) o j = i o nerve_box_edge(box;flip(f;x);b)
∧ nerve_box_edge(box;flip(f;b);a) o k = j o nerve_box_edge(box;flip(flip(f;x);b);a)
∧ l o nerve_box_edge(box;flip(flip(f;x);a);b) = nerve_box_edge(box;flip(f;a);b) o k
∧ i o nerve_box_edge(box;flip(f;x);a) = nerve_box_edge(box;f;a) o l))
∨ (∃i:cat-arrow(cat(G)) nerve_box_label(box;flip(f;x)) nerve_box_label(box;f)
∃j:cat-arrow(cat(G)) nerve_box_label(box;flip(flip(f;x);b)) nerve_box_label(box;flip(f;b))
∃k:cat-arrow(cat(G)) nerve_box_label(box;flip(flip(flip(f;x);a);b)) nerve_box_label(box;flip(flip(f;a);b))
∃l:cat-arrow(cat(G)) nerve_box_label(box;flip(flip(f;x);a)) nerve_box_label(box;flip(f;a))
(nerve_box_edge(box;flip(f;x);b) o j = i o nerve_box_edge(box;f;b)
∧ nerve_box_edge(box;flip(flip(f;x);b);a) o k = j o nerve_box_edge(box;flip(f;b);a)
∧ nerve_box_edge(box;flip(flip(f;x);a);b) o k = l o nerve_box_edge(box;flip(f;a);b)
∧ i o nerve_box_edge(box;f;a) = nerve_box_edge(box;flip(f;x);a) o l))
Latex:
Latex:
.....antecedent.....
1. G : Groupoid
2. I : Cname List
3. J : nameset(I) List
4. x : nameset(I)
5. i : \mBbbN{}2
6. box : open\_box(cubical-nerve(fst(G));I;J;x;i)
7. (\mexists{}j1\mmember{}J. (\mexists{}j2\mmember{}J. \mneg{}(j1 = j2)))
8. f : name-morph(I;[])
9. a : nameset(I)
10. (f a) = 0
11. b : nameset(I)
12. (f b) = 0
13. \mneg{}(a = b)
14. \mneg{}(\mexists{}v\mmember{}box. (\mneg{}(dimension(v) = b)) \mwedge{} (\mneg{}(dimension(v) = a)) \mwedge{} (direction(v) = (f dimension(v))))
15. (\mforall{}j\mmember{}J.(j = a) \mvee{} (j = b))
16. (a \mmember{} J)
17. (b \mmember{} J)
18. \mneg{}(x = a)
19. \mneg{}(x = b)
20. \mneg{}((f x) = i)
21. eq-cname(a;b) \msim{} ff
22. eq-cname(b;a) \msim{} eq-cname(a;b)
23. (flip(f;x) a) = 0
24. (flip(f;b) a) = 0
25. (flip(f;x) b) = 0
26. (flip(f;a) b) = 0
27. (flip(flip(f;x);b) a) = 0
28. (flip(flip(f;x);a) b) = 0
\mvdash{} (\mexists{}i:cat-arrow(cat(G)) nerve\_box\_label(box;f) nerve\_box\_label(box;flip(f;x))
\mexists{}j:cat-arrow(cat(G)) nerve\_box\_label(box;flip(f;b)) nerve\_box\_label(box;flip(flip(f;x);b))
\mexists{}k:cat-arrow(cat(G)) nerve\_box\_label(box;flip(flip(f;a);b))
nerve\_box\_label(box;flip(flip(flip(f;x);a);b))
\mexists{}l:cat-arrow(cat(G)) nerve\_box\_label(box;flip(f;a)) nerve\_box\_label(box;flip(flip(f;x);a))
(nerve\_box\_edge(box;f;b) o j = i o nerve\_box\_edge(box;flip(f;x);b)
\mwedge{} nerve\_box\_edge(box;flip(f;b);a) o k = j o nerve\_box\_edge(box;flip(flip(f;x);b);a)
\mwedge{} l o nerve\_box\_edge(box;flip(flip(f;x);a);b) = nerve\_box\_edge(box;flip(f;a);b) o k
\mwedge{} i o nerve\_box\_edge(box;flip(f;x);a) = nerve\_box\_edge(box;f;a) o l))
\mvee{} (\mexists{}i:cat-arrow(cat(G)) nerve\_box\_label(box;flip(f;x)) nerve\_box\_label(box;f)
\mexists{}j:cat-arrow(cat(G)) nerve\_box\_label(box;flip(flip(f;x);b)) nerve\_box\_label(box;flip(f;b))
\mexists{}k:cat-arrow(cat(G)) nerve\_box\_label(box;flip(flip(flip(f;x);a);b))
nerve\_box\_label(box;flip(flip(f;a);b))
\mexists{}l:cat-arrow(cat(G)) nerve\_box\_label(box;flip(flip(f;x);a)) nerve\_box\_label(box;flip(f;a))
(nerve\_box\_edge(box;flip(f;x);b) o j = i o nerve\_box\_edge(box;f;b)
\mwedge{} nerve\_box\_edge(box;flip(flip(f;x);b);a) o k = j o nerve\_box\_edge(box;flip(f;b);a)
\mwedge{} nerve\_box\_edge(box;flip(flip(f;x);a);b) o k = l o nerve\_box\_edge(box;flip(f;a);b)
\mwedge{} i o nerve\_box\_edge(box;f;a) = nerve\_box\_edge(box;flip(f;x);a) o l))
By
Latex:
(RepeatFor 2 (Thin (-7))
THEN (Assert ((i = 1) \mwedge{} ((f x) = 0)) \mvee{} ((i = 0) \mwedge{} ((f x) = 1)) BY
(MoveToConcl 20
THEN (GenConcl \mkleeneopen{}(f x) = u\mkleeneclose{}\mcdot{} THENA Auto)
THEN All Thin
THEN IntSegCases 2
THEN IntSegCases 1
THEN Auto))
)
Home
Index