---

Step * 1 1 2 2 1 1 of Lemma inj_into_ocmon


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. ∀x,y:|g|.  (↑(x =b y) ⇐⇒ ↑((f x) =b (f y)))
17. ∀x,y:|g|.  (↑(x ≤b y) ⇐⇒ ↑((f x) ≤b (f y)))
18. x : |g|
19. x1 : |g|
⊢ (f x) = (f x1) ∈ |h| ⇐⇒ (↑((f x) ≤b (f x1))) ∧ (↑((f x1) ≤b (f x)))
BY
{ Auto }

---

Latex:

---

Latex:

1.  g  :  GrpSig
2.  h  :  OCMon
3.  Assoc(|h|;*)
4.  Ident(|h|;*;e)
5.  Comm(|h|;*)
6.  UniformlyRefl(|h|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y))
7.  UniformlyTrans(|h|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y))
8.  UniformlyAntiSym(|h|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y))
9.  Connex(|h|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y))
10.  Cancel(|h|;|h|;*)
11.  \mforall{}[z:|h|].  monot(|h|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y);\mlambda{}w.(z  *  w))
12.  f  :  |g|  {}\mrightarrow{}  |h|
13.  FunThru2op(|g|;|h|;*;*;f)
14.  (f  e)  =  e
15.  Inj(|g|;|h|;f)
16.  \mforall{}x,y:|g|.    (\muparrow{}(x  =\msubb{}  y)  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}((f  x)  =\msubb{}  (f  y)))
17.  \mforall{}x,y:|g|.    (\muparrow{}(x  \mleq{}\msubb{}  y)  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}((f  x)  \mleq{}\msubb{}  (f  y)))
18.  x  :  |g|
19.  x1  :  |g|
\mvdash{}  (f  x)  =  (f  x1)  \mLeftarrow{}{}\mRightarrow{}  (\muparrow{}((f  x)  \mleq{}\msubb{}  (f  x1)))  \mwedge{}  (\muparrow{}((f  x1)  \mleq{}\msubb{}  (f  x)))


By

---

Latex:
Auto

---

Home Index