---

Step * 1 2 1 1 1 1 of Lemma fg-hom_wf


1. X : Type
2. G : Group{i}
3. f : X ⟶ |G|
4. w : free-word(X)
5. w2 : (X + X) List@i
6. w3 : (X + X) List@i
7. TC(λx,y. word-rel(X;x;y)) w2 w3
8. ∀x:(X + X) List. (fg-hom(G;f;x) ∈ |G|)
9. x : (X + X) List@i
10. y : (X + X) List@i
11. x@0 : X + X@i
12. y@0 : X + X@i
13. a : (X + X) List@i
14. b : (X + X) List@i
15. x@0 = -y@0
16. x = (a @ [x@0; y@0] @ b) ∈ ((X + X) List)
17. y = (a @ b) ∈ ((X + X) List)
⊢ (fg-hom(G;f;a) * (fg-hom(G;f;[x@0; y@0]) * fg-hom(G;f;b))) = (fg-hom(G;f;a) * fg-hom(G;f;b)) ∈ |G|
BY
{ (Subst' fg-hom(G;f;[x@0; y@0]) = e ∈ |G| 0 THEN Auto) }

1
.....equality..... 
1. X : Type
2. G : Group{i}
3. f : X ⟶ |G|
4. w : free-word(X)
5. w2 : (X + X) List@i
6. w3 : (X + X) List@i
7. TC(λx,y. word-rel(X;x;y)) w2 w3
8. ∀x:(X + X) List. (fg-hom(G;f;x) ∈ |G|)
9. x : (X + X) List@i
10. y : (X + X) List@i
11. x@0 : X + X@i
12. y@0 : X + X@i
13. a : (X + X) List@i
14. b : (X + X) List@i
15. x@0 = -y@0
16. x = (a @ [x@0; y@0] @ b) ∈ ((X + X) List)
17. y = (a @ b) ∈ ((X + X) List)
⊢ fg-hom(G;f;[x@0; y@0]) = e ∈ |G|

2
1. X : Type
2. G : Group{i}
3. f : X ⟶ |G|
4. w : free-word(X)
5. w2 : (X + X) List@i
6. w3 : (X + X) List@i
7. TC(λx,y. word-rel(X;x;y)) w2 w3
8. ∀x:(X + X) List. (fg-hom(G;f;x) ∈ |G|)
9. x : (X + X) List@i
10. y : (X + X) List@i
11. x@0 : X + X@i
12. y@0 : X + X@i
13. a : (X + X) List@i
14. b : (X + X) List@i
15. x@0 = -y@0
16. x = (a @ [x@0; y@0] @ b) ∈ ((X + X) List)
17. y = (a @ b) ∈ ((X + X) List)
⊢ (fg-hom(G;f;a) * (e * fg-hom(G;f;b))) = (fg-hom(G;f;a) * fg-hom(G;f;b)) ∈ |G|

---

Latex:

---

Latex:

1.  X  :  Type
2.  G  :  Group\{i\}
3.  f  :  X  {}\mrightarrow{}  |G|
4.  w  :  free-word(X)
5.  w2  :  (X  +  X)  List@i
6.  w3  :  (X  +  X)  List@i
7.  TC(\mlambda{}x,y.  word-rel(X;x;y))  w2  w3
8.  \mforall{}x:(X  +  X)  List.  (fg-hom(G;f;x)  \mmember{}  |G|)
9.  x  :  (X  +  X)  List@i
10.  y  :  (X  +  X)  List@i
11.  x@0  :  X  +  X@i
12.  y@0  :  X  +  X@i
13.  a  :  (X  +  X)  List@i
14.  b  :  (X  +  X)  List@i
15.  x@0  =  -y@0
16.  x  =  (a  @  [x@0;  y@0]  @  b)
17.  y  =  (a  @  b)
\mvdash{}  (fg-hom(G;f;a)  *  (fg-hom(G;f;[x@0;  y@0])  *  fg-hom(G;f;b)))  =  (fg-hom(G;f;a)  *  fg-hom(G;f;b))


By

---

Latex:
(Subst'  fg-hom(G;f;[x@0;  y@0])  =  e  0  THEN  Auto)

---

Home Index