---

Step * of Lemma bpa-equiv-equiv

∀[p:{2...}]. EquivRel(basic-padic(p);x,y.bpa-equiv(p;x;y))
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 Auto
   THEN D 0
   THEN Auto
   THEN D 0
   THEN Reduce 0
   THEN Auto
   THEN DVar `a'
   THEN Try (DVar `b')
   THEN Try (DVar `c')
   THEN All (RepUR ``bpa-equiv``)⋅
   THEN Auto) }

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))
10. Sym(basic-padic(p);x,y.let n,a = x 
                           in let m,b = y 
                              in p^m(p) * a = p^n(p) * b ∈ p-adics(p))
11. a1 : ℕ
12. a2 : p-adics(p)
13. b1 : ℕ
14. b2 : p-adics(p)
15. c1 : ℕ
16. c2 : p-adics(p)
17. p^b1(p) * a2 = p^a1(p) * b2 ∈ p-adics(p)
18. p^c1(p) * b2 = p^b1(p) * c2 ∈ p-adics(p)
⊢ p^c1(p) * a2 = p^a1(p) * c2 ∈ p-adics(p)

---

Latex:

---

Latex:
\mforall{}[p:\{2...\}].  EquivRel(basic-padic(p);x,y.bpa-equiv(p;x;y))


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  Auto
  THEN  D  0
  THEN  Auto
  THEN  D  0
  THEN  Reduce  0
  THEN  Auto
  THEN  DVar  `a'
  THEN  Try  (DVar  `b')
  THEN  Try  (DVar  `c')
  THEN  All  (RepUR  ``bpa-equiv``)\mcdot{}
  THEN  Auto)

---

Home Index