---

Step * of Lemma vs-subspace_functionality

∀K:RngSig. ∀vs:VectorSpace(K).
  ∀[P,Q:Point(vs) ⟶ ℙ].  ((∀x:Point(vs). (P[x] ⇐⇒ Q[x])) ⇒ {vs-subspace(K;vs;x.P[x]) ⇒ vs-subspace(K;vs;x.Q[x])})
BY
{ (Auto THEN (D 0 THENA Auto) THEN RepeatFor 2 (ParallelLast)) }

1
1. K : RngSig
2. vs : VectorSpace(K)
3. [P] : Point(vs) ⟶ ℙ
4. [Q] : Point(vs) ⟶ ℙ
5. ∀x:Point(vs). (P[x] ⇐⇒ Q[x])
6. (∀x,y:Point(vs).  (P[x] ⇒ P[y] ⇒ P[x + y])) ∧ (∀x:Point(vs). ∀a:|K|.  (P[x] ⇒ P[a * x]))
7. P[0]
⊢ Q[0]

2
1. K : RngSig
2. vs : VectorSpace(K)
3. [P] : Point(vs) ⟶ ℙ
4. [Q] : Point(vs) ⟶ ℙ
5. ∀x:Point(vs). (P[x] ⇐⇒ Q[x])
6. P[0]
7. (∀x,y:Point(vs).  (P[x] ⇒ P[y] ⇒ P[x + y])) ∧ (∀x:Point(vs). ∀a:|K|.  (P[x] ⇒ P[a * x]))
⊢ (∀x,y:Point(vs).  (Q[x] ⇒ Q[y] ⇒ Q[x + y])) ∧ (∀x:Point(vs). ∀a:|K|.  (Q[x] ⇒ Q[a * x]))

---

Latex:

---

Latex:
\mforall{}K:RngSig.  \mforall{}vs:VectorSpace(K).
    \mforall{}[P,Q:Point(vs)  {}\mrightarrow{}  \mBbbP{}].
        ((\mforall{}x:Point(vs).  (P[x]  \mLeftarrow{}{}\mRightarrow{}  Q[x]))  {}\mRightarrow{}  \{vs-subspace(K;vs;x.P[x])  {}\mRightarrow{}  vs-subspace(K;vs;x.Q[x])\})


By

---

Latex:
(Auto  THEN  (D  0  THENA  Auto)  THEN  RepeatFor  2  (ParallelLast))

---

Home Index