Step
*
2
of Lemma
bag-summation-linear1-right
1. T : Type
2. R : Type
3. add : R ⟶ R ⟶ R
4. mul : R ⟶ R ⟶ R
5. zero : R
6. b : bag(T)
7. f : T ⟶ R
8. ∀[g:T ⟶ R]
∀a:R. (Σ(x∈b). (f[x] add g[x]) mul a = ((Σ(x∈b). f[x] add Σ(x∈b). g[x]) mul a) ∈ R)
supposing (∃minus:R ⟶ R. IsGroup(R;add;zero;minus)) ∧ Comm(R;add) ∧ BiLinear(R;add;mul)
9. minus : R ⟶ R
10. IsGroup(R;add;zero;minus)
11. Comm(R;add)
12. BiLinear(R;add;mul)
13. a : R
14. Σ(x∈b). (f[x] add zero) mul a = ((Σ(x∈b). f[x] add Σ(x∈b). zero) mul a) ∈ R
⊢ Σ(x∈b). f[x] = (Σ(x∈b). f[x] add Σ(x∈b). zero) ∈ R
BY
{ (RWO "bag-summation-zero" 0 THEN Auto) }
1
1. T : Type
2. R : Type
3. add : R ⟶ R ⟶ R
4. mul : R ⟶ R ⟶ R
5. zero : R
6. b : bag(T)
7. f : T ⟶ R
8. ∀[g:T ⟶ R]
∀a:R. (Σ(x∈b). (f[x] add g[x]) mul a = ((Σ(x∈b). f[x] add Σ(x∈b). g[x]) mul a) ∈ R)
supposing (∃minus:R ⟶ R. IsGroup(R;add;zero;minus)) ∧ Comm(R;add) ∧ BiLinear(R;add;mul)
9. minus : R ⟶ R
10. IsGroup(R;add;zero;minus)
11. Comm(R;add)
12. BiLinear(R;add;mul)
13. a : R
14. Σ(x∈b). (f[x] add zero) mul a = ((Σ(x∈b). f[x] add Σ(x∈b). zero) mul a) ∈ R
⊢ Σ(x∈b). f[x] = (Σ(x∈b). f[x] add zero) ∈ R
Latex:
Latex:
1. T : Type
2. R : Type
3. add : R {}\mrightarrow{} R {}\mrightarrow{} R
4. mul : R {}\mrightarrow{} R {}\mrightarrow{} R
5. zero : R
6. b : bag(T)
7. f : T {}\mrightarrow{} R
8. \mforall{}[g:T {}\mrightarrow{} R]
\mforall{}a:R. (\mSigma{}(x\mmember{}b). (f[x] add g[x]) mul a = ((\mSigma{}(x\mmember{}b). f[x] add \mSigma{}(x\mmember{}b). g[x]) mul a))
supposing (\mexists{}minus:R {}\mrightarrow{} R. IsGroup(R;add;zero;minus)) \mwedge{} Comm(R;add) \mwedge{} BiLinear(R;add;mul)
9. minus : R {}\mrightarrow{} R
10. IsGroup(R;add;zero;minus)
11. Comm(R;add)
12. BiLinear(R;add;mul)
13. a : R
14. \mSigma{}(x\mmember{}b). (f[x] add zero) mul a = ((\mSigma{}(x\mmember{}b). f[x] add \mSigma{}(x\mmember{}b). zero) mul a)
\mvdash{} \mSigma{}(x\mmember{}b). f[x] = (\mSigma{}(x\mmember{}b). f[x] add \mSigma{}(x\mmember{}b). zero)
By
Latex:
(RWO "bag-summation-zero" 0 THEN Auto)
Home
Index