---

Step * 1 of Lemma groupoid-square-commutes-iff


1. G : Groupoid
2. x : cat-ob(cat(G))
3. y1 : cat-ob(cat(G))
4. y2 : cat-ob(cat(G))
5. z : cat-ob(cat(G))
6. x_y1 : cat-arrow(cat(G)) x y1
7. y1_z : cat-arrow(cat(G)) y1 z
8. x_y2 : cat-arrow(cat(G)) x y2
9. y2_z : cat-arrow(cat(G)) y2 z
10. (cat-comp(cat(G)) x y1 z x_y1 y1_z) = (cat-comp(cat(G)) x y2 z x_y2 y2_z) ∈ (cat-arrow(cat(G)) x z)
⊢ y2_z
= (cat-comp(cat(G)) y2 x z groupoid-inv(G;x;y2;x_y2) (cat-comp(cat(G)) x y2 z x_y2 y2_z))
∈ (cat-arrow(cat(G)) y2 z)
BY
{ TACTIC:((RWO  "cat-comp-assoc<" 0 THENA Auto) THEN RWO "groupoid_inv.2" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  G  :  Groupoid
2.  x  :  cat-ob(cat(G))
3.  y1  :  cat-ob(cat(G))
4.  y2  :  cat-ob(cat(G))
5.  z  :  cat-ob(cat(G))
6.  x$_{y1}$  :  cat-arrow(cat(G))  x  y1
7.  y1$_{z}$  :  cat-arrow(cat(G))  y1  z
8.  x$_{y2}$  :  cat-arrow(cat(G))  x  y2
9.  y2$_{z}$  :  cat-arrow(cat(G))  y2  z
10.  (cat-comp(cat(G))  x  y1  z  x$_{y1}$  y1$_{z}$)  =  (cat-comp(\000Ccat(G))  x  y2  z  x$_{y2}$  y2$_{z}$)
\mvdash{}  y2$_{z}$  =  (cat-comp(cat(G))  y2  x  z  groupoid-inv(G;x;y2;x$_{y2\mbackslash{}ff7\000Cd$)  (cat-comp(cat(G))  x  y2  z  x$_{y2}$  y2$_{z}$))


By

---

Latex:
TACTIC:((RWO    "cat-comp-assoc<"  0  THENA  Auto)  THEN  RWO  "groupoid\_inv.2"  0  THEN  Auto)

---

Home Index