---

Step * of Lemma quot_ring_sig

∀[r:CRng]. ∀[a:Ideal(r){i}].  ((∀x:|r|. SqStable(a x)) ⇒ (∀[d:detach_fun(|r|;a)]. (r / d ∈ RngSig)))
BY
{ (Auto
   THEN DVar `a'
   THEN (DVar `d' THENA Auto)
   THEN (InstLemma `quot_ring_car_wf` [⌜r⌝;⌜a⌝;⌜d⌝]⋅ THENA Auto)
   THEN Unfold `quot_ring` 0
   THEN Unfold `rng_sig` 0
   THEN Repeat ((MemCD THENL [Id; Id; Complete (Auto)]))) }

1
.....subterm..... T:t
1:n
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
⊢ Carrier(r/d) ∈ Type

2
.....subterm..... T:t
1:n
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
⊢ λx,y. (d (x +r (-r y))) ∈ Carrier(r/d) ⟶ Carrier(r/d) ⟶ 𝔹

3
.....subterm..... T:t
1:n
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
⊢ λx,y. tt ∈ Carrier(r/d) ⟶ Carrier(r/d) ⟶ 𝔹

4
.....subterm..... T:t
1:n
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
⊢ λx,y. (x +r y) ∈ Carrier(r/d) ⟶ Carrier(r/d) ⟶ Carrier(r/d)

5
.....subterm..... T:t
1:n
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
⊢ 0 ∈ Carrier(r/d)

6
.....subterm..... T:t
1:n
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
⊢ λx.(-r x) ∈ Carrier(r/d) ⟶ Carrier(r/d)

7
.....subterm..... T:t
1:n
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
⊢ λx,y. (x * y) ∈ Carrier(r/d) ⟶ Carrier(r/d) ⟶ Carrier(r/d)

8
.....subterm..... T:t
1:n
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
⊢ 1 ∈ Carrier(r/d)

9
.....subterm..... T:t
2:n
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
⊢ λx,y. (inr ⋅ ) ∈ Carrier(r/d) ⟶ Carrier(r/d) ⟶ (Carrier(r/d)?)

---

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{}  RngSig)))


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  Unfold  `quot\_ring`  0
  THEN  Unfold  `rng\_sig`  0
  THEN  Repeat  ((MemCD  THENL  [Id;  Id;  Complete  (Auto)])))

---

Home Index