---

Step * 1 1 1 of Lemma grp_inv_thru_op


1. g : IGroup
2. a : |g|
3. b : |g|
⊢ e = (a * (b * ((~ b) * (~ a)))) ∈ |g|
BY
{ RW (HigherC (GenLemmaC 1 `grp_inv_assoc`) 
    ANDTHENC HigherC GrpInvC) 0 THEN Auto }

---

Latex:

---

Latex:

1.  g  :  IGroup
2.  a  :  |g|
3.  b  :  |g|
\mvdash{}  e  =  (a  *  (b  *  ((\msim{}  b)  *  (\msim{}  a))))


By

---

Latex:
RW  (HigherC  (GenLemmaC  1  `grp\_inv\_assoc`) 
        ANDTHENC  HigherC  GrpInvC)  0  THEN  Auto

---

Home Index