---

Step * of Lemma vs-quotient_wf

∀[K:CRng]. ∀[vs:VectorSpace(K)]. ∀[P:Point(vs) ⟶ ℙ].  vs//z.P[z] ∈ VectorSpace(K) supposing vs-subspace(K;vs;z.P[z])
BY
{ (Auto
   THEN Unfold `vs-quotient` 0
   THEN (Assert EquivRel(Point(vs);x,y.x = y mod (z.P[z])) BY
               EAuto 1)
   THEN (Assert Point(vs) ⊆r (x,y:Point(vs)//x = y mod (z.P[z])) BY
               Auto)
   THEN MemCD
   THEN Try (Complete (Auto))) }

1
.....subterm..... T:t
3:n
1. K : CRng
2. vs : VectorSpace(K)
3. P : Point(vs) ⟶ ℙ
4. vs-subspace(K;vs;z.P[z])
5. EquivRel(Point(vs);x,y.x = y mod (z.P[z]))
6. Point(vs) ⊆r (x,y:Point(vs)//x = y mod (z.P[z]))
7. x : x,y:Point(vs)//x = y mod (z.P[z])
8. y : x,y:Point(vs)//x = y mod (z.P[z])
⊢ x + y ∈ x,y:Point(vs)//x = y mod (z.P[z])

2
.....subterm..... T:t
4:n
1. K : CRng
2. vs : VectorSpace(K)
3. P : Point(vs) ⟶ ℙ
4. vs-subspace(K;vs;z.P[z])
5. EquivRel(Point(vs);x,y.x = y mod (z.P[z]))
6. Point(vs) ⊆r (x,y:Point(vs)//x = y mod (z.P[z]))
7. k : |K|
8. z : x,y:Point(vs)//x = y mod (z.P[z])
⊢ k * z ∈ x,y:Point(vs)//x = y mod (z.P[z])

3
1. K : CRng
2. vs : VectorSpace(K)
3. P : Point(vs) ⟶ ℙ
4. vs-subspace(K;vs;z.P[z])
5. EquivRel(Point(vs);x,y.x = y mod (z.P[z]))
6. Point(vs) ⊆r (x,y:Point(vs)//x = y mod (z.P[z]))
⊢ (∀x,y,z:x,y:Point(vs)//x = y mod (z.P[z]).  (x + y + z = x + y + z ∈ (x,y:Point(vs)//x = y mod (z.P[z]))))
∧ (∀x,y:x,y:Point(vs)//x = y mod (z.P[z]).  (x + y = y + x ∈ (x,y:Point(vs)//x = y mod (z.P[z]))))
∧ (∀k:|K|. ∀x,y:x,y:Point(vs)//x = y mod (z.P[z]).  (k * x + y = k * x + k * y ∈ (x,y:Point(vs)//x = y mod (z.P[z]))))
∧ (∀x:x,y:Point(vs)//x = y mod (z.P[z]). (1 * x = x ∈ (x,y:Point(vs)//x = y mod (z.P[z]))))
∧ (∀x:x,y:Point(vs)//x = y mod (z.P[z]). (0 * x = 0 ∈ (x,y:Point(vs)//x = y mod (z.P[z]))))
∧ (∀x:x,y:Point(vs)//x = y mod (z.P[z]). ∀k,b:|K|.  (k * b * x = k * b * x ∈ (x,y:Point(vs)//x = y mod (z.P[z]))))
∧ (∀x:x,y:Point(vs)//x = y mod (z.P[z]). ∀k,b:|K|.  (k +K b * x = k * x + b * x ∈ (x,y:Point(vs)//x = y mod (z.P[z]))))

---

Latex:

---

Latex:
\mforall{}[K:CRng].  \mforall{}[vs:VectorSpace(K)].  \mforall{}[P:Point(vs)  {}\mrightarrow{}  \mBbbP{}].
    vs//z.P[z]  \mmember{}  VectorSpace(K)  supposing  vs-subspace(K;vs;z.P[z])


By

---

Latex:
(Auto
  THEN  Unfold  `vs-quotient`  0
  THEN  (Assert  EquivRel(Point(vs);x,y.x  =  y  mod  (z.P[z]))  BY
                          EAuto  1)
  THEN  (Assert  Point(vs)  \msubseteq{}r  (x,y:Point(vs)//x  =  y  mod  (z.P[z]))  BY
                          Auto)
  THEN  MemCD
  THEN  Try  (Complete  (Auto)))

---

Home Index