---

Step * 1 1 1 1 2 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)|
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
BY
{ ((Unfold `fun_thru_1op` 7 
THENM HypBackchain) THEN 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)|
12.  u  :  |a|
13.  a@0  :  omral\_alg(g;a).car
\mvdash{}  (f'  (omral\_alg(g;a).act  u  a@0))  =  (n.act  u  (f'  a@0))


By

---

Latex:
((Unfold  `fun\_thru\_1op`  7 
THENM  HypBackchain)  THEN  Auto)\mcdot{}

---

Home Index