---

Step * of Lemma inverse_grp_sig_hom_shift

∀[g,h:GrpSig]. ∀[f:MonHom(g,h)].
  (Inverse(|g|;*;e;~)) supposing (Inverse(|h|;*;e;~) and Inj(|g|;|h|;f) and fun_thru_1op(|g|;|h|;~;~;f))
BY
{ ((RepD THENM OnVar `f' AddProperties 
THENM ARepD ["compound";"basic"]) THENA Auto) }

1
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|)

---

Latex:

---

Latex:
\mforall{}[g,h:GrpSig].  \mforall{}[f:MonHom(g,h)].
    (Inverse(|g|;*;e;\msim{}))  supposing 
          (Inverse(|h|;*;e;\msim{})  and 
          Inj(|g|;|h|;f)  and 
          fun\_thru\_1op(|g|;|h|;\msim{};\msim{};f))


By

---

Latex:
((RepD  THENM  OnVar  `f'  AddProperties 
THENM  ARepD  ["compound";"basic"])  THENA  Auto)

---

Home Index