---

Step * 2 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. y2_z
= (cat-comp(cat(G)) y2 x z groupoid-inv(G;x;y2;x_y2) (cat-comp(cat(G)) x y1 z x_y1 y1_z))
∈ (cat-arrow(cat(G)) y2 z)
⊢ (cat-comp(cat(G)) x y1 z x_y1 y1_z)
= (cat-comp(cat(G)) x y2 z x_y2 (cat-comp(cat(G)) y2 x z groupoid-inv(G;x;y2;x_y2) (cat-comp(cat(G)) x y1 z x_y1 y1_z)))
∈ (cat-arrow(cat(G)) x z)
BY
{ TACTIC:((RWO  "cat-comp-assoc<" 0 THENA Auto) THEN RWO "groupoid_inv.1" 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.  y2$_{z}$  =  (cat-comp(cat(G))  y2  x  z  groupoid-inv(G;x;y2;x$_{y2\mbackslash{}f\000Cf7d$)  (cat-comp(cat(G))  x  y1  z  x$_{y1}$  y1$_{z}$))
\mvdash{}  (cat-comp(cat(G))  x  y1  z  x$_{y1}$  y1$_{z}$)
=  (cat-comp(cat(G))  x  y2  z  x$_{y2}$ 
      (cat-comp(cat(G))  y2  x  z  groupoid-inv(G;x;y2;x$_{y2}$)  (cat-comp(cat(G))  x  y1\000C  z  x$_{y1}$  y1$_{z}$)))


By

---

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

---

Home Index