---

Step * of Lemma iabgrp_op_inv_assoc

∀[g:IAbGrp{i}]. ∀[a,b:|g|].  (((a * ((~ a) * b)) = b ∈ |g|) ∧ (((~ a) * (a * b)) = b ∈ |g|))
BY
{ (((RepD) THENA Auto)
   THEN ((RWH (LemmaC `mon_assoc`) 0 
   THENM RWW "grp_inverse.1 grp_inverse.2" 0) THENA Auto)
   THEN Auto
   THEN ((RW GrpNormC 0) THEN Auto)) }

---

Latex:

---

Latex:
\mforall{}[g:IAbGrp\{i\}].  \mforall{}[a,b:|g|].    (((a  *  ((\msim{}  a)  *  b))  =  b)  \mwedge{}  (((\msim{}  a)  *  (a  *  b))  =  b))


By

---

Latex:
(((RepD)  THENA  Auto)
  THEN  ((RWH  (LemmaC  `mon\_assoc`)  0 
  THENM  RWW  "grp\_inverse.1  grp\_inverse.2"  0)  THENA  Auto)
  THEN  Auto
  THEN  ((RW  GrpNormC  0)  THEN  Auto))

---

Home Index