---

Step * of Lemma mon_when_hom_swap

∀[g,h:GrpSig]. ∀[f:MonHom(g,h)]. ∀[b:𝔹]. ∀[p:|g|].  ((when b. (f p)) = (f (when b. p)) ∈ |h|)
BY
{ ((RepD 
THENM Unfold `mon_when` 0 
THENM SplitOnConclITE) THENA Auto) }

1
.....truecase..... 
1. g : GrpSig
2. h : GrpSig
3. f : MonHom(g,h)
4. b : 𝔹
5. p : |g|
6. ↑b
⊢ (f p) = (f p) ∈ |h|

2
.....falsecase..... 
1. g : GrpSig
2. h : GrpSig
3. f : MonHom(g,h)
4. b : 𝔹
5. p : |g|
6. ¬↑b
⊢ e = (f e) ∈ |h|

---

Latex:

---

Latex:
\mforall{}[g,h:GrpSig].  \mforall{}[f:MonHom(g,h)].  \mforall{}[b:\mBbbB{}].  \mforall{}[p:|g|].    ((when  b.  (f  p))  =  (f  (when  b.  p)))


By

---

Latex:
((RepD 
THENM  Unfold  `mon\_when`  0 
THENM  SplitOnConclITE)  THENA  Auto)

---

Home Index