---

Step * 2 of Lemma fg-hom_wf


1. X : Type
2. G : Group{i}
3. f : X ⟶ |G|
4. w : free-word(X)
5. ∀w2,w:(X + X) List.  ((λx,y. word-rel(X;x;y)^* w2 w) ⇒ (fg-hom(G;f;w2) = fg-hom(G;f;w) ∈ |G|))
⊢ fg-hom(G;f;w) ∈ |G|
BY
{ ((newQuotientElim (-2) THENA Auto)
   THEN InstLemma `word-equiv-equiv` [⌜X⌝]⋅
   THEN Auto
   THEN RepeatFor 2 (Thin (-1))
   THEN D -1
   THEN ExRepD) }

1
1. X : Type
2. G : Group{i}
3. f : X ⟶ |G|
4. (X + X) List ∈ Type
5. ∀w1,w2:(X + X) List.  (word-equiv(X;w1;w2) ∈ Type)
6. ∀w1:(X + X) List. word-equiv(X;w1;w1)
7. ∀w2,w:(X + X) List.  ((λx,y. word-rel(X;x;y)^* w2 w) ⇒ (fg-hom(G;f;w2) = fg-hom(G;f;w) ∈ |G|))
8. w1 : (X + X) List@i
9. w2 : (X + X) List@i
10. w : (X + X) List@i
11. λx,y. word-rel(X;x;y)^* w1 w
12. λx,y. word-rel(X;x;y)^* w2 w
⊢ fg-hom(G;f;w1) = fg-hom(G;f;w2) ∈ |G|

---

Latex:

---

Latex:

1.  X  :  Type
2.  G  :  Group\{i\}
3.  f  :  X  {}\mrightarrow{}  |G|
4.  w  :  free-word(X)
5.  \mforall{}w2,w:(X  +  X)  List.    ((\mlambda{}x,y.  word-rel(X;x;y)\^{}*  w2  w)  {}\mRightarrow{}  (fg-hom(G;f;w2)  =  fg-hom(G;f;w)))
\mvdash{}  fg-hom(G;f;w)  \mmember{}  |G|


By

---

Latex:
((newQuotientElim  (-2)  THENA  Auto)
  THEN  InstLemma  `word-equiv-equiv`  [\mkleeneopen{}X\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  RepeatFor  2  (Thin  (-1))
  THEN  D  -1
  THEN  ExRepD)

---

Home Index