---

Step * 1 2 of Lemma real-ring_wf

.....set predicate..... 
1. λx,y. (x + y) ∈ (x,y:ℝ//(x = y)) ⟶ (x,y:ℝ//(x = y)) ⟶ (x,y:ℝ//(x = y))
2. λx,y. (x * y) ∈ (x,y:ℝ//(x = y)) ⟶ (x,y:ℝ//(x = y)) ⟶ (x,y:ℝ//(x = y))
3. λx.-(x) ∈ (x,y:ℝ//(x = y)) ⟶ (x,y:ℝ//(x = y))
⊢ IsRing(|real-ring()|;+real-ring();0;-real-ring();*;1)
BY
{ (RepUR ``ring_p group_p monoid_p bilinear assoc ident inverse `` 0
   THEN Auto
   THEN Try (DVar `x')
   THEN Try (DVar `y')
   THEN Try (DVar `z')
   THEN Try (DVar `a')
   THEN EqTypeCD
   THEN Auto
   THEN ∀h:hyp. (RW (SweepUpC (HypC h)) 0 THENA Complete (Auto)) 
   THEN Auto) }

---

Latex:

---

Latex:
.....set  predicate..... 
1.  \mlambda{}x,y.  (x  +  y)  \mmember{}  (x,y:\mBbbR{}//(x  =  y))  {}\mrightarrow{}  (x,y:\mBbbR{}//(x  =  y))  {}\mrightarrow{}  (x,y:\mBbbR{}//(x  =  y))
2.  \mlambda{}x,y.  (x  *  y)  \mmember{}  (x,y:\mBbbR{}//(x  =  y))  {}\mrightarrow{}  (x,y:\mBbbR{}//(x  =  y))  {}\mrightarrow{}  (x,y:\mBbbR{}//(x  =  y))
3.  \mlambda{}x.-(x)  \mmember{}  (x,y:\mBbbR{}//(x  =  y))  {}\mrightarrow{}  (x,y:\mBbbR{}//(x  =  y))
\mvdash{}  IsRing(|real-ring()|;+real-ring();0;-real-ring();*;1)


By

---

Latex:
(RepUR  ``ring\_p  group\_p  monoid\_p  bilinear  assoc  ident  inverse  ``  0
  THEN  Auto
  THEN  Try  (DVar  `x')
  THEN  Try  (DVar  `y')
  THEN  Try  (DVar  `z')
  THEN  Try  (DVar  `a')
  THEN  EqTypeCD
  THEN  Auto
  THEN  \mforall{}h:hyp.  (RW  (SweepUpC  (HypC  h))  0  THENA  Complete  (Auto)) 
  THEN  Auto)

---

Home Index