---

Step * 3 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,y:Point(free-vs(K;S)).  (fs-in-subtype(K;S;T;f) ⇒ fs-in-subtype(K;S;T;y) ⇒ fs-in-subtype(K;S;T;f + y))
9. f : Point(free-vs(K;S))
10. a : |K|
11. b : basic-formal-sum(K;S)
12. f = b ∈ formal-sum(K;S)
13. bfs-predicate(K;S;p.snd(p) ∈ T;b)
14. a * f = a * b ∈ formal-sum(K;S)
⊢ bfs-predicate(K;S;p.snd(p) ∈ T;a * b)
BY
{ (ParallelOp -2 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,y:Point(free-vs(K;S)).  (fs-in-subtype(K;S;T;f) ⇒ fs-in-subtype(K;S;T;y) ⇒ fs-in-subtype(K;S;T;f + y))
9. f : Point(free-vs(K;S))
10. a : |K|
11. b : basic-formal-sum(K;S)
12. f = b ∈ formal-sum(K;S)
13. ∀p:|K| × S. (p ↓∈ b ⇒ (snd(p) ∈ T))
14. a * f = a * b ∈ formal-sum(K;S)
15. p1 : |K|
16. p2 : S
17. <p1, p2> ↓∈ a * b
⊢ p2 ∈ T

---

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.  \mforall{}f,y:Point(free-vs(K;S)).
          (fs-in-subtype(K;S;T;f)  {}\mRightarrow{}  fs-in-subtype(K;S;T;y)  {}\mRightarrow{}  fs-in-subtype(K;S;T;f  +  y))
9.  f  :  Point(free-vs(K;S))
10.  a  :  |K|
11.  b  :  basic-formal-sum(K;S)
12.  f  =  b
13.  bfs-predicate(K;S;p.snd(p)  \mmember{}  T;b)
14.  a  *  f  =  a  *  b
\mvdash{}  bfs-predicate(K;S;p.snd(p)  \mmember{}  T;a  *  b)


By

---

Latex:
(ParallelOp  -2  THEN  Auto)

---

Home Index