---

Step * 1 2 1 1 of Lemma bpa-norm-equiv


1. p : {2...}
2. x1 : {1...}
3. x2 : p-adics(p)
4. x2 x1 ≠ 0
5. k : ℕx1 + 1
6. v1 : p-units(p)
⊢ p^(x1 - k)(p) * p^k(p) * v1 = p^x1(p) * v1 ∈ p-adics(p)
BY
{ ((InstLemma `p-adic-ring_wf` [⌜p⌝]⋅ THENA Auto)
   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 (RWW "-4 p-mul-int" 0 THENA Auto)
   THEN RepeatFor 2 (EqCDA)
   THEN RWO  "exp_add<" 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  p  :  \{2...\}
2.  x1  :  \{1...\}
3.  x2  :  p-adics(p)
4.  x2  x1  \mneq{}  0
5.  k  :  \mBbbN{}x1  +  1
6.  v1  :  p-units(p)
\mvdash{}  p\^{}(x1  -  k)(p)  *  p\^{}k(p)  *  v1  =  p\^{}x1(p)  *  v1


By

---

Latex:
((InstLemma  `p-adic-ring\_wf`  [\mkleeneopen{}p\mkleeneclose{}]\mcdot{}  THENA  Auto)
  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  (RWW  "-4  p-mul-int"  0  THENA  Auto)
  THEN  RepeatFor  2  (EqCDA)
  THEN  RWO    "exp\_add<"  0
  THEN  Auto)

---

Home Index