---

Step * of Lemma p-distrib

∀[p:{2...}]. ∀[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)))
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) }

---

Latex:

---

Latex:
\mforall{}[p:\{2...\}].  \mforall{}[a,x,y:p-adics(p)].    ((a  *  x  +  y  =  a  *  x  +  a  *  y)  \mwedge{}  (x  +  y  *  a  =  x  *  a  +  y  *  a))


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)

---

Home Index