Step
*
1
2
of Lemma
fps-linear-ucont-equal
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. F : PowerSeries(X;r) ⟶ PowerSeries(X;r)
6. G : PowerSeries(X;r) ⟶ PowerSeries(X;r)
7. ∀f,g:PowerSeries(X;r). (F[(f+g)] = (F[f]+F[g]) ∈ PowerSeries(X;r))
8. ∀f,g:PowerSeries(X;r). (G[(f+g)] = (G[f]+G[g]) ∈ PowerSeries(X;r))
9. ∀c:|r|. ∀f:PowerSeries(X;r). (F[(c)*f] = (c)*F[f] ∈ PowerSeries(X;r))
10. ∀c:|r|. ∀f:PowerSeries(X;r). (G[(c)*f] = (c)*G[f] ∈ PowerSeries(X;r))
11. ∀b:bag(X). (F[<b>] = G[<b>] ∈ PowerSeries(X;r))
12. f : PowerSeries(X;r)
13. b : bag(X)
14. d1 : bag(X)
15. ∀f:PowerSeries(X;r). (F[f][b] = F[fps-restrict(eq;r;f;d1)][b] ∈ |r|)
16. d : bag(X)
17. ∀f:PowerSeries(X;r). (G[f][b] = G[fps-restrict(eq;r;f;d)][b] ∈ |r|)
18. F[fps-restrict(eq;r;f;d1 + d)][b] = G[fps-restrict(eq;r;f;d1 + d)][b] ∈ |r|
⊢ F[fps-restrict(eq;r;f;d1)][b] = G[fps-restrict(eq;r;f;d)][b] ∈ |r|
BY
{ xxx((RWO "-4 -2" (-1) THEN Auto)
THEN NthHypEq (-1)
THEN RepeatFor 3 ((EqCD THEN Auto))
THEN BLemma `fps-ext`
THEN Auto
THEN RepUR ``fps-restrict fps-coeff`` 0
THEN RepeatFor 2 (AutoSplit))xxx }
1
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. F : PowerSeries(X;r) ⟶ PowerSeries(X;r)
6. G : PowerSeries(X;r) ⟶ PowerSeries(X;r)
7. ∀f,g:PowerSeries(X;r). (F[(f+g)] = (F[f]+F[g]) ∈ PowerSeries(X;r))
8. ∀f,g:PowerSeries(X;r). (G[(f+g)] = (G[f]+G[g]) ∈ PowerSeries(X;r))
9. ∀c:|r|. ∀f:PowerSeries(X;r). (F[(c)*f] = (c)*F[f] ∈ PowerSeries(X;r))
10. ∀c:|r|. ∀f:PowerSeries(X;r). (G[(c)*f] = (c)*G[f] ∈ PowerSeries(X;r))
11. ∀b:bag(X). (F[<b>] = G[<b>] ∈ PowerSeries(X;r))
12. f : PowerSeries(X;r)
13. b : bag(X)
14. d1 : bag(X)
15. ∀f:PowerSeries(X;r). (F[f][b] = F[fps-restrict(eq;r;f;d1)][b] ∈ |r|)
16. d : bag(X)
17. ∀f:PowerSeries(X;r). (G[f][b] = G[fps-restrict(eq;r;f;d)][b] ∈ |r|)
18. F[fps-restrict(eq;r;fps-restrict(eq;r;f;d1 + d);d1)][b]
= G[fps-restrict(eq;r;fps-restrict(eq;r;f;d1 + d);d)][b]
∈ |r|
19. b1 : bag(X)
20. ¬sub-bag(X;b1;d1 + d)
21. sub-bag(X;b1;d1)
⊢ (f b1) = 0 ∈ |r|
2
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. F : PowerSeries(X;r) ⟶ PowerSeries(X;r)
6. G : PowerSeries(X;r) ⟶ PowerSeries(X;r)
7. ∀f,g:PowerSeries(X;r). (F[(f+g)] = (F[f]+F[g]) ∈ PowerSeries(X;r))
8. ∀f,g:PowerSeries(X;r). (G[(f+g)] = (G[f]+G[g]) ∈ PowerSeries(X;r))
9. ∀c:|r|. ∀f:PowerSeries(X;r). (F[(c)*f] = (c)*F[f] ∈ PowerSeries(X;r))
10. ∀c:|r|. ∀f:PowerSeries(X;r). (G[(c)*f] = (c)*G[f] ∈ PowerSeries(X;r))
11. ∀b:bag(X). (F[<b>] = G[<b>] ∈ PowerSeries(X;r))
12. f : PowerSeries(X;r)
13. b : bag(X)
14. d1 : bag(X)
15. ∀f:PowerSeries(X;r). (F[f][b] = F[fps-restrict(eq;r;f;d1)][b] ∈ |r|)
16. d : bag(X)
17. ∀f:PowerSeries(X;r). (G[f][b] = G[fps-restrict(eq;r;f;d)][b] ∈ |r|)
18. F[fps-restrict(eq;r;fps-restrict(eq;r;f;d1 + d);d1)][b]
= G[fps-restrict(eq;r;fps-restrict(eq;r;f;d1 + d);d)][b]
∈ |r|
19. b1 : bag(X)
20. ¬sub-bag(X;b1;d1 + d)
21. sub-bag(X;b1;d)
⊢ (f b1) = 0 ∈ |r|
Latex:
Latex:
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. F : PowerSeries(X;r) {}\mrightarrow{} PowerSeries(X;r)
6. G : PowerSeries(X;r) {}\mrightarrow{} PowerSeries(X;r)
7. \mforall{}f,g:PowerSeries(X;r). (F[(f+g)] = (F[f]+F[g]))
8. \mforall{}f,g:PowerSeries(X;r). (G[(f+g)] = (G[f]+G[g]))
9. \mforall{}c:|r|. \mforall{}f:PowerSeries(X;r). (F[(c)*f] = (c)*F[f])
10. \mforall{}c:|r|. \mforall{}f:PowerSeries(X;r). (G[(c)*f] = (c)*G[f])
11. \mforall{}b:bag(X). (F[<b>] = G[<b>])
12. f : PowerSeries(X;r)
13. b : bag(X)
14. d1 : bag(X)
15. \mforall{}f:PowerSeries(X;r). (F[f][b] = F[fps-restrict(eq;r;f;d1)][b])
16. d : bag(X)
17. \mforall{}f:PowerSeries(X;r). (G[f][b] = G[fps-restrict(eq;r;f;d)][b])
18. F[fps-restrict(eq;r;f;d1 + d)][b] = G[fps-restrict(eq;r;f;d1 + d)][b]
\mvdash{} F[fps-restrict(eq;r;f;d1)][b] = G[fps-restrict(eq;r;f;d)][b]
By
Latex:
xxx((RWO "-4 -2" (-1) THEN Auto)
THEN NthHypEq (-1)
THEN RepeatFor 3 ((EqCD THEN Auto))
THEN BLemma `fps-ext`
THEN Auto
THEN RepUR ``fps-restrict fps-coeff`` 0
THEN RepeatFor 2 (AutoSplit))xxx
Home
Index