---

Step * 1 of Lemma inverse_grp_sig_hom_shift


1. g : GrpSig
2. h : GrpSig
3. f : MonHom(g,h)
4. ∀[a1,a2:|g|].  ((f (a1 * a2)) = ((f a1) * (f a2)) ∈ |h|)
5. (f e) = e ∈ |h|
6. ∀[a:|g|]. ((f (~ a)) = (~ (f a)) ∈ |h|)
7. ∀a1,a2:|g|.  (((f a1) = (f a2) ∈ |h|) ⇒ (a1 = a2 ∈ |g|))
8. ∀[x:|h|]. (((x * (~ x)) = e ∈ |h|) ∧ (((~ x) * x) = e ∈ |h|))
9. x : |g|
⊢ ((x * (~ x)) = e ∈ |g|) ∧ (((~ x) * x) = e ∈ |g|)
BY
{ ((D 0  
THENM BHyp 7 
THENM RWW "4 5 6" 0 
THENM BHyp 8) THENA Auto) }

---

Latex:

---

Latex:

1.  g  :  GrpSig
2.  h  :  GrpSig
3.  f  :  MonHom(g,h)
4.  \mforall{}[a1,a2:|g|].    ((f  (a1  *  a2))  =  ((f  a1)  *  (f  a2)))
5.  (f  e)  =  e
6.  \mforall{}[a:|g|].  ((f  (\msim{}  a))  =  (\msim{}  (f  a)))
7.  \mforall{}a1,a2:|g|.    (((f  a1)  =  (f  a2))  {}\mRightarrow{}  (a1  =  a2))
8.  \mforall{}[x:|h|].  (((x  *  (\msim{}  x))  =  e)  \mwedge{}  (((\msim{}  x)  *  x)  =  e))
9.  x  :  |g|
\mvdash{}  ((x  *  (\msim{}  x))  =  e)  \mwedge{}  (((\msim{}  x)  *  x)  =  e)


By

---

Latex:
((D  0   
THENM  BHyp  7 
THENM  RWW  "4  5  6"  0 
THENM  BHyp  8)  THENA  Auto)

---

Home Index