---

Step * of Lemma quot_ring_wf

∀[r:CRng]. ∀[a:Ideal(r){i}].  ((∀x:|r|. SqStable(a x)) ⇒ (∀[d:detach_fun(|r|;a)]. (r / d ∈ CRng)))
BY
{ (Auto
   THEN DVar `a'
   THEN (DVar `d' THENA Auto)
   THEN (InstLemma `quot_ring_car_wf` [⌜r⌝;⌜a⌝;⌜d⌝]⋅ THENA Auto)
   THEN (InstLemma `quot_ring_sig` [⌜r⌝;⌜a⌝;⌜d⌝]⋅ THENA Auto)) }

1
1. r : CRng
2. a : |r| ⟶ ℙ
3. a Ideal of r
4. ∀x:|r|. SqStable(a x)
5. d : |r| ⟶ 𝔹
6. ∀x:|r|. (a x ⇐⇒ ↑(d x))
7. Carrier(r/d) ∈ Type
8. r / d ∈ RngSig
⊢ r / d ∈ CRng

---

Latex:

---

Latex:
\mforall{}[r:CRng].  \mforall{}[a:Ideal(r)\{i\}].    ((\mforall{}x:|r|.  SqStable(a  x))  {}\mRightarrow{}  (\mforall{}[d:detach\_fun(|r|;a)].  (r  /  d  \mmember{}  CRng)))


By

---

Latex:
(Auto
  THEN  DVar  `a'
  THEN  (DVar  `d'  THENA  Auto)
  THEN  (InstLemma  `quot\_ring\_car\_wf`  [\mkleeneopen{}r\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `quot\_ring\_sig`  [\mkleeneopen{}r\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index