---

Step * of Lemma qdot-linear

∀[as,bs,cs:ℚ List].
  qdot(as;qv-add(bs;cs)) = (qdot(as;bs) + qdot(as;cs)) ∈ ℚ 
  supposing (dimension(as) = dimension(bs) ∈ ℤ) ∧ (dimension(as) = dimension(cs) ∈ ℤ)
BY
{ TACTIC:(Auto
          THEN Unfold `qdot` 0
          THEN RWO "sum_plus_q<" 0⋅
          THEN Auto
          THEN Try ((Fold `qv-dim` 0 THEN Auto THEN RWO "dim-qv-add" 0 THEN Auto))
          THEN ((EqCD THEN Auto) THEN RWO "select-qv-add" 0 THEN Auto THEN All (Unfold `qv-dim`) THEN QNorm 0)⋅) }

---

Latex:

---

Latex:
\mforall{}[as,bs,cs:\mBbbQ{}  List].
    qdot(as;qv-add(bs;cs))  =  (qdot(as;bs)  +  qdot(as;cs)) 
    supposing  (dimension(as)  =  dimension(bs))  \mwedge{}  (dimension(as)  =  dimension(cs))


By

---

Latex:
TACTIC:(Auto
                THEN  Unfold  `qdot`  0
                THEN  RWO  "sum\_plus\_q<"  0\mcdot{}
                THEN  Auto
                THEN  Try  ((Fold  `qv-dim`  0  THEN  Auto  THEN  RWO  "dim-qv-add"  0  THEN  Auto))
                THEN  ((EqCD  THEN  Auto)
                            THEN  RWO  "select-qv-add"  0
                            THEN  Auto
                            THEN  All  (Unfold  `qv-dim`)
                            THEN  QNorm  0)\mcdot{})

---

Home Index