---

Step * 1 1 2 4 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. 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)
18. UniformLinorder(|g|;x,y.↑(x ≤b y))
19. =b = (λx,y. ((x ≤b y) ∧b (y ≤b x))) ∈ (|g| ⟶ |g| ⟶ 𝔹)
20. Cancel(|g|;|g|;*)
21. z : |g|
⊢ fun_thru_1op(|g|;|h|;λw.(z * w);λw.((f z) * w);f)
BY
{ ((All (Eval ``fun_thru_1op fun_thru_2op``)  
THENM RepD) THENA Auto) }

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. ∀[a1,a2:|g|].  ((f (a1 * a2)) = ((f a1) * (f a2)) ∈ |h|)
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)
18. UniformLinorder(|g|;x,y.↑(x ≤b y))
19. =b = (λx,y. ((x ≤b y) ∧b (y ≤b x))) ∈ (|g| ⟶ |g| ⟶ 𝔹)
20. Cancel(|g|;|g|;*)
21. z : |g|
22. a : |g|
⊢ (f (z * a)) = ((f z) * (f a)) ∈ |h|

---

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.  RelsIso(|g|;|h|;x,y.\muparrow{}(x  =\msubb{}  y);x,y.\muparrow{}(x  =\msubb{}  y);f)
17.  RelsIso(|g|;|h|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y);x,y.\muparrow{}(x  \mleq{}\msubb{}  y);f)
18.  UniformLinorder(|g|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y))
19.  =\msubb{}  =  (\mlambda{}x,y.  ((x  \mleq{}\msubb{}  y)  \mwedge{}\msubb{}  (y  \mleq{}\msubb{}  x)))
20.  Cancel(|g|;|g|;*)
21.  z  :  |g|
\mvdash{}  fun\_thru\_1op(|g|;|h|;\mlambda{}w.(z  *  w);\mlambda{}w.((f  z)  *  w);f)


By

---

Latex:
((All  (Eval  ``fun\_thru\_1op  fun\_thru\_2op``)   
THENM  RepD)  THENA  Auto)

---

Home Index