---

Step * of Lemma vs-map-quotient

∀[K:CRng]. ∀[A,B:VectorSpace(K)]. ∀[P:Point(A) ⟶ ℙ].
  ∀[f:A ⟶ B]. f ∈ A//z.P[z] ⟶ B supposing ∀a:Point(A). (P[a] ⇒ ((f a) = 0 ∈ Point(B))) 
  supposing vs-subspace(K;A;z.P[z])
BY
{ (InstLemma `vs-map-quotients` []
   THEN RepeatFor 4 (ParallelLast')
   THEN (D -1 With ⌜λ2b.b = 0 ∈ Point(B)⌝  THENA Auto)
   THEN (ParallelLast' THENA (Auto THEN D 0 THEN RepUR ``so_apply so_lambda`` 0 THEN Auto THEN RWO "-1 -2" 0 THEN Auto))
   THEN (RepeatFor 2 (ParallelLast)
         THENA ((RepeatFor 2 (ParallelLast) THEN RepUR ``so_apply so_lambda`` 0) THEN Auto)
         )) }

1
1. K : CRng
2. A : VectorSpace(K)
3. B : VectorSpace(K)
4. P : Point(A) ⟶ ℙ
5. vs-subspace(K;A;z.P[z])
6. ∀[f:A ⟶ B]. f ∈ A//z.P[z] ⟶ B//z.λ2b.b = 0 ∈ Point(B)[z] supposing ∀a:Point(A). (P[a] ⇒ λ2b.b = 0 ∈ Point(B)[f a])
7. f : A ⟶ B
8. ∀a:Point(A). (P[a] ⇒ ((f a) = 0 ∈ Point(B)))
9. f ∈ A//z.P[z] ⟶ B//z.λ2b.b = 0 ∈ Point(B)[z]
⊢ f ∈ A//z.P[z] ⟶ B

---

Latex:

---

Latex:
\mforall{}[K:CRng].  \mforall{}[A,B:VectorSpace(K)].  \mforall{}[P:Point(A)  {}\mrightarrow{}  \mBbbP{}].
    \mforall{}[f:A  {}\mrightarrow{}  B].  f  \mmember{}  A//z.P[z]  {}\mrightarrow{}  B  supposing  \mforall{}a:Point(A).  (P[a]  {}\mRightarrow{}  ((f  a)  =  0)) 
    supposing  vs-subspace(K;A;z.P[z])


By

---

Latex:
(InstLemma  `vs-map-quotients`  []
  THEN  RepeatFor  4  (ParallelLast')
  THEN  (D  -1  With  \mkleeneopen{}\mlambda{}\msubtwo{}b.b  =  0\mkleeneclose{}    THENA  Auto)
  THEN  (ParallelLast'
              THENA  (Auto
                            THEN  D  0
                            THEN  RepUR  ``so\_apply  so\_lambda``  0
                            THEN  Auto
                            THEN  RWO  "-1  -2"  0
                            THEN  Auto)
              )
  THEN  (RepeatFor  2  (ParallelLast)
              THENA  ((RepeatFor  2  (ParallelLast)  THEN  RepUR  ``so\_apply  so\_lambda``  0)  THEN  Auto)
              ))

---

Home Index