---

Step * 1 1 1 of Lemma quot_ring_wf


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
⊢ (((∀[x,y,z:Carrier(r/d)].  ((x +r (y +r z)) = ((x +r y) +r z) ∈ Carrier(r/d)))
  ∧ (∀[x:Carrier(r/d)]. (((x +r 0) = x ∈ Carrier(r/d)) ∧ ((0 +r x) = x ∈ Carrier(r/d)))))
  ∧ (∀[x:Carrier(r/d)]. (((x +r (-r x)) = 0 ∈ Carrier(r/d)) ∧ (((-r x) +r x) = 0 ∈ Carrier(r/d)))))
∧ ((∀[x,y,z:Carrier(r/d)].  ((x * (y * z)) = ((x * y) * z) ∈ Carrier(r/d)))
  ∧ (∀[x:Carrier(r/d)]. (((x * 1) = x ∈ Carrier(r/d)) ∧ ((1 * x) = x ∈ Carrier(r/d)))))
∧ (∀[a,x,y:Carrier(r/d)].
     (((a * (x +r y)) = ((a * x) +r (a * y)) ∈ Carrier(r/d)) ∧ (((x +r y) * a) = ((x * a) +r (y * a)) ∈ Carrier(r/d))))
BY
{ (SplitAndConcl
   THEN (UnivCD THENA Auto)
   THEN SplitAndConcl
   THEN Try ((OnVar `x' quotD THENA (Auto THEN RW RngNormC 0 THEN Auto)))
   THEN Try ((OnVar `y' quotD THENA Auto))
   THEN Try ((OnVar `z' quotD THENA Auto))
   THEN Try ((OnVar `a1' quotD THENA Auto))
   THEN EqTypeCD
   THEN Auto
   THEN Try ((UsingVars [`a'] (BLemma `ideal-detach-equiv`)⋅ THEN Auto))
   THEN (RWO "6<" 0 THENA Auto)
   THEN ∀h:hyp. (RWO  "6<" h THENA Auto) 
   THEN RW RngNormC 0
   THEN Auto
   THEN RepeatFor 2 (D 3)
   THEN Auto
   THEN RepUR ``add_grp_of_rng`` 5) }

1
1. r : CRng
2. a : |r| ⟶ ℙ
3. a e
4. ∀a@0:|r↓+gp|. ((a a@0) ⇒ (a (~ a@0)))
5. ∀a@0,b:|r|.  ((a a@0) ⇒ (a b) ⇒ (a (a@0 +r b)))
6. ∀a@0,b:|r|.  ((a a@0) ⇒ (a (a@0 * b)))
7. ∀x:|r|. SqStable(a x)
8. d : |r| ⟶ 𝔹
9. ∀x:|r|. (a x ⇐⇒ a x)
10. Carrier(r/d) ∈ Type
11. r / d ∈ RngSig
12. x : |r|
13. x1 : |r|
14. a (x +r (-r x1))
15. y : |r|
16. y1 : |r|
17. a (y +r (-r y1))
18. z : |r|
19. z1 : |r|
20. a (z +r (-r z1))
⊢ a (x +r ((-r x1) +r (y +r ((-r y1) +r (z +r (-r z1))))))

2
1. r : CRng
2. a : |r| ⟶ ℙ
3. a e
4. ∀a@0:|r↓+gp|. ((a a@0) ⇒ (a (~ a@0)))
5. ∀a@0,b:|r|.  ((a a@0) ⇒ (a b) ⇒ (a (a@0 +r b)))
6. ∀a@0,b:|r|.  ((a a@0) ⇒ (a (a@0 * b)))
7. ∀x:|r|. SqStable(a x)
8. d : |r| ⟶ 𝔹
9. ∀x:|r|. (a x ⇐⇒ a x)
10. Carrier(r/d) ∈ Type
11. r / d ∈ RngSig
12. x : |r|
13. x1 : |r|
14. a (x +r (-r x1))
15. y : |r|
16. y1 : |r|
17. a (y +r (-r y1))
18. z : |r|
19. z1 : |r|
20. a (z +r (-r z1))
⊢ a ((x * (y * z)) +r (-r (x1 * (y1 * z1))))

3
1. r : CRng
2. a : |r| ⟶ ℙ
3. a e
4. ∀a@0:|r↓+gp|. ((a a@0) ⇒ (a (~ a@0)))
5. ∀a@0,b:|r|.  ((a a@0) ⇒ (a b) ⇒ (a (a@0 +r b)))
6. ∀a@0,b:|r|.  ((a a@0) ⇒ (a (a@0 * b)))
7. ∀x:|r|. SqStable(a x)
8. d : |r| ⟶ 𝔹
9. ∀x:|r|. (a x ⇐⇒ a x)
10. Carrier(r/d) ∈ Type
11. r / d ∈ RngSig
12. x : |r|
13. x1 : |r|
14. a (x +r (-r x1))
15. y : |r|
16. y1 : |r|
17. a (y +r (-r y1))
18. a1 : |r|
19. a2 : |r|
20. a (a1 +r (-r a2))
⊢ a ((a1 * x) +r ((a1 * y) +r ((-r (a2 * x1)) +r (-r (a2 * y1)))))

4
1. r : CRng
2. a : |r| ⟶ ℙ
3. a e
4. ∀a@0:|r↓+gp|. ((a a@0) ⇒ (a (~ a@0)))
5. ∀a@0,b:|r|.  ((a a@0) ⇒ (a b) ⇒ (a (a@0 +r b)))
6. ∀a@0,b:|r|.  ((a a@0) ⇒ (a (a@0 * b)))
7. ∀x:|r|. SqStable(a x)
8. d : |r| ⟶ 𝔹
9. ∀x:|r|. (a x ⇐⇒ a x)
10. Carrier(r/d) ∈ Type
11. r / d ∈ RngSig
12. x : |r|
13. x1 : |r|
14. a (x +r (-r x1))
15. y : |r|
16. y1 : |r|
17. a (y +r (-r y1))
18. a1 : |r|
19. a2 : |r|
20. a (a1 +r (-r a2))
⊢ a ((x * a1) +r ((-r (x1 * a2)) +r ((y * a1) +r (-r (y1 * a2)))))

---

Latex:

---

Latex:

1.  r  :  CRng
2.  a  :  |r|  {}\mrightarrow{}  \mBbbP{}
3.  a  Ideal  of  r
4.  \mforall{}x:|r|.  SqStable(a  x)
5.  d  :  |r|  {}\mrightarrow{}  \mBbbB{}
6.  \mforall{}x:|r|.  (a  x  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}(d  x))
7.  Carrier(r/d)  \mmember{}  Type
8.  r  /  d  \mmember{}  RngSig
\mvdash{}  (((\mforall{}[x,y,z:Carrier(r/d)].    ((x  +r  (y  +r  z))  =  ((x  +r  y)  +r  z)))
    \mwedge{}  (\mforall{}[x:Carrier(r/d)].  (((x  +r  0)  =  x)  \mwedge{}  ((0  +r  x)  =  x))))
    \mwedge{}  (\mforall{}[x:Carrier(r/d)].  (((x  +r  (-r  x))  =  0)  \mwedge{}  (((-r  x)  +r  x)  =  0))))
\mwedge{}  ((\mforall{}[x,y,z:Carrier(r/d)].    ((x  *  (y  *  z))  =  ((x  *  y)  *  z)))
    \mwedge{}  (\mforall{}[x:Carrier(r/d)].  (((x  *  1)  =  x)  \mwedge{}  ((1  *  x)  =  x))))
\mwedge{}  (\mforall{}[a,x,y:Carrier(r/d)].
          (((a  *  (x  +r  y))  =  ((a  *  x)  +r  (a  *  y)))  \mwedge{}  (((x  +r  y)  *  a)  =  ((x  *  a)  +r  (y  *  a)))))


By

---

Latex:
(SplitAndConcl
  THEN  (UnivCD  THENA  Auto)
  THEN  SplitAndConcl
  THEN  Try  ((OnVar  `x'  quotD  THENA  (Auto  THEN  RW  RngNormC  0  THEN  Auto)))
  THEN  Try  ((OnVar  `y'  quotD  THENA  Auto))
  THEN  Try  ((OnVar  `z'  quotD  THENA  Auto))
  THEN  Try  ((OnVar  `a1'  quotD  THENA  Auto))
  THEN  EqTypeCD
  THEN  Auto
  THEN  Try  ((UsingVars  [`a']  (BLemma  `ideal-detach-equiv`)\mcdot{}  THEN  Auto))
  THEN  (RWO  "6<"  0  THENA  Auto)
  THEN  \mforall{}h:hyp.  (RWO    "6<"  h  THENA  Auto) 
  THEN  RW  RngNormC  0
  THEN  Auto
  THEN  RepeatFor  2  (D  3)
  THEN  Auto
  THEN  RepUR  ``add\_grp\_of\_rng``  5)

---

Home Index