---

Step * 2 of Lemma fs-in-subtype-subspace


1. K : CRng
2. S : Type
3. T : Type
4. strong-subtype(T;S)
5. T ⊆r S
6. respects-equality(S;T)
7. ∀[a,b:S].  (a = b ∈ T ∈ ℙ)
8. f : Point(free-vs(K;S))
9. y : Point(free-vs(K;S))
10. fs-in-subtype(K;S;T;f)
11. fs-in-subtype(K;S;T;y)
⊢ fs-in-subtype(K;S;T;f + y)
BY
{ (D -2 THEN D -1 THEN RepeatFor 2 (UnfoldTopAb 0) THEN Unhide THEN D 0 THEN ExRepD THEN D 0 With ⌜b1 + b⌝  THEN Auto) }

1
1. K : CRng
2. S : Type
3. T : Type
4. strong-subtype(T;S)
5. T ⊆r S
6. respects-equality(S;T)
7. ∀[a,b:S].  (a = b ∈ T ∈ ℙ)
8. f : Point(free-vs(K;S))
9. y : Point(free-vs(K;S))
10. b1 : basic-formal-sum(K;S)
11. f = b1 ∈ formal-sum(K;S)
12. bfs-predicate(K;S;p.snd(p) ∈ T;b1)
13. b : basic-formal-sum(K;S)
14. y = b ∈ formal-sum(K;S)
15. bfs-predicate(K;S;p.snd(p) ∈ T;b)
⊢ f + y = (b1 + b) ∈ formal-sum(K;S)

2
1. K : CRng
2. S : Type
3. T : Type
4. strong-subtype(T;S)
5. T ⊆r S
6. respects-equality(S;T)
7. ∀[a,b:S].  (a = b ∈ T ∈ ℙ)
8. f : Point(free-vs(K;S))
9. y : Point(free-vs(K;S))
10. b1 : basic-formal-sum(K;S)
11. f = b1 ∈ formal-sum(K;S)
12. bfs-predicate(K;S;p.snd(p) ∈ T;b1)
13. b : basic-formal-sum(K;S)
14. y = b ∈ formal-sum(K;S)
15. bfs-predicate(K;S;p.snd(p) ∈ T;b)
16. f + y = (b1 + b) ∈ formal-sum(K;S)
⊢ bfs-predicate(K;S;p.snd(p) ∈ T;b1 + b)

---

Latex:

---

Latex:

1.  K  :  CRng
2.  S  :  Type
3.  T  :  Type
4.  strong-subtype(T;S)
5.  T  \msubseteq{}r  S
6.  respects-equality(S;T)
7.  \mforall{}[a,b:S].    (a  =  b  \mmember{}  \mBbbP{})
8.  f  :  Point(free-vs(K;S))
9.  y  :  Point(free-vs(K;S))
10.  fs-in-subtype(K;S;T;f)
11.  fs-in-subtype(K;S;T;y)
\mvdash{}  fs-in-subtype(K;S;T;f  +  y)


By

---

Latex:
(D  -2
  THEN  D  -1
  THEN  RepeatFor  2  (UnfoldTopAb  0)
  THEN  Unhide
  THEN  D  0
  THEN  ExRepD
  THEN  D  0  With  \mkleeneopen{}b1  +  b\mkleeneclose{} 
  THEN  Auto)

---

Home Index