---

Step * of Lemma fmonalg_properties

∀g:AbMon. ∀a:CRng. ∀m:FMonAlg(g;a).
  (IsMonHom{g,m.alg↓rg↓xmn}(m.inj)
  ∧ (∀n:algebra{i:l}(a). ∀f:MonHom(g,n↓rg↓xmn).
       (m.umap n f) = !f':m.alg.car ⟶ n.car. (alg_hom_p(a; m.alg; n; f') ∧ ((f' o m.inj) = f ∈ (|g| ⟶ n.car)))))
BY
{ ((UnivCD THENA Auto) THEN skip{(D -1 THEN Auto THEN BackThruSomeHyp)}) }

1
1. g : AbMon
2. a : CRng
3. m : FMonAlg(g;a)
⊢ IsMonHom{g,m.alg↓rg↓xmn}(m.inj)
∧ (∀n:algebra{i:l}(a). ∀f:MonHom(g,n↓rg↓xmn).
     (m.umap n f) = !f':m.alg.car ⟶ n.car. (alg_hom_p(a; m.alg; n; f') ∧ ((f' o m.inj) = f ∈ (|g| ⟶ n.car))))

---

Latex:

---

Latex:
\mforall{}g:AbMon.  \mforall{}a:CRng.  \mforall{}m:FMonAlg(g;a).
    (IsMonHom\{g,m.alg\mdownarrow{}rg\mdownarrow{}xmn\}(m.inj)
    \mwedge{}  (\mforall{}n:algebra\{i:l\}(a).  \mforall{}f:MonHom(g,n\mdownarrow{}rg\mdownarrow{}xmn).
              (m.umap  n  f)  =  !f':m.alg.car  {}\mrightarrow{}  n.car.  (alg\_hom\_p(a;  m.alg;  n;  f')  \mwedge{}  ((f'  o  m.inj)  =  f))))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  skip\{(D  -1  THEN  Auto  THEN  BackThruSomeHyp)\})

---

Home Index