---

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

∀[K:Rng]. ∀A:VectorSpace(K). ∀[B:VectorSpace(K)]. ∀[f:A ⟶ B].  vs-subspace(K;B;b.b ∈ Img(f))
BY
{ (Auto THEN RepUR ``vs-subspace vs-map-image`` 0 THEN Auto THEN ExRepD) }

1
1. [K] : Rng
2. A : VectorSpace(K)
3. [B] : VectorSpace(K)
4. [f] : A ⟶ B
⊢ ∃a:Point(A). ((f a) = 0 ∈ Point(B))

2
1. [K] : Rng
2. A : VectorSpace(K)
3. [B] : VectorSpace(K)
4. [f] : A ⟶ B
5. a2 : Point(A)
6. (f a2) = 0 ∈ Point(B)
7. b : Point(B)
8. y : Point(B)
9. a1 : Point(A)
10. (f a1) = b ∈ Point(B)
11. a : Point(A)
12. (f a) = y ∈ Point(B)
⊢ ∃a:Point(A). ((f a) = b + y ∈ Point(B))

3
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))

---

Latex:

---

Latex:
\mforall{}[K:Rng].  \mforall{}A:VectorSpace(K).  \mforall{}[B:VectorSpace(K)].  \mforall{}[f:A  {}\mrightarrow{}  B].    vs-subspace(K;B;b.b  \mmember{}  Img(f))


By

---

Latex:
(Auto  THEN  RepUR  ``vs-subspace  vs-map-image``  0  THEN  Auto  THEN  ExRepD)

---

Home Index