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