---

Step * 1 1 of Lemma free_abmon_endomorph_is_id


1. S : DSet
2. M : FAbMon(S)
3. f : MonHom(M.mon,M.mon)
4. (f o M.inj) = M.inj ∈ (|S| ⟶ |M.mon|)
5. ((M.umap M.mon M.inj) o M.inj) = M.inj ∈ (|S| ⟶ |M.mon|)
6. ∀f:MonHom(M.mon,M.mon)
     (((f o M.inj) = M.inj ∈ (|S| ⟶ |M.mon|)) ⇒ (f = (M.umap M.mon M.inj) ∈ (|M.mon| ⟶ |M.mon|)))
⊢ f = Id{|M.mon|} ∈ (|M.mon| ⟶ |M.mon|)
BY
{ ((InstHyp [Id{|M.mon|}] 6 
 ) THENA Auto) }

1
1. S : DSet
2. M : FAbMon(S)
3. f : MonHom(M.mon,M.mon)
4. (f o M.inj) = M.inj ∈ (|S| ⟶ |M.mon|)
5. ((M.umap M.mon M.inj) o M.inj) = M.inj ∈ (|S| ⟶ |M.mon|)
6. ∀f:MonHom(M.mon,M.mon)
     (((f o M.inj) = M.inj ∈ (|S| ⟶ |M.mon|)) ⇒ (f = (M.umap M.mon M.inj) ∈ (|M.mon| ⟶ |M.mon|)))
7. Id{|M.mon|} = (M.umap M.mon M.inj) ∈ (|M.mon| ⟶ |M.mon|)
⊢ f = Id{|M.mon|} ∈ (|M.mon| ⟶ |M.mon|)

---

Latex:

---

Latex:

1.  S  :  DSet
2.  M  :  FAbMon(S)
3.  f  :  MonHom(M.mon,M.mon)
4.  (f  o  M.inj)  =  M.inj
5.  ((M.umap  M.mon  M.inj)  o  M.inj)  =  M.inj
6.  \mforall{}f:MonHom(M.mon,M.mon).  (((f  o  M.inj)  =  M.inj)  {}\mRightarrow{}  (f  =  (M.umap  M.mon  M.inj)))
\mvdash{}  f  =  Id\{|M.mon|\}


By

---

Latex:
((InstHyp  [Id\{|M.mon|\}]  6 
  )  THENA  Auto)

---

Home Index