---

Step * 1 2 of Lemma fps-rng_wf

.....set predicate..... 
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
⊢ IsRing(|fps-rng(r)|;+fps-rng(r);0;-fps-rng(r);*;1)
BY
{ TACTIC:((Assert IsMonoid(|r|;+r;0) ∧ Inverse(|r|;+r;0;-r) ∧ IsMonoid(|r|;*;1) ∧ BiLinear(|r|;+r;*) BY
                 (RepeatFor 2 (DVar `r') THEN D -2 THEN D -3 THEN Auto))
          THEN RepeatFor 3 (D 0)
          THEN Reduce 0
          THEN Auto) }

1
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. IsMonoid(|r|;+r;0)
6. Inverse(|r|;+r;0;-r)
7. IsMonoid(|r|;*;1)
8. BiLinear(|r|;+r;*)
⊢ Assoc(PowerSeries(X;r);λf,g. (f+g))

2
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. IsMonoid(|r|;+r;0)
6. Inverse(|r|;+r;0;-r)
7. IsMonoid(|r|;*;1)
8. BiLinear(|r|;+r;*)
⊢ Ident(PowerSeries(X;r);λf,g. (f+g);0)

3
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. IsMonoid(|r|;+r;0)
6. Inverse(|r|;+r;0;-r)
7. IsMonoid(|r|;*;1)
8. BiLinear(|r|;+r;*)
9. x : |fps-rng(r)|
⊢ (x+-(x)) = 0 ∈ PowerSeries(X;r)

4
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. IsMonoid(|r|;+r;0)
6. Inverse(|r|;+r;0;-r)
7. IsMonoid(|r|;*;1)
8. BiLinear(|r|;+r;*)
⊢ Assoc(PowerSeries(X;r);λf,g. (f*g))

5
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. IsMonoid(|r|;+r;0)
6. Inverse(|r|;+r;0;-r)
7. IsMonoid(|r|;*;1)
8. BiLinear(|r|;+r;*)
⊢ Ident(PowerSeries(X;r);λf,g. (f*g);1)

6
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. IsMonoid(|r|;+r;0)
6. Inverse(|r|;+r;0;-r)
7. IsMonoid(|r|;*;1)
8. BiLinear(|r|;+r;*)
9. a : |fps-rng(r)|
10. x : PowerSeries(X;r)
11. y : PowerSeries(X;r)
⊢ (a*(x+y)) = ((a*x)+(a*y)) ∈ PowerSeries(X;r)

7
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. IsMonoid(|r|;+r;0)
6. Inverse(|r|;+r;0;-r)
7. IsMonoid(|r|;*;1)
8. BiLinear(|r|;+r;*)
9. a : |fps-rng(r)|
10. x : PowerSeries(X;r)
11. y : PowerSeries(X;r)
12. (a*(x+y)) = ((a*x)+(a*y)) ∈ PowerSeries(X;r)
⊢ ((x+y)*a) = ((x*a)+(y*a)) ∈ PowerSeries(X;r)

---

Latex:

---

Latex:
.....set  predicate..... 
1.  X  :  Type
2.  valueall-type(X)
3.  eq  :  EqDecider(X)
4.  r  :  CRng
\mvdash{}  IsRing(|fps-rng(r)|;+fps-rng(r);0;-fps-rng(r);*;1)


By

---

Latex:
TACTIC:((Assert  IsMonoid(|r|;+r;0)
                              \mwedge{}  Inverse(|r|;+r;0;-r)
                              \mwedge{}  IsMonoid(|r|;*;1)
                              \mwedge{}  BiLinear(|r|;+r;*)  BY
                              (RepeatFor  2  (DVar  `r')  THEN  D  -2  THEN  D  -3  THEN  Auto))
                THEN  RepeatFor  3  (D  0)
                THEN  Reduce  0
                THEN  Auto)

---

Home Index