---

Step * 3 of Lemma vs-quotient_wf


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]))))
BY
{ (Auto
   THEN DVar `x'
   THEN Try (DVar `y')
   THEN Try (DVar `z')
   THEN (RW VSNormC 0 THENA Auto)
   THEN EqTypeCD
   THEN Auto
   THEN RWW "vs-mul-linear vs-mul-one vs-mul-zero vs-mul-mul vs-mul-add" 0
   THEN EAuto 2
   THEN RW VSNormC 0
   THEN EAuto 2) }

---

Latex:

---

Latex:

1.  K  :  CRng
2.  vs  :  VectorSpace(K)
3.  P  :  Point(vs)  {}\mrightarrow{}  \mBbbP{}
4.  vs-subspace(K;vs;z.P[z])
5.  EquivRel(Point(vs);x,y.x  =  y  mod  (z.P[z]))
6.  Point(vs)  \msubseteq{}r  (x,y:Point(vs)//x  =  y  mod  (z.P[z]))
\mvdash{}  (\mforall{}x,y,z:x,y:Point(vs)//x  =  y  mod  (z.P[z]).    (x  +  y  +  z  =  x  +  y  +  z))
\mwedge{}  (\mforall{}x,y:x,y:Point(vs)//x  =  y  mod  (z.P[z]).    (x  +  y  =  y  +  x))
\mwedge{}  (\mforall{}k:|K|.  \mforall{}x,y:x,y:Point(vs)//x  =  y  mod  (z.P[z]).    (k  *  x  +  y  =  k  *  x  +  k  *  y))
\mwedge{}  (\mforall{}x:x,y:Point(vs)//x  =  y  mod  (z.P[z]).  (1  *  x  =  x))
\mwedge{}  (\mforall{}x:x,y:Point(vs)//x  =  y  mod  (z.P[z]).  (0  *  x  =  0))
\mwedge{}  (\mforall{}x:x,y:Point(vs)//x  =  y  mod  (z.P[z]).  \mforall{}k,b:|K|.    (k  *  b  *  x  =  k  *  b  *  x))
\mwedge{}  (\mforall{}x:x,y:Point(vs)//x  =  y  mod  (z.P[z]).  \mforall{}k,b:|K|.    (k  +K  b  *  x  =  k  *  x  +  b  *  x))


By

---

Latex:
(Auto
  THEN  DVar  `x'
  THEN  Try  (DVar  `y')
  THEN  Try  (DVar  `z')
  THEN  (RW  VSNormC  0  THENA  Auto)
  THEN  EqTypeCD
  THEN  Auto
  THEN  RWW  "vs-mul-linear  vs-mul-one  vs-mul-zero  vs-mul-mul  vs-mul-add"  0
  THEN  EAuto  2
  THEN  RW  VSNormC  0
  THEN  EAuto  2)

---

Home Index