Hi Mingli, It's very good that you have a paper to follow, and very good that you set yourself as a target to prove another of the "100 theorems"! Good luck, and don't hesitate to shout for help whenever you feel blocked, I'm sure you'll find many willing to help!
The title of the paper is "A very simple proof", but not everything is as simple as it claims ;-) Very very quickly surveying what you might need: It seems you're right that we do not have the 3D cross product in Metamath yet. That's probably a very good addition! (and absolutely necessary for that proof) To express the Euclidean space in 3 dimensions, you can use ` ( EEhil ` 3 )` . It is defined as ` ( RR^ ( 1 ... 3 ) ) `, and that's a structure which is also a vector space. Then, for example, the set of quadratic forms over RR^3 will be ` ( QFrm ` ( EEhil ` 3 ) ) ` (once you've defined it!). We already have quite some matrix algebra, defined by Stefan O'Rear and Alexander Van der Vekens. Alexander has already introduced the concept of "linear dependency" as `linDepS` (see ~df-lindeps). Norm has a whole chapter about projective geometry, but unfortunately I don't understand it, I can't tell whether it could be useful. I hope this helps somehow! BR, _ Thierry On 06/02/2022 11:25, Mingli Yuan wrote:
Thanks, Alex and vvs Quadratic form is widely used, but looks like it is still missing in metamath. I guess I need the bilinear condition but I'm not sure about it. In fact, following paper[1], I am trying to solve Pascal's Hexagon theorem. If not wrong, I did not see too many obstacles for the formalization of the simple proof. The next step is to introduce homogeneous coordinates which connect conic sections in 2d with quadratic form in 3d. And then by some algebraic property of cross product in 3d space to prove the theorem. (we still do not have cross product in 3d?) Maybe difficult for a newbie to solve, at least it is a good chance for exercises. So far the learning curve is a little bit steep because a lot of conventions are not documented? But the community is very nice, which reminds me of Norm. [1]: A very simple proof of Pascal’s hexagon theorem and some applications by Nedeljko Stefanovic and Milos Milosevic On Sun, Feb 6, 2022 at 7:10 AM vvs <[email protected]> wrote: Hi Mingli, (2) How can we express something like a type with parameter and the initialization of a type with parameter. I'm not an expert, so don't take my word for it. But let me guess. Haskell is based on simple type theory while set.mm <http://set.mm> is ZFC, i.e. set theory. They are different beasts. You can embed type theory, of course, but that would not be set.mm <http://set.mm> anymore, IMHO. But maybe some real expert will say that I'm telling nonsensicality and this should be easy to do :) -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/4bef40e5-3ab7-402d-850c-e08aaeb0edcan%40googlegroups.com <https://groups.google.com/d/msgid/metamath/4bef40e5-3ab7-402d-850c-e08aaeb0edcan%40googlegroups.com?utm_medium=email&utm_source=footer>. -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAGDRuAhT3ZADrOrPF3%3D9nVv3SZCVj8ZVh5_Rv%3D%2BRZMErfqvHYQ%40mail.gmail.com <https://groups.google.com/d/msgid/metamath/CAGDRuAhT3ZADrOrPF3%3D9nVv3SZCVj8ZVh5_Rv%3D%2BRZMErfqvHYQ%40mail.gmail.com?utm_medium=email&utm_source=footer>.
-- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/4c69763f-314e-266a-cd54-a458b70432d9%40gmx.net.
