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