---

Step * 2 of Lemma omral_fma_wf2


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)))
BY
{ ((Unfold `uni_sat` 0 THEN GenRepD 
THENM All (\i.Force `5` (Reduce i))) THENA Auto) }

1
1. g : OCMon
2. a : CDRng
3. IsMonHom{g,omral_alg(g;a)↓rg↓xmn}(λk.inj(k,1))
4. n : algebra{i:l}(a)
5. f : MonHom(g,n↓rg↓xmn)
⊢ alg_hom_p(a; omral_alg(g;a); n; alg_umap(n,f))

2
1. g : OCMon
2. a : CDRng
3. IsMonHom{g,omral_alg(g;a)↓rg↓xmn}(λk.inj(k,1))
4. n : algebra{i:l}(a)
5. f : MonHom(g,n↓rg↓xmn)
⊢ (alg_umap(n,f) o (λk.inj(k,1))) = f ∈ (|g| ⟶ n.car)

3
1. g : OCMon
2. a : CDRng
3. IsMonHom{g,omral_alg(g;a)↓rg↓xmn}(λk.inj(k,1))
4. n : algebra{i:l}(a)
5. f : MonHom(g,n↓rg↓xmn)
6. a' : |omral(g;a)| ⟶ n.car
7. alg_hom_p(a; omral_alg(g;a); n; a')
8. (a' o (λk.inj(k,1))) = f ∈ (|g| ⟶ n.car)
⊢ a' = alg_umap(n,f) ∈ (|omral(g;a)| ⟶ n.car)

---

Latex:

---

Latex:

1.  g  :  OCMon
2.  a  :  CDRng
3.  IsMonHom\{g,omral\_fma(g;a).alg\mdownarrow{}rg\mdownarrow{}xmn\}(omral\_fma(g;a).inj)
4.  n  :  algebra\{i:l\}(a)
5.  f  :  MonHom(g,n\mdownarrow{}rg\mdownarrow{}xmn)
\mvdash{}  (omral\_fma(g;a).umap  n  f)  =  !f':omral\_fma(g;a).alg.car  {}\mrightarrow{}  n.car
                                                                (alg\_hom\_p(a;  omral\_fma(g;a).alg;  n;  f')
                                                                \mwedge{}  ((f'  o  omral\_fma(g;a).inj)  =  f))


By

---

Latex:
((Unfold  `uni\_sat`  0  THEN  GenRepD 
THENM  All  (\mbackslash{}i.Force  `5`  (Reduce  i)))  THENA  Auto)

---

Home Index