---

Step * 1 of Lemma mon_nat_op_hom_swap


1. g : IMonoid
2. h : IMonoid
3. f : MonHom(g,h)
4. n : ℕ
5. u : |g|
⊢ (n ⋅ (f u)) = (f (n ⋅ u)) ∈ |h|
BY
{ ((AddProperties 3 
THENM ARepD ["compound";"basic"] THENM OnVar `n' NatInd) THENA Auto) }

1
.....basecase..... 
1. g : IMonoid
2. h : IMonoid
3. f : MonHom(g,h)
4. ∀[a1,a2:|g|].  ((f (a1 * a2)) = ((f a1) * (f a2)) ∈ |h|)
5. (f e) = e ∈ |h|
6. n : ℤ
7. u : |g|
⊢ (0 ⋅ (f u)) = (f (0 ⋅ u)) ∈ |h|

2
.....upcase..... 
1. g : IMonoid
2. h : IMonoid
3. f : MonHom(g,h)
4. ∀[a1,a2:|g|].  ((f (a1 * a2)) = ((f a1) * (f a2)) ∈ |h|)
5. (f e) = e ∈ |h|
6. u : |g|
7. n : ℤ
8. 0 < n
9. ((n - 1) ⋅ (f u)) = (f ((n - 1) ⋅ u)) ∈ |h|
⊢ (n ⋅ (f u)) = (f (n ⋅ u)) ∈ |h|

---

Latex:

---

Latex:

1.  g  :  IMonoid
2.  h  :  IMonoid
3.  f  :  MonHom(g,h)
4.  n  :  \mBbbN{}
5.  u  :  |g|
\mvdash{}  (n  \mcdot{}  (f  u))  =  (f  (n  \mcdot{}  u))


By

---

Latex:
((AddProperties  3 
THENM  ARepD  ["compound";"basic"]  THENM  OnVar  `n'  NatInd)  THENA  Auto)

---

Home Index