---

Step * of Lemma proj-sep-implies

∀n:ℕ. ∀a,b:ℙ^n.  (a ≠ b ⇒ (∃i,j:ℕn + 1. (a i) * (b j) ≠ (a j) * (b i)))
BY
{ (Auto
   THEN (InstLemma `Cauchy-Schwarz-strict` [⌜n + 1⌝;⌜a⌝;⌜b⌝]⋅ THENA Auto)
   THEN D -1
   THEN Thin (-2)
   THEN (D -1 THENM (RepeatFor 2 (ParallelLast) THEN BLemma `rneq-symmetry` THEN Auto))
   THEN ((BLemma `Cauchy-Schwarz-non-equality` THEN Auto THEN D -1 THEN (All (RWW "real-vec-sep-iff-rneq") THENA Auto))
         THENL [ParallelOp -2; ParallelLast]
   )) }

1
1. n : ℕ
2. a : ℙ^n
3. b : ℙ^n
4. i : ℕn + 1
5. u(a) i ≠ u(b) i
6. ∃i:ℕn + 1. u(a) i ≠ r(-1)*u(b) i
⊢ a i ≠ (||a||/||b||)*b i

2
1. n : ℕ
2. a : ℙ^n
3. b : ℙ^n
4. ∃i:ℕn + 1. u(a) i ≠ u(b) i
5. i : ℕn + 1
6. u(a) i ≠ r(-1)*u(b) i
⊢ a i ≠ (-(||a||)/||b||)*b i

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}a,b:\mBbbP{}\^{}n.    (a  \mneq{}  b  {}\mRightarrow{}  (\mexists{}i,j:\mBbbN{}n  +  1.  (a  i)  *  (b  j)  \mneq{}  (a  j)  *  (b  i)))


By

---

Latex:
(Auto
  THEN  (InstLemma  `Cauchy-Schwarz-strict`  [\mkleeneopen{}n  +  1\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  Thin  (-2)
  THEN  (D  -1  THENM  (RepeatFor  2  (ParallelLast)  THEN  BLemma  `rneq-symmetry`  THEN  Auto))
  THEN  ((BLemma  `Cauchy-Schwarz-non-equality`
                THEN  Auto
                THEN  D  -1
                THEN  (All  (RWW  "real-vec-sep-iff-rneq")  THENA  Auto))
              THENL  [ParallelOp  -2;  ParallelLast]
  ))

---

Home Index