---

Step * 1 of Lemma grp_eq_shift_right


1. g : IGroup
2. a : |g|
3. b : |g|
⊢ uiff(a = b ∈ |g|;e = (b * (~ a)) ∈ |g|)
BY
{ ((RWN 2 (LemmaWithC [`c',a] `grp_eq_op_r`) 0 
THENM RW GrpNormC 0) THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
((RWN  2  (LemmaWithC  [`c',a]  `grp\_eq\_op\_r`)  0 
THENM  RW  GrpNormC  0)  THEN  Auto)

---

Home Index