---

Step * 1 1 of Lemma fg-lift_wf


1. X : Type
2. G : Group{i}@i'
3. f : X ⟶ |G|@i
4. a : free-word(X)@i
5. b : free-word(X)@i
⊢ fg-hom(G;f;a + b) = (fg-hom(G;f;a) * fg-hom(G;f;b)) ∈ |G|
BY
{ ((InstLemma `word-equiv-equiv` [⌜X⌝]⋅ THEN Auto) THEN (newQuotientElim (-3) THENA Auto)) }

1
1. X : Type
2. G : Group{i}@i'
3. f : X ⟶ |G|@i
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. b : free-word(X)@i
8. EquivRel((X + X) List;w1,w2.word-equiv(X;w1;w2))
9. w1 : (X + X) List@i
10. w2 : (X + X) List@i
11. word-equiv(X;w1;w2)
12. |G| = |G| ∈ Type
⊢ fg-hom(G;f;w1 + b) = (fg-hom(G;f;w2) * fg-hom(G;f;b)) ∈ |G|

---

Latex:

---

Latex:

1.  X  :  Type
2.  G  :  Group\{i\}@i'
3.  f  :  X  {}\mrightarrow{}  |G|@i
4.  a  :  free-word(X)@i
5.  b  :  free-word(X)@i
\mvdash{}  fg-hom(G;f;a  +  b)  =  (fg-hom(G;f;a)  *  fg-hom(G;f;b))


By

---

Latex:
((InstLemma  `word-equiv-equiv`  [\mkleeneopen{}X\mkleeneclose{}]\mcdot{}  THEN  Auto)  THEN  (newQuotientElim  (-3)  THENA  Auto))

---

Home Index