Step
*
of Lemma
vs-iso-iff-kernel-0
∀[K:Rng]. ∀[A,B:VectorSpace(K)].
(A ≅ B
⇐⇒ ∃f:A ⟶ B. ((∀a:Point(A). (a ∈ Ker(f)
⇐⇒ a = 0 ∈ Point(A))) ∧ Surj(Point(A);Point(B);f)))
BY
{ Auto }
1
1. [K] : Rng
2. [A] : VectorSpace(K)
3. [B] : VectorSpace(K)
4. A ≅ B
⊢ ∃f:A ⟶ B. ((∀a:Point(A). (a ∈ Ker(f)
⇐⇒ a = 0 ∈ Point(A))) ∧ Surj(Point(A);Point(B);f))
2
1. [K] : Rng
2. [A] : VectorSpace(K)
3. [B] : VectorSpace(K)
4. ∃f:A ⟶ B. ((∀a:Point(A). (a ∈ Ker(f)
⇐⇒ a = 0 ∈ Point(A))) ∧ Surj(Point(A);Point(B);f))
⊢ A ≅ B
Latex:
Latex:
\mforall{}[K:Rng]. \mforall{}[A,B:VectorSpace(K)].
(A \mcong{} B \mLeftarrow{}{}\mRightarrow{} \mexists{}f:A {}\mrightarrow{} B. ((\mforall{}a:Point(A). (a \mmember{} Ker(f) \mLeftarrow{}{}\mRightarrow{} a = 0)) \mwedge{} Surj(Point(A);Point(B);f)))
By
Latex:
Auto
Home
Index