---

Step * of Lemma vs-map-quotients

No Annotations
∀[K:CRng]. ∀[A,B:VectorSpace(K)]. ∀[P:Point(A) ⟶ ℙ]. ∀[Q:Point(B) ⟶ ℙ].
  ∀[f:A ⟶ B]. f ∈ A//z.P[z] ⟶ B//z.Q[z] supposing ∀a:Point(A). (P[a] ⇒ Q[f a]) 
  supposing vs-subspace(K;A;z.P[z]) ∧ vs-subspace(K;B;z.Q[z])
BY
{ (Intros
   THEN Unhide
   THEN DVar `f'
   THEN (Assert ⌜f ∈ Point(A//z.P[z]) ⟶ Point(B//z.Q[z])⌝⋅ THENM ((MemTypeCD THENW Auto) THEN Try (Trivial)))) }

1
.....assertion..... 
1. K : CRng
2. A : VectorSpace(K)
3. B : VectorSpace(K)
4. P : Point(A) ⟶ ℙ
5. Q : Point(B) ⟶ ℙ
6. vs-subspace(K;A;z.P[z]) ∧ vs-subspace(K;B;z.Q[z])
7. f : Point(A) ⟶ Point(B)
8. (∀u,v:Point(A).  ((f u + v) = f u + f v ∈ Point(B))) ∧ (∀a:|K|. ∀u:Point(A).  ((f a * u) = a * f u ∈ Point(B)))
9. ∀a:Point(A). (P[a] ⇒ Q[f a])
⊢ f ∈ Point(A//z.P[z]) ⟶ Point(B//z.Q[z])

2
.....set predicate..... 
1. K : CRng
2. A : VectorSpace(K)
3. B : VectorSpace(K)
4. P : Point(A) ⟶ ℙ
5. Q : Point(B) ⟶ ℙ
6. vs-subspace(K;A;z.P[z]) ∧ vs-subspace(K;B;z.Q[z])
7. f : Point(A) ⟶ Point(B)
8. (∀u,v:Point(A).  ((f u + v) = f u + f v ∈ Point(B))) ∧ (∀a:|K|. ∀u:Point(A).  ((f a * u) = a * f u ∈ Point(B)))
9. ∀a:Point(A). (P[a] ⇒ Q[f a])
10. f ∈ Point(A//z.P[z]) ⟶ Point(B//z.Q[z])
⊢ (∀u,v:Point(A//z.P[z]).  ((f u + v) = f u + f v ∈ Point(B//z.Q[z])))
∧ (∀a:|K|. ∀u:Point(A//z.P[z]).  ((f a * u) = a * f u ∈ Point(B//z.Q[z])))

---

Latex:

---

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


By

---

Latex:
(Intros
  THEN  Unhide
  THEN  DVar  `f'
  THEN  (Assert  \mkleeneopen{}f  \mmember{}  Point(A//z.P[z])  {}\mrightarrow{}  Point(B//z.Q[z])\mkleeneclose{}\mcdot{}
  THENM  ((MemTypeCD  THENW  Auto)  THEN  Try  (Trivial))
  ))

---

Home Index