---

Step * 1 1 1 1 1 of Lemma omral_alg_umap_unique


1. g : OCMon
2. a : CDRng
3. n : algebra{i:l}(a)
4. f : |g| ⟶ n.car
5. f' : algebra_hom(a; omral_alg(g;a); n)
6. ∀[a1,a2:omral_alg(g;a).car].  ((f' (a1 omral_alg(g;a).plus a2)) = ((f' a1) n.plus (f' a2)) ∈ n.car)
7. ∀u:|a|. fun_thru_1op(omral_alg(g;a).car;n.car;omral_alg(g;a).act u;n.act u;f')
8. ∀[a1,a2:omral_alg(g;a).car].  ((f' (a1 omral_alg(g;a).times a2)) = ((f' a1) n.times (f' a2)) ∈ n.car)
9. (f' omral_alg(g;a).one) = n.one ∈ n.car
10. (f' o (λk:|g|. inj(k,1))) = f ∈ (|g| ⟶ n.car)
11. ps : |omral(g;a)|
⊢ f' ∈ |(omral_alg(g;a)↓grp)| ⟶ |(n↓grp)|
BY
{ Auto }

---

Latex:

---

Latex:

1.  g  :  OCMon
2.  a  :  CDRng
3.  n  :  algebra\{i:l\}(a)
4.  f  :  |g|  {}\mrightarrow{}  n.car
5.  f'  :  algebra\_hom(a;  omral\_alg(g;a);  n)
6.  \mforall{}[a1,a2:omral\_alg(g;a).car].    ((f'  (a1  omral\_alg(g;a).plus  a2))  =  ((f'  a1)  n.plus  (f'  a2)))
7.  \mforall{}u:|a|.  fun\_thru\_1op(omral\_alg(g;a).car;n.car;omral\_alg(g;a).act  u;n.act  u;f')
8.  \mforall{}[a1,a2:omral\_alg(g;a).car].    ((f'  (a1  omral\_alg(g;a).times  a2))  =  ((f'  a1)  n.times  (f'  a2)))
9.  (f'  omral\_alg(g;a).one)  =  n.one
10.  (f'  o  (\mlambda{}k:|g|.  inj(k,1)))  =  f
11.  ps  :  |omral(g;a)|
\mvdash{}  f'  \mmember{}  |(omral\_alg(g;a)\mdownarrow{}grp)|  {}\mrightarrow{}  |(n\mdownarrow{}grp)|


By

---

Latex:
Auto

---

Home Index