Step * 1 1 1 2 1 1 1 of Lemma not-proj-sep-iff-proj-eq


1. : ℕ
2. : ℙ^n
3. : ℙ^n
4. ∀i:ℕ1. ((u(a) i) (u(b) i))
5. : ℕ1
6. ((r1/||a||) (a i)) ((r1/||b||) (b i))
7. (((r1/||a||) (a i)) ||a||) (((r1/||b||) (b i)) ||a||)
⊢ (a i) ((||a||/||b||) (b i))
BY
(nRNorm (-1) THENA Auto) }

1
1. : ℕ
2. : ℙ^n
3. : ℙ^n
4. ∀i:ℕ1. ((u(a) i) (u(b) i))
5. : ℕ1
6. ((r1/||a||) (a i)) ((r1/||b||) (b i))
7. (a i) ((b i) (||a||/||b||))
⊢ (a i) ((||a||/||b||) (b i))


Latex:


Latex:

1.  n  :  \mBbbN{}
2.  a  :  \mBbbP{}\^{}n
3.  b  :  \mBbbP{}\^{}n
4.  \mforall{}i:\mBbbN{}n  +  1.  ((u(a)  i)  =  (u(b)  i))
5.  i  :  \mBbbN{}n  +  1
6.  ((r1/||a||)  *  (a  i))  =  ((r1/||b||)  *  (b  i))
7.  (((r1/||a||)  *  (a  i))  *  ||a||)  =  (((r1/||b||)  *  (b  i))  *  ||a||)
\mvdash{}  (a  i)  =  ((||a||/||b||)  *  (b  i))


By


Latex:
(nRNorm  (-1)  THENA  Auto)




Home Index