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


1. CRng
2. Type
3. Type
4. strong-subtype(T;S)
5. T ⊆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. Point(free-vs(K;S))
10. |K|
11. basic-formal-sum(K;S)
12. b ∈ formal-sum(K;S)
13. ∀p:|K| × S. (p ↓∈  (snd(p) ∈ T))
14. b ∈ formal-sum(K;S)
15. p1 |K|
16. p2 S
17. <p1, p2> ↓∈ b
⊢ p2 ∈ T
BY
(RepUR ``formal-sum-mul`` -2
   THEN (BagMemberD (-1) THENA Auto)
   THEN RepeatFor (D -1)
   THEN -2
   THEN All Reduce
   THEN -1) }

1
1. CRng
2. Type
3. Type
4. strong-subtype(T;S)
5. T ⊆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. Point(free-vs(K;S))
10. |K|
11. basic-formal-sum(K;S)
12. b ∈ formal-sum(K;S)
13. ∀p:|K| × S. (p ↓∈  (snd(p) ∈ T))
14. b ∈ formal-sum(K;S)
15. p1 |K|
16. p2 S
17. v1 |K|
18. v2 S
19. <v1, v2> ↓∈ b
20. <p1, p2> = <v1, v2> ∈ (|K| × S)
⊢ 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.  \mforall{}p:|K|  \mtimes{}  S.  (p  \mdownarrow{}\mmember{}  b  {}\mRightarrow{}  (snd(p)  \mmember{}  T))
14.  a  *  f  =  a  *  b
15.  p1  :  |K|
16.  p2  :  S
17.  <p1,  p2>  \mdownarrow{}\mmember{}  a  *  b
\mvdash{}  p2  \mmember{}  T


By


Latex:
(RepUR  ``formal-sum-mul``  -2
  THEN  (BagMemberD  (-1)  THENA  Auto)
  THEN  RepeatFor  2  (D  -1)
  THEN  D  -2
  THEN  All  Reduce
  THEN  D  -1)




Home Index