Step
*
2
of Lemma
padic-ring_wf
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))
BY
{ ((Assert ∀a,b:basic-padic(p). bpa-equiv(p;bpa-mul(p;a;b);pa-mul(p;a;b)) BY
(Auto THEN Unfold `pa-mul` 0 THEN Auto))
THEN (Assert ∀a,b:basic-padic(p). bpa-equiv(p;bpa-add(p;a;b);pa-add(p;a;b)) BY
(Auto THEN Unfold `pa-add` 0 THEN Auto))
THEN RepeatFor 2 ((D 0 THEN Reduce 0 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. ∀a,b:basic-padic(p). bpa-equiv(p;bpa-mul(p;a;b);pa-mul(p;a;b))
11. ∀a,b:basic-padic(p). bpa-equiv(p;bpa-add(p;a;b);pa-add(p;a;b))
⊢ IsMonoid(padic(p);λu,v. pa-add(p;u;v);0(p))
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))
10. ∀a,b:basic-padic(p). bpa-equiv(p;bpa-mul(p;a;b);pa-mul(p;a;b))
11. ∀a,b:basic-padic(p). bpa-equiv(p;bpa-add(p;a;b);pa-add(p;a;b))
⊢ Inverse(padic(p);λu,v. pa-add(p;u;v);0(p);λu.pa-minus(p;u))
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))
10. ∀a,b:basic-padic(p). bpa-equiv(p;bpa-mul(p;a;b);pa-mul(p;a;b))
11. ∀a,b:basic-padic(p). bpa-equiv(p;bpa-add(p;a;b);pa-add(p;a;b))
⊢ Assoc(padic(p);λu,v. pa-mul(p;u;v))
4
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. ∀a,b:basic-padic(p). bpa-equiv(p;bpa-mul(p;a;b);pa-mul(p;a;b))
11. ∀a,b:basic-padic(p). bpa-equiv(p;bpa-add(p;a;b);pa-add(p;a;b))
⊢ Ident(padic(p);λu,v. pa-mul(p;u;v);1(p))
5
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. ∀a,b:basic-padic(p). bpa-equiv(p;bpa-mul(p;a;b);pa-mul(p;a;b))
11. ∀a,b:basic-padic(p). bpa-equiv(p;bpa-add(p;a;b);pa-add(p;a;b))
12. IsMonoid(padic(p);λu,v. pa-mul(p;u;v);1(p))
13. a : padic(p)
14. x : padic(p)
15. y : padic(p)
⊢ pa-mul(p;a;pa-add(p;x;y)) = pa-add(p;pa-mul(p;a;x);pa-mul(p;a;y)) ∈ padic(p)
6
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. ∀a,b:basic-padic(p). bpa-equiv(p;bpa-mul(p;a;b);pa-mul(p;a;b))
11. ∀a,b:basic-padic(p). bpa-equiv(p;bpa-add(p;a;b);pa-add(p;a;b))
12. IsMonoid(padic(p);λu,v. pa-mul(p;u;v);1(p))
13. a : padic(p)
14. x : padic(p)
15. y : padic(p)
16. pa-mul(p;a;pa-add(p;x;y)) = pa-add(p;pa-mul(p;a;x);pa-mul(p;a;y)) ∈ padic(p)
⊢ pa-mul(p;pa-add(p;x;y);a) = pa-add(p;pa-mul(p;x;a);pa-mul(p;y;a)) ∈ padic(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)
\mvdash{} IsRing(padic(p);\mlambda{}u,v. pa-add(p;u;v);0(p);\mlambda{}u.pa-minus(p;u);\mlambda{}u,v. pa-mul(p;u;v);1(p))
By
Latex:
((Assert \mforall{}a,b:basic-padic(p). bpa-equiv(p;bpa-mul(p;a;b);pa-mul(p;a;b)) BY
(Auto THEN Unfold `pa-mul` 0 THEN Auto))
THEN (Assert \mforall{}a,b:basic-padic(p). bpa-equiv(p;bpa-add(p;a;b);pa-add(p;a;b)) BY
(Auto THEN Unfold `pa-add` 0 THEN Auto))
THEN RepeatFor 2 ((D 0 THEN Reduce 0 THEN Auto)))
Home
Index