---

Step * of Lemma r2-det_functionality

∀[p,q,r,p',q',r':ℝ^2].  (|pqr| = |p'q'r'|) supposing (req-vec(2;r;r') and req-vec(2;q;q') and req-vec(2;p;p'))
BY
{ (Auto THEN All (Unfold `req-vec`)) }

1
1. p : ℝ^2
2. q : ℝ^2
3. r : ℝ^2
4. p' : ℝ^2
5. q' : ℝ^2
6. r' : ℝ^2
7. ∀i:ℕ2. ((p i) = (p' i))
8. ∀i:ℕ2. ((q i) = (q' i))
9. ∀i:ℕ2. ((r i) = (r' i))
⊢ |pqr| = |p'q'r'|

---

Latex:

---

Latex:
\mforall{}[p,q,r,p',q',r':\mBbbR{}\^{}2].
    (|pqr|  =  |p'q'r'|)  supposing  (req-vec(2;r;r')  and  req-vec(2;q;q')  and  req-vec(2;p;p'))


By

---

Latex:
(Auto  THEN  All  (Unfold  `req-vec`))

---

Home Index