---

Step * 1 1 1 1 of Lemma omral_alg_umap_unique

.....wf..... 
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. (f' o (λk:|g|. inj(k,1))) = f ∈ (|g| ⟶ n.car)
7. ps : |omral(g;a)|
⊢ f' ∈ MonHom(omral_alg(g;a)↓grp,n↓grp)
BY
{ ((AddAllProperties 5 
THENM MemTypeCD 
THEN IfLabL [`set predicate`, 
  BLemma `module_hom_is_grp_hom`] 
THENM AGenRepD ["compound";"basic"] 
THENM HypBackchain) THENA Auto)⋅ }

1
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)|

2
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)|
12. u : |a|
13. a@0 : omral_alg(g;a).car
⊢ (f' (omral_alg(g;a).act u a@0)) = (n.act u (f' a@0)) ∈ n.car

---

Latex:

---

Latex:
.....wf..... 
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.  (f'  o  (\mlambda{}k:|g|.  inj(k,1)))  =  f
7.  ps  :  |omral(g;a)|
\mvdash{}  f'  \mmember{}  MonHom(omral\_alg(g;a)\mdownarrow{}grp,n\mdownarrow{}grp)


By

---

Latex:
((AddAllProperties  5 
THENM  MemTypeCD 
THEN  IfLabL  [`set  predicate`, 
    BLemma  `module\_hom\_is\_grp\_hom`] 
THENM  AGenRepD  ["compound";"basic"] 
THENM  HypBackchain)  THENA  Auto)\mcdot{}

---

Home Index