---

Step * of Lemma padic-ring_wf

No Annotations
∀[p:{2...}]. (padic-ring(p) ∈ CRng)
BY
{ ((InstLemma `p-adic-ring_wf` [] THEN ParallelLast')
   THEN (MemTypeHD (-1)⋅ THENA Auto)
   THEN Fold `member` (-2)
   THEN (MemTypeHD (-2)⋅ THENA Auto)
   THEN Fold `member` (-3)
   THEN RepUR ``p-adic-ring ring_p group_p monoid_p`` -2
   THEN RepUR ``bilinear assoc ident inverse`` -2
   THEN RepUR ``p-adic-ring comm`` -1
   THEN Repeat ((MemTypeCD THEN Auto))
   THEN RepUR ``padic-ring`` 0) }

1
1. p : {2...}
2. ℤ(p) ∈ RngSig
3. ∀[x,y,z:p-adics(p)].  (x + y + z = x + y + z ∈ p-adics(p))
4. ∀[x:p-adics(p)]. ((x + 0(p) = x ∈ p-adics(p)) ∧ (0(p) + x = x ∈ p-adics(p)))
5. ∀[x:p-adics(p)]. ((x + -(x) = 0(p) ∈ p-adics(p)) ∧ (-(x) + x = 0(p) ∈ p-adics(p)))
6. ∀[x,y,z:p-adics(p)].  (x * y * z = x * y * z ∈ p-adics(p))
7. ∀[x:p-adics(p)]. ((x * 1(p) = x ∈ p-adics(p)) ∧ (1(p) * x = x ∈ p-adics(p)))
8. ∀[a,x,y:p-adics(p)].  ((a * x + y = a * x + a * y ∈ p-adics(p)) ∧ (x + y * a = x * a + y * a ∈ p-adics(p)))
9. ∀[x,y:p-adics(p)].  (x * y = y * x ∈ p-adics(p))
⊢ <padic(p), λu,v. ff, λu,v. ff, λu,v. pa-add(p;u;v), 0(p), λu.pa-minus(p;u), λu,v. pa-mul(p;u;v), 1(p), λu,v. (inr ⋅ )>\000C ∈ RngSig

2
1. p : {2...}
2. ℤ(p) ∈ RngSig
3. ∀[x,y,z:p-adics(p)].  (x + y + z = x + y + z ∈ p-adics(p))
4. ∀[x:p-adics(p)]. ((x + 0(p) = x ∈ p-adics(p)) ∧ (0(p) + x = x ∈ p-adics(p)))
5. ∀[x:p-adics(p)]. ((x + -(x) = 0(p) ∈ p-adics(p)) ∧ (-(x) + x = 0(p) ∈ p-adics(p)))
6. ∀[x,y,z:p-adics(p)].  (x * y * z = x * y * z ∈ p-adics(p))
7. ∀[x:p-adics(p)]. ((x * 1(p) = x ∈ p-adics(p)) ∧ (1(p) * x = x ∈ p-adics(p)))
8. ∀[a,x,y:p-adics(p)].  ((a * x + y = a * x + a * y ∈ p-adics(p)) ∧ (x + y * a = x * a + y * a ∈ p-adics(p)))
9. ∀[x,y:p-adics(p)].  (x * y = y * x ∈ p-adics(p))
⊢ IsRing(padic(p);λu,v. pa-add(p;u;v);0(p);λu.pa-minus(p;u);λu,v. pa-mul(p;u;v);1(p))

3
1. p : {2...}
2. ℤ(p) ∈ RngSig
3. ∀[x,y,z:p-adics(p)].  (x + y + z = x + y + z ∈ p-adics(p))
4. ∀[x:p-adics(p)]. ((x + 0(p) = x ∈ p-adics(p)) ∧ (0(p) + x = x ∈ p-adics(p)))
5. ∀[x:p-adics(p)]. ((x + -(x) = 0(p) ∈ p-adics(p)) ∧ (-(x) + x = 0(p) ∈ p-adics(p)))
6. ∀[x,y,z:p-adics(p)].  (x * y * z = x * y * z ∈ p-adics(p))
7. ∀[x:p-adics(p)]. ((x * 1(p) = x ∈ p-adics(p)) ∧ (1(p) * x = x ∈ p-adics(p)))
8. ∀[a,x,y:p-adics(p)].  ((a * x + y = a * x + a * y ∈ p-adics(p)) ∧ (x + y * a = x * a + y * a ∈ p-adics(p)))
9. ∀[x,y:p-adics(p)].  (x * y = y * x ∈ p-adics(p))
⊢ Comm(padic(p);λu,v. pa-mul(p;u;v))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[p:\{2...\}].  (padic-ring(p)  \mmember{}  CRng)


By

---

Latex:
((InstLemma  `p-adic-ring\_wf`  []  THEN  ParallelLast')
  THEN  (MemTypeHD  (-1)\mcdot{}  THENA  Auto)
  THEN  Fold  `member`  (-2)
  THEN  (MemTypeHD  (-2)\mcdot{}  THENA  Auto)
  THEN  Fold  `member`  (-3)
  THEN  RepUR  ``p-adic-ring  ring\_p  group\_p  monoid\_p``  -2
  THEN  RepUR  ``bilinear  assoc  ident  inverse``  -2
  THEN  RepUR  ``p-adic-ring  comm``  -1
  THEN  Repeat  ((MemTypeCD  THEN  Auto))
  THEN  RepUR  ``padic-ring``  0)

---

Home Index