---

Step * 1 of Lemma grp_inv_assoc


1. g : IGroup
2. a : |g|
3. b : |g|
⊢ ((a * ((~ a) * b)) = b ∈ |g|) ∧ (((~ a) * (a * b)) = b ∈ |g|)
BY
{ (Auto
   THEN RW 
          (HigherC (LemmaC `mon_assoc`) 
           ANDTHENC HigherC GrpInverseC 
           ANDTHENC HigherC MonIdentC 
          ) 0 
        THEN Auto
   ) }

---

Latex:

---

Latex:

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


By

---

Latex:
(Auto
  THEN  RW 
                (HigherC  (LemmaC  `mon\_assoc`) 
                  ANDTHENC  HigherC  GrpInverseC 
                  ANDTHENC  HigherC  MonIdentC 
                )  0 
            THEN  Auto
  )

---

Home Index