---

Step * of Lemma omral_fma_wf2

∀g:OCMon. ∀a:CDRng.  (omral_fma(g;a) ∈ FMonAlg(g;a))
BY
{ (Auto THEN MemTypeCD THEN Auto) }

1
1. g : OCMon
2. a : CDRng
⊢ IsMonHom{g,omral_fma(g;a).alg↓rg↓xmn}(omral_fma(g;a).inj)

2
1. g : OCMon
2. a : CDRng
3. IsMonHom{g,omral_fma(g;a).alg↓rg↓xmn}(omral_fma(g;a).inj)
4. n : algebra{i:l}(a)
5. f : MonHom(g,n↓rg↓xmn)
⊢ (omral_fma(g;a).umap n f) = !f':omral_fma(g;a).alg.car ⟶ n.car
                                (alg_hom_p(a; omral_fma(g;a).alg; n; f')
                                ∧ ((f' o omral_fma(g;a).inj) = f ∈ (|g| ⟶ n.car)))

---

Latex:

---

Latex:
\mforall{}g:OCMon.  \mforall{}a:CDRng.    (omral\_fma(g;a)  \mmember{}  FMonAlg(g;a))


By

---

Latex:
(Auto  THEN  MemTypeCD  THEN  Auto)

---

Home Index