---

Step * of Lemma int_op_wf

∀[g:Group{i}]. ∀[a:ℤ]. ∀[e:|g|].  (a x(*;e;~) e ∈ |g|)
BY
{ Unfold `int_op` 0 THEN UnivCD THENA Auto }

1
1. g : Group{i}
2. a : ℤ
3. e : |g|
⊢ if 0 ≤z a then a x(*;e) e else ~ -a x(*;e) e fi  ∈ |g|

---

Latex:

---

Latex:
\mforall{}[g:Group\{i\}].  \mforall{}[a:\mBbbZ{}].  \mforall{}[e:|g|].    (a  x(*;e;\msim{})  e  \mmember{}  |g|)


By

---

Latex:
Unfold  `int\_op`  0  THEN  UnivCD  THENA  Auto

---

Home Index