---

Step * 1 1 of Lemma hgrp_of_ocgrp_wf2


1. g : OGrp
⊢ IsMonHomInj(g↓hgrp;g;λx.x)
BY
{ ((Eval ``inject monoid_hom_p fun_thru_2op mon_hom_inj_p`` 0) THEN Auto) }

1
1. g : OGrp
2. ∀[a1,a2:|g|+].  ((a1 * a2) = (a1 * a2) ∈ |g|)
3. e = e ∈ |g|
4. a1 : |g|+@i
5. a2 : |g|+@i
6. a1 = a2 ∈ |g|@i
⊢ a1 = a2 ∈ |g|+

---

Latex:

---

Latex:

1.  g  :  OGrp
\mvdash{}  IsMonHomInj(g\mdownarrow{}hgrp;g;\mlambda{}x.x)


By

---

Latex:
((Eval  ``inject  monoid\_hom\_p  fun\_thru\_2op  mon\_hom\_inj\_p``  0)  THEN  Auto)

---

Home Index