---

Step * of Lemma mon_hom_p_comp

∀[g,h,k:GrpSig]. ∀[r:|g| ⟶ |h|]. ∀[s:|h| ⟶ |k|].
  (IsMonHom{g,k}(s o r)) supposing (IsMonHom{h,k}(s) and IsMonHom{g,h}(r))
BY
{ ((Eval ``monoid_hom_p fun_thru_2op`` 0 
THENM GenRepD) THENA Auto) }

1
1. g : GrpSig
2. h : GrpSig
3. k : GrpSig
4. r : |g| ⟶ |h|
5. s : |h| ⟶ |k|
6. ∀[a1,a2:|g|].  ((r (a1 * a2)) = ((r a1) * (r a2)) ∈ |h|)
7. (r e) = e ∈ |h|
8. ∀[a1,a2:|h|].  ((s (a1 * a2)) = ((s a1) * (s a2)) ∈ |k|)
9. (s e) = e ∈ |k|
10. a1 : |g|
11. a2 : |g|
⊢ (s (r (a1 * a2))) = ((s (r a1)) * (s (r a2))) ∈ |k|

2
1. g : GrpSig
2. h : GrpSig
3. k : GrpSig
4. r : |g| ⟶ |h|
5. s : |h| ⟶ |k|
6. ∀[a1,a2:|g|].  ((r (a1 * a2)) = ((r a1) * (r a2)) ∈ |h|)
7. (r e) = e ∈ |h|
8. ∀[a1,a2:|h|].  ((s (a1 * a2)) = ((s a1) * (s a2)) ∈ |k|)
9. (s e) = e ∈ |k|
⊢ (s (r e)) = e ∈ |k|

---

Latex:

---

Latex:
\mforall{}[g,h,k:GrpSig].  \mforall{}[r:|g|  {}\mrightarrow{}  |h|].  \mforall{}[s:|h|  {}\mrightarrow{}  |k|].
    (IsMonHom\{g,k\}(s  o  r))  supposing  (IsMonHom\{h,k\}(s)  and  IsMonHom\{g,h\}(r))


By

---

Latex:
((Eval  ``monoid\_hom\_p  fun\_thru\_2op``  0 
THENM  GenRepD)  THENA  Auto)

---

Home Index