---

Step * 1 1 1 2 of Lemma quot_grp_inv_wf

.....antecedent..... 
1. g : IGroup
2. h : |g| ⟶ ℙ
3. h SubGrp of g
4. norm_subset_p(g;h)
5. v : |g|
6. v1 : |g|
7. v ≡ v1 (mod h in g)
⊢ ~ v ≡ ~ v1 (mod h in g)
BY
{ (UnfoldTopAb (-1) THEN UnfoldTopAb 0 THEN (UnfoldTopAb 3 THEN UnfoldTopAb 4) THEN Auto) }

1
1. g : IGroup
2. h : |g| ⟶ ℙ
3. h e
4. ∀a:|g|. ((h a) ⇒ (h (~ a)))
5. ∀a,b:|g|.  ((h a) ⇒ (h b) ⇒ (h (a * b)))
6. ∀a,b:|g|.  ((h b) ⇒ (h ((~ a) * (b * a))))
7. v : |g|
8. v1 : |g|
9. h (v * (~ v1))
⊢ h ((~ v) * (~ (~ v1)))

---

Latex:

---

Latex:
.....antecedent..... 
1.  g  :  IGroup
2.  h  :  |g|  {}\mrightarrow{}  \mBbbP{}
3.  h  SubGrp  of  g
4.  norm\_subset\_p(g;h)
5.  v  :  |g|
6.  v1  :  |g|
7.  v  \mequiv{}  v1  (mod  h  in  g)
\mvdash{}  \msim{}  v  \mequiv{}  \msim{}  v1  (mod  h  in  g)


By

---

Latex:
(UnfoldTopAb  (-1)  THEN  UnfoldTopAb  0  THEN  (UnfoldTopAb  3  THEN  UnfoldTopAb  4)  THEN  Auto)

---

Home Index