---

Step * of Lemma mon_when_thru_op

∀[g:IMonoid]. ∀[b:𝔹]. ∀[p,q:|g|].  ((when b. (p * q)) = ((when b. p) * (when b. q)) ∈ |g|)
BY
{ ((RepD THENM Unfold `mon_when` 0 
THENM OnVar `b' BoolCases THENM AbReduce 0) THENA Auto) }

1
1. g : IMonoid
2. p : |g|
3. q : |g|
⊢ (p * q) = (p * q) ∈ |g|

2
1. g : IMonoid
2. p : |g|
3. q : |g|
⊢ e = (e * e) ∈ |g|

---

Latex:

---

Latex:
\mforall{}[g:IMonoid].  \mforall{}[b:\mBbbB{}].  \mforall{}[p,q:|g|].    ((when  b.  (p  *  q))  =  ((when  b.  p)  *  (when  b.  q)))


By

---

Latex:
((RepD  THENM  Unfold  `mon\_when`  0 
THENM  OnVar  `b'  BoolCases  THENM  AbReduce  0)  THENA  Auto)

---

Home Index