Step
*
1
1
of Lemma
fps-elim-hom
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. x : X
6. FunThru2op(PowerSeries(X;r);PowerSeries(X;r);λf,g. (f+g);λf,g. (f+g);fps-elim(x))
7. a1 : PowerSeries(X;r)
8. a2 : PowerSeries(X;r)
9. b : bag(X)
10. x ↓∈ b
11. ∀[b:bag(bag(X) × bag(X))]. ∀[f:(bag(X) × bag(X)) ⟶ |r|].
Σ(x∈b). f[x] = 0 ∈ |r|
supposing (∀x:bag(X) × bag(X). (x ↓∈ b
⇒ (f[x] = 0 ∈ |r|))) ∧ IsMonoid(|r|;+r;0) ∧ Comm(|r|;+r)
12. p : bag(X) × bag(X)
13. p ↓∈ bag-partitions(eq;b)
⊢ (* if bag-deq-member(eq;x;fst(p)) then 0 else a1 (fst(p)) fi
if bag-deq-member(eq;x;snd(p)) then 0 else a2 (snd(p)) fi )
= 0
∈ |r|
BY
{ xxx((D (-2) THEN (RWO "bag-member-partitions" (-1) THENA Auto))
THEN Reduce 0
THEN RepeatFor 2 (AutoSplit)
THEN RW RngNormC 0
THEN Auto)⋅xxx }
1
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. x : X
6. FunThru2op(PowerSeries(X;r);PowerSeries(X;r);λf,g. (f+g);λf,g. (f+g);fps-elim(x))
7. a1 : PowerSeries(X;r)
8. a2 : PowerSeries(X;r)
9. b : bag(X)
10. x ↓∈ b
11. ∀[b:bag(bag(X) × bag(X))]. ∀[f:(bag(X) × bag(X)) ⟶ |r|].
Σ(x∈b). f[x] = 0 ∈ |r|
supposing (∀x:bag(X) × bag(X). (x ↓∈ b
⇒ (f[x] = 0 ∈ |r|))) ∧ IsMonoid(|r|;+r;0) ∧ Comm(|r|;+r)
12. p1 : bag(X)
13. ¬x ↓∈ p1
14. p2 : bag(X)
15. ¬x ↓∈ p2
16. (p1 + p2) = b ∈ bag(X)
⊢ (* (a1 p1) (a2 p2)) = 0 ∈ |r|
Latex:
Latex:
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. x : X
6. FunThru2op(PowerSeries(X;r);PowerSeries(X;r);\mlambda{}f,g. (f+g);\mlambda{}f,g. (f+g);fps-elim(x))
7. a1 : PowerSeries(X;r)
8. a2 : PowerSeries(X;r)
9. b : bag(X)
10. x \mdownarrow{}\mmember{} b
11. \mforall{}[b:bag(bag(X) \mtimes{} bag(X))]. \mforall{}[f:(bag(X) \mtimes{} bag(X)) {}\mrightarrow{} |r|].
\mSigma{}(x\mmember{}b). f[x] = 0
supposing (\mforall{}x:bag(X) \mtimes{} bag(X). (x \mdownarrow{}\mmember{} b {}\mRightarrow{} (f[x] = 0))) \mwedge{} IsMonoid(|r|;+r;0) \mwedge{} Comm(|r|;+r)
12. p : bag(X) \mtimes{} bag(X)
13. p \mdownarrow{}\mmember{} bag-partitions(eq;b)
\mvdash{} (* if bag-deq-member(eq;x;fst(p)) then 0 else a1 (fst(p)) fi
if bag-deq-member(eq;x;snd(p)) then 0 else a2 (snd(p)) fi )
= 0
By
Latex:
xxx((D (-2) THEN (RWO "bag-member-partitions" (-1) THENA Auto))
THEN Reduce 0
THEN RepeatFor 2 (AutoSplit)
THEN RW RngNormC 0
THEN Auto)\mcdot{}xxx
Home
Index