---

Step * 1 of Lemma inj_into_ocmon


1. g : GrpSig
2. h : OCMon
3. f : |g| ⟶ |h|
4. IsMonHomInj(g;h;f)
5. RelsIso(|g|;|h|;x,y.↑(x =b y);x,y.↑(x =b y);f)
6. RelsIso(|g|;|h|;x,y.↑(x ≤b y);x,y.↑(x ≤b y);f)
⊢ g ∈ OCMon
BY
{ ((AddAllProperties 2 THENA Auto) THEN ARepD ["compound"] THEN Thin 10 THENM Thin 12) }

1
1. g : GrpSig
2. h : OCMon
3. Assoc(|h|;*)
4. Ident(|h|;*;e)
5. Comm(|h|;*)
6. UniformlyRefl(|h|;x,y.↑(x ≤b y))
7. UniformlyTrans(|h|;x,y.↑(x ≤b y))
8. UniformlyAntiSym(|h|;x,y.↑(x ≤b y))
9. Connex(|h|;x,y.↑(x ≤b y))
10. Cancel(|h|;|h|;*)
11. ∀[z:|h|]. monot(|h|;x,y.↑(x ≤b y);λw.(z * w))
12. f : |g| ⟶ |h|
13. FunThru2op(|g|;|h|;*;*;f)
14. (f e) = e ∈ |h|
15. Inj(|g|;|h|;f)
16. RelsIso(|g|;|h|;x,y.↑(x =b y);x,y.↑(x =b y);f)
17. RelsIso(|g|;|h|;x,y.↑(x ≤b y);x,y.↑(x ≤b y);f)
⊢ g ∈ OCMon

---

Latex:

---

Latex:

1.  g  :  GrpSig
2.  h  :  OCMon
3.  f  :  |g|  {}\mrightarrow{}  |h|
4.  IsMonHomInj(g;h;f)
5.  RelsIso(|g|;|h|;x,y.\muparrow{}(x  =\msubb{}  y);x,y.\muparrow{}(x  =\msubb{}  y);f)
6.  RelsIso(|g|;|h|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y);x,y.\muparrow{}(x  \mleq{}\msubb{}  y);f)
\mvdash{}  g  \mmember{}  OCMon


By

---

Latex:
((AddAllProperties  2  THENA  Auto)  THEN  ARepD  ["compound"]  THEN  Thin  10  THENM  Thin  12)

---

Home Index