---

Step * of Lemma rn-ip_wf

No Annotations
∀[n:{2...}]. (ipℝ^n ∈ InnerProductSpace)
BY
{ (((D 0 THENA Auto) THEN (Assert vecℝ^n ∈ RealVectorSpace BY Auto))
   THEN Unfold `rn-ip` 0
   THEN MemCD
   THEN Try (Trivial)
   THEN RepUR ``rv-n rn-ss mk-ss ss-eq ss-sep ss-point mk-real-vector-space`` 0
   THEN RepUR ``rv-add rv-mul rv-0`` 0
   THEN Try ((MemTypeCD THEN Reduce 0 THEN Auto))
   THEN Auto) }

1
1. n : {2...}
2. vecℝ^n ∈ RealVectorSpace
3. x1 : ℝ^n
4. x2 : ℝ^n
5. y1 : ℝ^n
6. y2 : ℝ^n
7. ¬x1 ≠ x2
8. ¬y1 ≠ y2
⊢ x1⋅y1 = x2⋅y2

---

Latex:

---

Latex:
No  Annotations
\mforall{}[n:\{2...\}].  (ip\mBbbR{}\^{}n  \mmember{}  InnerProductSpace)


By

---

Latex:
(((D  0  THENA  Auto)  THEN  (Assert  vec\mBbbR{}\^{}n  \mmember{}  RealVectorSpace  BY  Auto))
  THEN  Unfold  `rn-ip`  0
  THEN  MemCD
  THEN  Try  (Trivial)
  THEN  RepUR  ``rv-n  rn-ss  mk-ss  ss-eq  ss-sep  ss-point  mk-real-vector-space``  0
  THEN  RepUR  ``rv-add  rv-mul  rv-0``  0
  THEN  Try  ((MemTypeCD  THEN  Reduce  0  THEN  Auto))
  THEN  Auto)

---

Home Index