---

Step * of Lemma qdot-linear2

∀[as,bs:ℚ List]. ∀[r:ℚ].  qdot(as;qv-mul(r;bs)) = (r * qdot(as;bs)) ∈ ℚ supposing dimension(as) = dimension(bs) ∈ ℤ
BY
{ xxx(Auto
      THEN xxx(Unfold `qdot` 0
               THEN (RWO "prod_sum_l_q" 0 THENA (Auto THEN Fold `qv-dim` 0 THEN Auto THEN RWO "dim-qv-mul" 0 THEN Auto))
               THEN ((EqCD THEN Auto) THEN RWO "select-qv-mul" 0)
               THEN Auto
               THEN All (Unfold `qv-dim`)
               THEN QNorm 0
               THEN Auto)xxx
      )xxx }

---

Latex:

---

Latex:
\mforall{}[as,bs:\mBbbQ{}  List].  \mforall{}[r:\mBbbQ{}].
    qdot(as;qv-mul(r;bs))  =  (r  *  qdot(as;bs))  supposing  dimension(as)  =  dimension(bs)


By

---

Latex:
xxx(Auto
        THEN  xxx(Unfold  `qdot`  0
                          THEN  (RWO  "prod\_sum\_l\_q"  0
                                      THENA  (Auto  THEN  Fold  `qv-dim`  0  THEN  Auto  THEN  RWO  "dim-qv-mul"  0  THEN  Auto)
                                      )
                          THEN  ((EqCD  THEN  Auto)  THEN  RWO  "select-qv-mul"  0)
                          THEN  Auto
                          THEN  All  (Unfold  `qv-dim`)
                          THEN  QNorm  0
                          THEN  Auto)xxx
        )xxx

---

Home Index