---

Step * 1 of Lemma grp_inv_thru_op


1. g : IGroup
2. a : |g|
3. b : |g|
⊢ ((a * b) * (~ (a * b))) = ((a * b) * ((~ b) * (~ a))) ∈ |g|
BY
{ RWH GrpInvC 0 THENA Auto }

1
1. g : IGroup
2. a : |g|
3. b : |g|
⊢ e = ((a * b) * ((~ b) * (~ a))) ∈ |g|

---

Latex:

---

Latex:

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


By

---

Latex:
RWH  GrpInvC  0  THENA  Auto

---

Home Index