---

Step * of Lemma nsgrp_of_ideal_wf

∀[r:CRng]. ∀[a:Ideal(r){i}].  (a↓+nsgp ∈ NormSubGrp{i}(r↓+gp))
BY
{ (Auto THEN DVar `a'⋅ THEN MemTypeCD THEN Try (Complete (ProveWfLemma)) THEN Auto) }

1
1. r : CRng
2. a : |r| ⟶ ℙ
3. a Ideal of r
⊢ a↓+nsgp SubGrp of r↓+gp

2
1. r : CRng
2. a : |r| ⟶ ℙ
3. a Ideal of r
4. a↓+nsgp SubGrp of r↓+gp
⊢ norm_subset_p(r↓+gp;a↓+nsgp)

---

Latex:

---

Latex:
\mforall{}[r:CRng].  \mforall{}[a:Ideal(r)\{i\}].    (a\mdownarrow{}+nsgp  \mmember{}  NormSubGrp\{i\}(r\mdownarrow{}+gp))


By

---

Latex:
(Auto  THEN  DVar  `a'\mcdot{}  THEN  MemTypeCD  THEN  Try  (Complete  (ProveWfLemma))  THEN  Auto)

---

Home Index