---

Step * 1 of Lemma vs-lift-add


1. S : Type
2. K : CRng
3. vs : VectorSpace(K)
4. f : S ⟶ vs."Point"
5. u : Base
6. u1 : Base
7. u = u1 ∈ pertype(λa,b. ((a ∈ basic-formal-sum(K;S)) ∧ (b ∈ basic-formal-sum(K;S)) ∧ bfs-equiv(K;S;a;b)))
8. u ∈ basic-formal-sum(K;S)
9. u1 ∈ basic-formal-sum(K;S)
10. bfs-equiv(K;S;u;u1)
11. v : Base
12. v1 : Base
13. v = v1 ∈ pertype(λa,b. ((a ∈ basic-formal-sum(K;S)) ∧ (b ∈ basic-formal-sum(K;S)) ∧ bfs-equiv(K;S;a;b)))
14. v ∈ basic-formal-sum(K;S)
15. v1 ∈ basic-formal-sum(K;S)
16. bfs-equiv(K;S;v;v1)
⊢ vs-lift(vs;f;u + v) = vs-lift(vs;f;u1) + vs-lift(vs;f;v1) ∈ Point(vs)
BY
{ (Subst' vs-lift(vs;f;u + v) = vs-lift(vs;f;u) + vs-lift(vs;f;v) ∈ Point(vs) 0 THENA Auto) }

1
1. S : Type
2. K : CRng
3. vs : VectorSpace(K)
4. f : S ⟶ vs."Point"
5. u : Base
6. u1 : Base
7. u = u1 ∈ pertype(λa,b. ((a ∈ basic-formal-sum(K;S)) ∧ (b ∈ basic-formal-sum(K;S)) ∧ bfs-equiv(K;S;a;b)))
8. u ∈ basic-formal-sum(K;S)
9. u1 ∈ basic-formal-sum(K;S)
10. bfs-equiv(K;S;u;u1)
11. v : Base
12. v1 : Base
13. v = v1 ∈ pertype(λa,b. ((a ∈ basic-formal-sum(K;S)) ∧ (b ∈ basic-formal-sum(K;S)) ∧ bfs-equiv(K;S;a;b)))
14. v ∈ basic-formal-sum(K;S)
15. v1 ∈ basic-formal-sum(K;S)
16. bfs-equiv(K;S;v;v1)
⊢ vs-lift(vs;f;u) + vs-lift(vs;f;v) = vs-lift(vs;f;u1) + vs-lift(vs;f;v1) ∈ Point(vs)

---

Latex:

---

Latex:

1.  S  :  Type
2.  K  :  CRng
3.  vs  :  VectorSpace(K)
4.  f  :  S  {}\mrightarrow{}  vs."Point"
5.  u  :  Base
6.  u1  :  Base
7.  u  =  u1
8.  u  \mmember{}  basic-formal-sum(K;S)
9.  u1  \mmember{}  basic-formal-sum(K;S)
10.  bfs-equiv(K;S;u;u1)
11.  v  :  Base
12.  v1  :  Base
13.  v  =  v1
14.  v  \mmember{}  basic-formal-sum(K;S)
15.  v1  \mmember{}  basic-formal-sum(K;S)
16.  bfs-equiv(K;S;v;v1)
\mvdash{}  vs-lift(vs;f;u  +  v)  =  vs-lift(vs;f;u1)  +  vs-lift(vs;f;v1)


By

---

Latex:
(Subst'  vs-lift(vs;f;u  +  v)  =  vs-lift(vs;f;u)  +  vs-lift(vs;f;v)  0  THENA  Auto)

---

Home Index