---

Step * of Lemma grp_inv_thru_op

∀[g:IGroup]. ∀[a,b:|g|].  ((~ (a * b)) = ((~ b) * (~ a)) ∈ |g|)
BY
{ UnivCD  
THENM Using [`a',a * b] 
 (BackThruLemma `grp_op_cancel_l`) THENA Auto }

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

---

Latex:

---

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


By

---

Latex:
UnivCD   
THENM  Using  [`a',a  *  b] 
  (BackThruLemma  `grp\_op\_cancel\_l`)  THENA  Auto

---

Home Index