---

Step * of Lemma groupoid-square-commutes-iff2

∀[G:Groupoid]. ∀[x,y1,y2,z:cat-ob(cat(G))]. ∀[x_y1:cat-arrow(cat(G)) x y1]. ∀[y1_z:cat-arrow(cat(G)) y1 z].
∀[x_y2:cat-arrow(cat(G)) x y2]. ∀[y2_z:cat-arrow(cat(G)) y2 z].
  uiff(x_y1 o y1_z = x_y2 o y2_z;x_y1
  = (cat-comp(cat(G)) x z y1 (cat-comp(cat(G)) x y2 z x_y2 y2_z) groupoid-inv(G;y1;z;y1_z))
  ∈ (cat-arrow(cat(G)) x y1))
BY
{ (Auto THEN All (RepUR ``cat-square-commutes``)) }

1
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)
⊢ x_y1
= (cat-comp(cat(G)) x z y1 (cat-comp(cat(G)) x y2 z x_y2 y2_z) groupoid-inv(G;y1;z;y1_z))
∈ (cat-arrow(cat(G)) x y1)

2
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. x_y1
= (cat-comp(cat(G)) x z y1 (cat-comp(cat(G)) x y2 z x_y2 y2_z) groupoid-inv(G;y1;z;y1_z))
∈ (cat-arrow(cat(G)) x y1)
⊢ (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)

---

Latex:

---

Latex:
\mforall{}[G:Groupoid].  \mforall{}[x,y1,y2,z:cat-ob(cat(G))].  \mforall{}[x$_{y1}$:cat-arrow(cat(G))  x  y1].  \000C\mforall{}[y1$_{z}$:cat-arrow(cat(G)) 
                                                                                                                                                                  y1 
                                                                                                                                                                  z].
\mforall{}[x$_{y2}$:cat-arrow(cat(G))  x  y2].  \mforall{}[y2$_{z}$:cat-arrow(cat\000C(G))  y2  z].
    uiff(x$_{y1}$  o  y1$_{z}$  =  x$_{y2}$  o  \000Cy2$_{z}$;x$_{y1}$
    =  (cat-comp(cat(G))  x  z  y1  (cat-comp(cat(G))  x  y2  z  x$_{y2}$  y2$_{\000Cz}$)  groupoid-inv(G;y1;z;y1$_{z}$)))


By

---

Latex:
(Auto  THEN  All  (RepUR  ``cat-square-commutes``))

---

Home Index