---

Step * 1 1 1 2 1 of Lemma quot_grp_inv_wf


1. g : IGroup
2. h : |g| ⟶ ℙ
3. h e
4. ∀a:|g|. ((h a) ⇒ (h (~ a)))
5. ∀a,b:|g|.  ((h a) ⇒ (h b) ⇒ (h (a * b)))
6. ∀a,b:|g|.  ((h b) ⇒ (h ((~ a) * (b * a))))
7. v : |g|
8. v1 : |g|
9. h (v * (~ v1))
⊢ h ((~ v) * (~ (~ v1)))
BY
{ (FHyp 4 [-1] THENA Auto) }

1
1. g : IGroup
2. h : |g| ⟶ ℙ
3. h e
4. ∀a:|g|. ((h a) ⇒ (h (~ a)))
5. ∀a,b:|g|.  ((h a) ⇒ (h b) ⇒ (h (a * b)))
6. ∀a,b:|g|.  ((h b) ⇒ (h ((~ a) * (b * a))))
7. v : |g|
8. v1 : |g|
9. h (v * (~ v1))
10. h (~ (v * (~ v1)))
⊢ h ((~ v) * (~ (~ v1)))

---

Latex:

---

Latex:

1.  g  :  IGroup
2.  h  :  |g|  {}\mrightarrow{}  \mBbbP{}
3.  h  e
4.  \mforall{}a:|g|.  ((h  a)  {}\mRightarrow{}  (h  (\msim{}  a)))
5.  \mforall{}a,b:|g|.    ((h  a)  {}\mRightarrow{}  (h  b)  {}\mRightarrow{}  (h  (a  *  b)))
6.  \mforall{}a,b:|g|.    ((h  b)  {}\mRightarrow{}  (h  ((\msim{}  a)  *  (b  *  a))))
7.  v  :  |g|
8.  v1  :  |g|
9.  h  (v  *  (\msim{}  v1))
\mvdash{}  h  ((\msim{}  v)  *  (\msim{}  (\msim{}  v1)))


By

---

Latex:
(FHyp  4  [-1]  THENA  Auto)

---

Home Index