---

Step * 1 2 of Lemma oal_omcp_wf

.....set predicate..... 
1. s : LOSet@i'
2. g : OGrp@i'
⊢ (∀j:|s|. IsMonHom{g↓hgrp,<oal_hgp(s;g), λk,v. inj(k,v), λh,f. umap(h,f)>.mon}(<oal_hgp(s;g), λk,v. inj(k,v), λh,f. uma\000Cp(h,f)>.inj j))
∧ (∀h:AbMon. ∀f:|s| ⟶ MonHom(g↓hgrp,h).
     (<oal_hgp(s;g), λk,v. inj(k,v), λh,f. umap(h,f)>.umap h f) = !v:|<oal_hgp(s;g), λk,v. inj(k,v), λh,f. umap(h,f)>.mo\000Cn| ⟶ |h|
                                                            (IsMonHom{<oal_hgp(s;g), λk,v. inj(k,v), λh,f. umap(h,f)>.mo\000Cn,h}(v)
                                                            ∧ (∀j:|s|
                                                                 ((f j)
                                                                 = (v o (<oal_hgp(s;g), λk,v. inj(k,v), λh,f. umap(h,f)>\000C.inj j))
                                                                 ∈ (|(g↓hgrp)| ⟶ |h|)))))
BY
{ Auto }

1
1. s : LOSet@i'
2. g : OGrp@i'
3. j : |s|@i
⊢ IsMonHom{g↓hgrp,<oal_hgp(s;g), λk,v. inj(k,v), λh,f. umap(h,f)>.mon}(<oal_hgp(s;g), λk,v. inj(k,v), λh,f. umap(h,f)>.i\000Cnj j)

2
1. s : LOSet@i'
2. g : OGrp@i'
3. ∀j:|s|. IsMonHom{g↓hgrp,<oal_hgp(s;g), λk,v. inj(k,v), λh,f. umap(h,f)>.mon}(<oal_hgp(s;g), λk,v. inj(k,v), λh,f. uma\000Cp(h,f)>.inj j)
4. h : AbMon@i'
5. f : |s| ⟶ MonHom(g↓hgrp,h)@i
⊢ (<oal_hgp(s;g), λk,v. inj(k,v), λh,f. umap(h,f)>.umap h f) = !v:|<oal_hgp(s;g), λk,v. inj(k,v), λh,f. umap(h,f)>.mon| \000C⟶ |h|
                                                         (IsMonHom{<oal_hgp(s;g), λk,v. inj(k,v), λh,f. umap(h,f)>.mon,h\000C}(v)
                                                         ∧ (∀j:|s|
                                                              ((f j)
                                                              = (v o (<oal_hgp(s;g), λk,v. inj(k,v), λh,f. umap(h,f)>.in\000Cj j))
                                                              ∈ (|(g↓hgrp)| ⟶ |h|))))

---

Latex:

---

Latex:
.....set  predicate..... 
1.  s  :  LOSet@i'
2.  g  :  OGrp@i'
\mvdash{}  (\mforall{}j:|s|.  IsMonHom\{g\mdownarrow{}hgrp,<oal\_hgp(s;g),  \mlambda{}k,v.  inj(k,v),  \mlambda{}h,f.  umap(h,f)>.mon\}(<oal\_hgp(s;g),  \mlambda{}k,v.\000C  inj(k,v),  \mlambda{}h,f.  umap(h,f)>.inj  j))
\mwedge{}  (\mforall{}h:AbMon.  \mforall{}f:|s|  {}\mrightarrow{}  MonHom(g\mdownarrow{}hgrp,h).
          (<oal\_hgp(s;g),  \mlambda{}k,v.  inj(k,v),  \mlambda{}h,f.  umap(h,f)>.umap  h  f)  =  !v:|<oal\_hgp(s;g)
                                                                                                                            ,  \mlambda{}k,v.  inj(k,v)
                                                                                                                            ,  \mlambda{}h,f.  umap(h,f)>.mon|  {}\mrightarrow{}  |h|
                                                                                                                        (IsMonHom\{<oal\_hgp(s;g)
                                                                                                                                            ,  \mlambda{}k,v.  inj(k,v)
                                                                                                                                            ,  \mlambda{}h,f.  umap(h,f)>.mon,h\}(v)
                                                                                                                        \mwedge{}  (\mforall{}j:|s|
                                                                                                                                  ((f  j)
                                                                                                                                  =  (v  o  (<oal\_hgp(s;g)
                                                                                                                                                  ,  \mlambda{}k,v.  inj(k,v)
                                                                                                                                                  ,  \mlambda{}h,f.  umap(h,f)>.inj 
                                                                                                                                                  j))))))


By

---

Latex:
Auto

---

Home Index