---

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


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)
19. p^c1(p) * p^b1(p) * a2 = p^c1(p) * p^a1(p) * b2 ∈ p-adics(p)
20. p^a1(p) * p^c1(p) * b2 = p^a1(p) * p^b1(p) * c2 ∈ p-adics(p)
21. p^a1(p) * p^c1(p) * b2 = p^c1(p) * p^a1(p) * b2 ∈ p-adics(p)
22. p^c1(p) * p^b1(p) * a2 = p^a1(p) * p^b1(p) * c2 ∈ p-adics(p)
⊢ p^c1(p) * a2 = p^a1(p) * c2 ∈ p-adics(p)
BY
{ ThinVar `b2' }

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. c1 : ℕ
15. c2 : p-adics(p)
16. p^c1(p) * p^b1(p) * a2 = p^a1(p) * p^b1(p) * c2 ∈ p-adics(p)
⊢ p^c1(p) * a2 = p^a1(p) * c2 ∈ p-adics(p)

---

Latex:

---

Latex:

1.  p  :  \{2...\}
2.  \mBbbZ{}(p)  \mmember{}  RngSig
3.  \mforall{}[x,y,z:p-adics(p)].    (x  +  y  +  z  =  x  +  y  +  z)
4.  \mforall{}[x:p-adics(p)].  ((x  +  0(p)  =  x)  \mwedge{}  (0(p)  +  x  =  x))
5.  \mforall{}[x:p-adics(p)].  ((x  +  -(x)  =  0(p))  \mwedge{}  (-(x)  +  x  =  0(p)))
6.  \mforall{}[x,y,z:p-adics(p)].    (x  *  y  *  z  =  x  *  y  *  z)
7.  \mforall{}[x:p-adics(p)].  ((x  *  1(p)  =  x)  \mwedge{}  (1(p)  *  x  =  x))
8.  \mforall{}[a,x,y:p-adics(p)].    ((a  *  x  +  y  =  a  *  x  +  a  *  y)  \mwedge{}  (x  +  y  *  a  =  x  *  a  +  y  *  a))
9.  \mforall{}[x,y:p-adics(p)].    (x  *  y  =  y  *  x)
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)
11.  a1  :  \mBbbN{}
12.  a2  :  p-adics(p)
13.  b1  :  \mBbbN{}
14.  b2  :  p-adics(p)
15.  c1  :  \mBbbN{}
16.  c2  :  p-adics(p)
17.  p\^{}b1(p)  *  a2  =  p\^{}a1(p)  *  b2
18.  p\^{}c1(p)  *  b2  =  p\^{}b1(p)  *  c2
19.  p\^{}c1(p)  *  p\^{}b1(p)  *  a2  =  p\^{}c1(p)  *  p\^{}a1(p)  *  b2
20.  p\^{}a1(p)  *  p\^{}c1(p)  *  b2  =  p\^{}a1(p)  *  p\^{}b1(p)  *  c2
21.  p\^{}a1(p)  *  p\^{}c1(p)  *  b2  =  p\^{}c1(p)  *  p\^{}a1(p)  *  b2
22.  p\^{}c1(p)  *  p\^{}b1(p)  *  a2  =  p\^{}a1(p)  *  p\^{}b1(p)  *  c2
\mvdash{}  p\^{}c1(p)  *  a2  =  p\^{}a1(p)  *  c2


By

---

Latex:
ThinVar  `b2'

---

Home Index