Step
*
1
1
of Lemma
fps-mul-coeff-bag-rep-simple
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. n : ℕ
5. k : ℕn + 1
6. r : CRng
7. f : PowerSeries(X;r)
8. g : PowerSeries(X;r)
9. x : X
10. ∀i:ℕn + 1. ((¬(i = k ∈ ℤ))
⇒ (f[bag-rep(i;x)] = 0 ∈ |r|))
11. x1 : bag(X)
12. x2 : bag(X)
13. <x1, x2> ↓∈ bag-partitions(eq;bag-rep(n;x))
⊢ (<x1, x2> = <bag-rep(k;x), bag-rep(n - k;x)> ∈ (bag(X) × bag(X))) ∨ ((* f[fst(<x1, x2>)] g[snd(<x1, x2>)]) = 0 ∈ |r|)
BY
{ BagMemberD (-1)⋅ }
1
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. n : ℕ
5. k : ℕn + 1
6. r : CRng
7. f : PowerSeries(X;r)
8. g : PowerSeries(X;r)
9. x : X
10. ∀i:ℕn + 1. ((¬(i = k ∈ ℤ))
⇒ (f[bag-rep(i;x)] = 0 ∈ |r|))
11. x1 : bag(X)
12. x2 : bag(X)
13. (x1 + x2) = bag-rep(n;x) ∈ bag(X)
⊢ (<x1, x2> = <bag-rep(k;x), bag-rep(n - k;x)> ∈ (bag(X) × bag(X))) ∨ ((* f[fst(<x1, x2>)] g[snd(<x1, x2>)]) = 0 ∈ |r|)
Latex:
Latex:
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. n : \mBbbN{}
5. k : \mBbbN{}n + 1
6. r : CRng
7. f : PowerSeries(X;r)
8. g : PowerSeries(X;r)
9. x : X
10. \mforall{}i:\mBbbN{}n + 1. ((\mneg{}(i = k)) {}\mRightarrow{} (f[bag-rep(i;x)] = 0))
11. x1 : bag(X)
12. x2 : bag(X)
13. <x1, x2> \mdownarrow{}\mmember{} bag-partitions(eq;bag-rep(n;x))
\mvdash{} (<x1, x2> = <bag-rep(k;x), bag-rep(n - k;x)>) \mvee{} ((* f[fst(<x1, x2>)] g[snd(<x1, x2>)]) = 0)
By
Latex:
BagMemberD (-1)\mcdot{}
Home
Index