---

Step * 3 of Lemma vs-map-image-is-subspace


1. [K] : Rng
2. A : VectorSpace(K)
3. [B] : VectorSpace(K)
4. [f] : A ⟶ B
5. a1 : Point(A)
6. (f a1) = 0 ∈ Point(B)
7. ∀b,y:Point(B).
     ((∃a:Point(A). ((f a) = b ∈ Point(B)))
     ⇒ (∃a:Point(A). ((f a) = y ∈ Point(B)))
     ⇒ (∃a:Point(A). ((f a) = b + y ∈ Point(B))))
8. b : Point(B)
9. a@0 : |K|
10. a : Point(A)
11. (f a) = b ∈ Point(B)
⊢ ∃a:Point(A). ((f a) = a@0 * b ∈ Point(B))
BY
{ (D 0 With ⌜a@0 * a⌝  THEN Auto THEN DVar `f' THEN Auto) }

---

Latex:

---

Latex:

1.  [K]  :  Rng
2.  A  :  VectorSpace(K)
3.  [B]  :  VectorSpace(K)
4.  [f]  :  A  {}\mrightarrow{}  B
5.  a1  :  Point(A)
6.  (f  a1)  =  0
7.  \mforall{}b,y:Point(B).
          ((\mexists{}a:Point(A).  ((f  a)  =  b))  {}\mRightarrow{}  (\mexists{}a:Point(A).  ((f  a)  =  y))  {}\mRightarrow{}  (\mexists{}a:Point(A).  ((f  a)  =  b  +  y)))
8.  b  :  Point(B)
9.  a@0  :  |K|
10.  a  :  Point(A)
11.  (f  a)  =  b
\mvdash{}  \mexists{}a:Point(A).  ((f  a)  =  a@0  *  b)


By

---

Latex:
(D  0  With  \mkleeneopen{}a@0  *  a\mkleeneclose{}    THEN  Auto  THEN  DVar  `f'  THEN  Auto)

---

Home Index