Hi :)I recently discovered metamath and have been reading the book. I think it's a great project as having computer feedback on proofs is a really powerful tool, one which I wish I had access to during my PhD. I'm hopeful that I might be able to add some proofs to set.mm which would be great. So far I understand about the proof assistant and I was able to reprove eftcl using it which felt pretty good. Here's a bunch of questions I have about how to actually contribute a new proof, any help would be appreciated.1. Presumably the first step is to find some material to contribute. My background is in PDE's and the more highschoolish the material the better (trigonometry, basic calculus etc) and I'm also ok at analysis and functional analysis topics. So what sort of things are at the boundary of metamath and need to be added? Are there any books which people want programmed in?
2. Once I find a proof to put in presumably the first step is to make sure it has no skipped steps so far as metamath is concerned, I don't know how hard this will be. Relevant to pt 1 are there any materials which have proofs already in very rigorous form which are easier to program in?
3. Say I have a theorem and the proof on paper. I think to add it to set.mm I need to first edit the text file to include the theorem. Would I just try to copy one of the current theorems, give it a comment, a name and put in the result formally? Where does it go, just in the most appropriate section?
4. This is a main issue. Say I have a theorem I want to prove and I know what steps I need to find in set.mm to substitute into it, how do I go about finding them? For example when reproving eftcl I just used the labels provided on the web page but if I had a new proof how would I find the labels for certain results? For example I didn't know "Closure law for division" was the name of what I was looking for so it was pretty difficult to try to find divcld (which is what is needed for that proof). Is there any advice on the best way of finding things? Is it trying to write out what you want in proper notation and searching inside the metamth program?
5. I guess after that it's a case of entering the proof into metamath, verifying, saving and writing to the source. What happens after this? Would I make a github pull request to get the proof included in the main repo? Can I make pull requests directly to the main repo or do I need to fork?
Maybe it would be good to try to make a beginners guide to contributing proofs? The book has a guide to proving demo.mm however that is quite a different process from this.
I wonder if maybe 57. Heron's formula is a good target as it doesn't seem that complicated and is on the 100 list. If anyone else is already working on it I am happy to look elsewhere.
I found this proof on wikipedia which seems really simple, if that's not a stupid place to look. It rests on the law of cosines (lawcos) and sinccossq which are in the database but I couldn't find Area of a Triangle = 1/2 base * height, is that in there? Also I'm also not sure how to get the opposite of a triangle = hypotenuse sin theta. After that it looks mostly like algebra which should be ok once I find the right substitutions.
Am I headed in the right direction at all? I hope it's ok to ask so many questions.
$( <MM> <PROOF_ASST> THEOREM=heron LOC_AFTER=
aaa::df-area |- area
= ( &S5
e. { &S4
e. ~P ( RR X. RR )
| ( A. &S3
e. RR
( &S4 " { &S3 } ) e. ( `' vol " RR )
/\ ( &S3
e. RR
|-> ( vol ` ( &S4 " { &S3 } ) ) )
e. L^1 ) }
|-> S. RR
( vol ` ( &S5 " { &S3 } ) )
_d &S3 )
!d1:: |- F
= ( &S1
e. ( CC \ { 0 } )
, &S2
e. ( CC \ { 0 } )
|-> ( Im ` ( log ` ( &S2 / &S1 ) ) ) )
!d2:: |- a = ( abs ` ( A - 0 ) )
!d3:: |- b = ( abs ` ( B - 0 ) )
!d4:: |- c = ( abs ` ( B - A ) )
!d5:: |- O = ( ( A - 0 ) F ( B - 0 ) )
10:d1,d2,d3,d4,d5:lawcos
|- ( ( ( B e. CC /\ A e. CC /\ 0 e. CC )
/\ ( B =/= 0 /\ A =/= 0 ) )
-> ( c ^ 2 )
= ( ( ( a ^ 2 ) + ( b ^ 2 ) )
-
( 2 x. ( ( a x. b ) x. ( cos ` O ) ) ) ) )
*if O is complex then so are sin^2 O and cos^2
20::sincl |- ( O e. CC -> ( sin ` O ) e. CC )
30::sqcl |- ( ( sin ` O ) e. CC -> ( ( sin ` O ) ^ 2 ) e. CC )
40::coscl |- ( O e. CC -> ( cos ` O ) e. CC )
50::sqcl |- ( ( cos ` O ) e. CC -> ( ( cos ` O ) ^ 2 ) e. CC )
*if you have A + B - B = C then A = C, strip this down so the conditions are just O
100::pncan |- ( ( ( ( sin ` O ) ^ 2 ) e. CC
/\ ( ( cos ` O ) ^ 2 ) e. CC )
-> ( ( ( ( sin ` O ) ^ 2 ) + ( ( cos ` O ) ^ 2 ) )
-
( ( cos ` O ) ^ 2 ) )
= ( ( sin ` O ) ^ 2 ) )
101:30,100:sylan |- ( ( ( sin ` O ) e. CC /\ ( ( cos ` O ) ^ 2 ) e. CC )
-> ( ( ( ( sin ` O ) ^ 2 ) + ( ( cos ` O ) ^ 2 ) ) - ( ( cos ` O ) ^ 2 ) ) = ( ( sin ` O ) ^ 2 ) )
102:20,101:sylan |- ( ( O e. CC /\ ( ( cos ` O ) ^ 2 ) e. CC )
-> ( ( ( ( sin ` O ) ^ 2 ) + ( ( cos ` O ) ^ 2 ) ) - ( ( cos ` O ) ^ 2 ) ) = ( ( sin ` O ) ^ 2 ) )
103:50,102:sylan2 |- ( ( O e. CC /\ ( cos ` O ) e. CC )
-> ( ( ( ( sin ` O ) ^ 2 ) + ( ( cos ` O ) ^ 2 ) ) - ( ( cos ` O ) ^ 2 ) ) = ( ( sin ` O ) ^ 2 ) )
104:40,103:sylan2 |- ( ( O e. CC /\ O e. CC )
-> ( ( ( ( sin ` O ) ^ 2 ) + ( ( cos ` O ) ^ 2 ) ) - ( ( cos ` O ) ^ 2 ) ) = ( ( sin ` O ) ^ 2 ) )
105:104:anidms |- ( O e. CC
-> ( ( ( ( sin ` O ) ^ 2 ) + ( ( cos ` O ) ^ 2 ) ) - ( ( cos ` O ) ^ 2 ) ) = ( ( sin ` O ) ^ 2 ) )
*start with sin^2 + cos^2 = 1
110::sincossq |- ( O e. CC -> ( ( ( sin ` O ) ^ 2 ) + ( ( cos ` O ) ^ 2 ) ) = 1 )
*add cos^2 to both sides
115:110:oveq1d |- ( O e. CC -> ( ( ( ( sin ` O ) ^ 2 ) + ( ( cos ` O ) ^ 2 ) ) - ( ( cos ` O ) ^ 2 ) )
= ( 1 - ( ( cos ` O ) ^ 2 ) ) )
*simplify
120:105,115:eqtr3d |- ( O e. CC -> ( ( sin ` O ) ^ 2 ) = ( 1 - ( ( cos ` O ) ^ 2 ) ) )
*Use area formula
200:: |- ( ( A e. ( RR X. RR ) /\ B e. ( RR X. RR ) /\ O e. CC /\ ( a e. CC /\ b e. CC ) )
-> ( ( 1 / 2 ) x. ( A X. B ) ) = ( ( ( ( 1 / 2 ) x. a ) x. b ) x. ( sin ` O ) ) )
*square both sides
220:200:oveq1d |- ( ( A e. ( RR X. RR ) /\ B e. ( RR X. RR ) /\ O e. CC /\ ( a e. CC /\ b e. CC ) )
-> ( ( ( 1 / 2 ) x. ( A X. B ) ) ^ 2 ) = ( ( ( ( ( 1 / 2 ) x. a ) x. b ) x. ( sin ` O ) ) ^ 2 ) )
*distribute squared
230:220: |- ( ( A e. ( RR X. RR ) /\ B e. ( RR X. RR ) /\ O e. CC /\ ( a e. CC /\ b e. CC ) )
-> ( ( ( 1 / 2 ) x. ( A X. B ) ) ^ 2 ) = ( ( ( ( ( 1 / 2 ) x. a ) x. b ) ^ 2 ) x. ( ( sin ` O ) ^ 2 ) ) )
1000:: |- s = ( ( ( a + b ) + c ) / 2 )
qed:: |- ( ( 1 / 2 ) x. ( A X. B ) )
= ( ( ( ( s x. ( s - a ) ) x. ( s - b ) ) x. ( s - c ) ) ^ ( 1 / 2 ) )
$)
Hi Jon,
Let me try to answer, I hope I'll be clear enough:
` F ` is the signed angle construct (as used in ~ ang180 )
Alternatively, you could of course add this ' F = ... ' formula
as a hypothesis in the final theorem. It does not make much sense
if ` F ` actually appears nowhere in the theorem, so then you
could drop it in a second version (again, using ~ eqid) - but it's
more elegant to hide it throughout.
You can take care of steps d2~d4 in a similar way (using ~ eqid).
This will result in having ` ( A - 0 ) ` in your formula: I would
recommend simplifying it to ` A ` (using ~ subid1d) before further
manipulating the formula. This exercise may be a bit annoying, it
may have been avoided if a "deduction" formulation had been used
for ~ lawcos.
Thank you for the helpful replies and encouragement. I've been playing a bit with mmj2 a bit this morning and have more newb questions. Please feel free to take time to answer or not to answer, I don't want to become a burden.
Firstly I was thinking about what you said Mario about triangles and areas and thought maybe a good idea is to state Heron's result in terms of vectors and the cross product. So a triangle is made of two vectors, A and B, and the area of it is 1/2 A X. B. What do you think? Is this a reasonable approach? Diagram
Here is my first scribblings in mmj2, it's not so good so far. Here are my questions with it.
1. with lawcos what is d1 about? I am a bit confused by it. Also how do I fill in the theorems for d1 - d5, for example it should be d2::something |-, what is the something?
2. With step 115 I wanted to just take something away from both sides, is there a way of doing this? I was hoping it would fill in automatically.
3. ovq1d filled in which was great :) Maybe I should be using sqr thoughout though, I am not sure, is the power ( 1 / 2 ) or sqr preferable?
4. 140. I think is false, which is a problem, sqr (a ^ 2) = +- a however I only want the positive branch. I am not sure what to do about this. I was wondering about squaring both sides of 500 and working from there but I will need to take a sqr at the end.
$( <MM> <PROOF_ASST> THEOREM=heron LOC_AFTER=
!d1:: |- F
= ( &S1
e. ( CC \ { 0 } )
, &S2
e. ( CC \ { 0 } )
|-> ( Im ` ( log ` ( &S2 / &S1 ) ) ) )
!d2:: |- a = ( abs ` ( A - 0 ) )
!d3:: |- b = ( abs ` ( B - 0 ) )
!d4:: |- c = ( abs ` ( B - A ) )
!d5:: |- O = ( ( A - 0 ) F ( B - 0 ) )
10:d1,d2,d3,d4,d5:lawcos
|- ( ( ( B e. CC /\ A e. CC /\ 0 e. CC )
/\ ( B =/= 0 /\ A =/= 0 ) )
-> ( c ^ 2 )
= ( ( ( a ^ 2 ) + ( b ^ 2 ) )
-
( 2 x. ( ( a x. b ) x. ( cos ` O ) ) ) ) )
110::sincossq |- ( O e. CC -> ( ( ( sin ` O ) ^ 2 ) + ( ( cos ` O ) ^ 2 ) ) = 1 )
115:: |- ( O e. CC -> ( ( ( ( sin ` O ) ^ 2 ) + ( ( cos ` O ) ^ 2 ) ) - ( ( cos ` O ) ^ 2 ) )
= ( 1 - ( ( cos ` O ) ^ 2 ) ) )
120:115: |- ( O e. CC -> ( ( sin ` O ) ^ 2 ) = ( 1 - ( ( cos ` O ) ^ 2 ) ) )
130:120:oveq1d |- ( O e. CC -> ( ( ( sin ` O ) ^ 2 ) ^ ( 1 / 2 ) ) = ( ( 1 - ( ( cos ` O ) ^ 2 ) ) ^ ( 1 / 2 ) ) )
140:: |- ( O e. CC -> ( sqr ` ( O ^ 2 ) ) = O )
150:130,140: |- ( O e. CC -> ( sin ` O ) = ( ( 1 - ( ( cos ` O ) ^ 2 ) ) ^ ( 1 / 2 ) ) )
400:: |- s = ( ( ( a + b ) + c ) / 2 )
500:: |- ( ( 1 / 2 ) x. ( A X. B ) ) = ( ( ( ( 1 / 2 ) x. a ) x. b ) x. ( sin ` O ) )
qed:: |- ( ( 1 / 2 ) x. ( A X. B ) )
= ( ( ( ( s x. ( s - a ) ) x. ( s - b ) ) x. ( s - c ) ) ^ ( 1 / 2 ) )
$)
--
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 metamath+u...@googlegroups.com.
To post to this group, send email to meta...@googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.
Hi Jon,
Ok, let me try to help again.
First, obviously you've progressed well already, well done!
Still, let's get back to the basics: in your proof,
So I would first rewrite the theorem in your MM file:
${
heron.f $e |- F = ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 }
) |-> ( Im ` ( log ` ( y / x ) ) ) ) $.
heron.x $e |- X = ( abs ` ( B - C ) ) $.
heron.y $e |- Y = ( abs ` ( A - C ) ) $.
heron.z $e |- Z = ( abs ` ( A - B ) ) $.
heron.o $e |- O = ( ( B - C ) F ( A - C ) ) $.
heron.s $e |- S = ( ( ( X + Y ) + Z ) / 2 ) $.
heron.a $e |- ( ph -> A e. CC ) $.
heron.b $e |- ( ph -> B
e. CC ) $.
heron.c
$e |- ( ph -> C e. CC ) $.
heron.d
$e |- ( ph -> (
A =/= C /\ B =/= C ) ) $.
$( Heron's Formula ... $)
heron $p |- ( ph -> ( ( ( 1 / 2 ) x. ( X x. Y ) ) x. (
abs ` ( sin ` O ) ) )
= ( sqr ` ( ( S x. ( S - Z ) ) x. ( ( S - Y ) x. ( S -
Z ) ) ) ) ) $=
? $.
$}
Here, I have added in the hypothesis the definitions for F, X, Y,
Z, O (same as in the law of cosines) and for S (the semi
perimeter).
I have also added conditions to the theorem's formula: all points
of the triangle are distinct complex numbers. And I have corrected
the variables (X, Y, Z, S instead of a, b, c, s).
This way, we have a clear goal :)
Of course one may wish to prove that ( ( ( 1 / 2 ) x. ( X x. Y ) ) x. ( abs ` ( sin ` O ) ) ) is indeed the area of the triangle, but that's another story, let's leave that for your second proof ;-)
The formulation I chose is a "deduction" one, meaning I also introduce a wff variable ph. This shall make proof writing a bit less tedious, since you will not have to repeat "( A e. CC /\ B e. CC /\ ..." etc. at the start of each line.You should be able to prove things like ( ph -> O e. RR ) easily, you're almost there (hint: use ~ ovmpt2d for your step o2).
Your next step would be using ~ fveq2d and ~ absre, to get something like:
|- ( ph -> ( abs ` ( sin ` O ) ) = ( sqr ` ( ( sin ` O
) ^ 2 ) ) )
Continue like this, I believe you're on the right track!
_Can anyone help me find this? I have searched and cannot see it.( ( ( B - C ) e. CC /\ ( B - C ) =/= 0 ) -> ( B - C ) e. ( CC / { 0 } ) )
--
H1: |- ((((1/2) * x) * y) * sin O)^2 = (((1/2) * x) * y)^2 * (1 - ((x^2 + y^2 - z^2)/2)^2 / (x*y)^2)8:mulassd |- ((1/2) * x) * y = (1/2) * (x * y)6:8 |- (((1/2) * x) * y)^2 = ((1/2) * (x * y))^25:6,7 |- (((1/2) * x) * y)^2 = (1/2)^2 * (x * y)^27:mulexp |- ((1/2) * (x * y))^2 = (1/2)^2 * (x * y)^23:5 |- (((1/2) * x) * y)^2 * (1 - ((x^2 + y^2 - z^2)/2)^2 / (x*y)^2) = ((1/2)^2 * (x * y)^2) * (1 - ((x^2 + y^2 - z^2)/2)^2 / (x*y)^2)9:mulassd |- ((1/2)^2 * (x * y)^2) * (1 - ((x^2 + y^2 - z^2)/2)^2 / (x*y)^2) = (1/2)^2 * ((x * y)^2 * (1 - ((x^2 + y^2 - z^2)/2)^2 / (x*y)^2))12:mulsubdid |- (x * y)^2 * (1 - ((x^2 + y^2 - z^2)/2)^2 / (x*y)^2) = (x * y)^2 * 1 - (x * y)^2 * ((x^2 + y^2 - z^2)/2)^2 / (x*y)^2)14:mulid1d |- (x * y)^2 * 1 = (x * y)^215:divcan2d |- (x * y)^2 * ((x^2 + y^2 - z^2)/2)^2 / (x*y)^2) = ((x^2 + y^2 - z^2)/2)^213:14,15 |- (x * y)^2 * 1 - (x * y)^2 * ((x^2 + y^2 - z^2)/2)^2 / (x*y)^2) = (x * y)^2 - ((x^2 + y^2 - z^2)/2)^211:12,13 |- (x * y)^2 * (1 - ((x^2 + y^2 - z^2)/2)^2 / (x*y)^2) = (x * y)^2 - ((x^2 + y^2 - z^2)/2)^210:11 |- (1/2)^2 * ((x * y)^2 * (1 - ((x^2 + y^2 - z^2)/2)^2 / (x*y)^2)) = (1/2)^2 * ((x * y)^2 - ((x^2 + y^2 - z^2)/2)^2)4:9,10 |- ((1/2)^2 * (x * y)^2) * (1 - ((x^2 + y^2 - z^2)/2)^2 / (x*y)^2) = (1/2)^2 * ((x * y)^2 - ((x^2 + y^2 - z^2)/2)^2)2:3,4 |- (((1/2) * x) * y)^2 * (1 - ((x^2 + y^2 - z^2)/2)^2 / (x*y)^2) = (1/2)^2 * ((x * y)^2 - ((x^2 + y^2 - z^2)/2)^2)qed:1,2 |- ((((1/2) * x) * y) * sin O)^2 = (1/2)^2 * ((x * y)^2 - ((x^2 + y^2 - z^2)/2)^2)
Hey, so I think I'm going to stop doing this proof, it is just extremely painful to try and do algebra on large expressions with these tools. I am just trying to multiply up by ( 2 ^ 2 ) = 4 and it's just a nightmare of so many steps. I didn't understand when I started this proof how difficult the algebra was going to be, on wikipedia it's just 5 lines a highschooler could do so I figured it wouldn't take so long.I think these would be my thoughts about MetaMath having played around with it for 2 weeks:1. Metamath is awesome, it's amazing how many theorems there are and how much progress has been made.2. I am convinced computer assisted proofs are the future of mathematics. It always seemed insane to me that I would prove something and show it to my supervisor and if we both felt it was right then we assumed it was. Having the computer check your work is super helpful and I think in 20 years it will seem ridiculous to try and prove things by hand.
3. It would have been helpful to get a warning when I started on this proof about how long and hard it would be. If you have beginners come along maybe it is worth trying to set them a 5 line proof or something as an exercise. Basically I just waded in way too deep and got stuck and have now failed which is not such a nice experience, though I have learned a lot which is good.4. The biggest weakness of Metamath is the tooling. I think mmj2 is great and obviously has had a lot of work go into it so I want to praise that. I think there's 3 areas where it could really be improved:A. It's annoying how strict it is that there must be a gap between brackets and how it can't tell you which bracket isn't closed. When it parses the line into a tree I think there will be a point where it expects a bracket and doesn't find one so should be able to tell you that info maybe, though I am not sure.B. Using work variables is a nice system however when you fill them in it formats the result in a difficult way (with many line breaks) and so it is then a nightmare to delete all this extra whitespace to get back to a reasonable form. This is connected to the fact that the editor is not so good and you cannot wrap around lines.
On the subject of work variables it would be great if you could wrap an expression into a temporary variable and then work with this for a while and then at the end just replace that temporary variable with the expression it represents. I think that is the idea for work variables and it would be really nice if it could make things a lot easier.
C. Before anyone would seriously use metamath as a theorem prover it would need to work at a higher level, it would be amazing to have a computer algebra system or similar which let you do standard manipulations easily. I understand David you are working in this direction and the stuff you are doing looks helpful.
I had a bit of a look at Norm's talk about MM and one of the things in it is that the goal isn't to make MM into a theorem prover that working mathematicians would use. However I am sure that over the next while some tool will come to fill this position just because it is such an enormous assistance in proving things, however it is a lot of work to get to that point as it needs the whole tree of mathematics filled in and it needs to be a flexible and easy to use tool.Anyway I would love to be able to help make a really fluid tool, I can program however I am not so good with large programs already written and I don't know Java so it would be a bit difficult to help with that. I wondered about making my own tool however that is probably more work than I can accomplish so sorry about that.
--
4. The biggest weakness of Metamath is the tooling. I think mmj2 is great and obviously has had a lot of work go into it so I want to praise that. I think there's 3 areas where it could really be improved:A. It's annoying how strict it is that there must be a gap between brackets and how it can't tell you which bracket isn't closed. When it parses the line into a tree I think there will be a point where it expects a bracket and doesn't find one so should be able to tell you that info maybe, though I am not sure.
B. Using work variables is a nice system however when you fill them in it formats the result in a difficult way (with many line breaks) and so it is then a nightmare to delete all this extra whitespace to get back to a reasonable form. This is connected to the fact that the editor is not so good and you cannot wrap around lines.
On the subject of work variables it would be great if you could wrap an expression into a temporary variable and then work with this for a while and then at the end just replace that temporary variable with the expression it represents. I think that is the idea for work variables and it would be really nice if it could make things a lot easier.
C. Before anyone would seriously use metamath as a theorem prover it would need to work at a higher level, it would be amazing to have a computer algebra system or similar which let you do standard manipulations easily. I understand David you are working in this direction and the stuff you are doing looks helpful.
I had a bit of a look at Norm's talk about MM and one of the things in it is that the goal isn't to make MM into a theorem prover that working mathematicians would use. However I am sure that over the next while some tool will come to fill this position just because it is such an enormous assistance in proving things, however it is a lot of work to get to that point as it needs the whole tree of mathematics filled in and it needs to be a flexible and easy to use tool.
Anyway I would love to be able to help make a really fluid tool, I can program however I am not so good with large programs already written and I don't know Java so it would be a bit difficult to help with that. I wondered about making my own tool however that is probably more work than I can accomplish so sorry about that.
I have been thinking more about whether it is possible to directly substitute things, ( for example if A = B -> ((W x. A)/C) = ((W x. B)/C) or whatever ). Is there any way this could be defined for an arbitrary symbol string? Presumably MM is doing this sort of substitution all the time when unifying etc? If it were possible to have something like this I think it would result in a massive speedup because you can work on small pieces of a large formula and then quickly swap them.
Thanks Mario.Can I ask some questions about establishing the area of a triangle in CC? I think it would be helpful for heron and will also be needed for Pick's Theorem (though that looks very hard).
I'm not sure I really understand this thing; ∫ℝ(vol‘(𝑆 “ {𝑡})) d𝑡 As far as I understand it means that t runs from -inf to inf and is kind of all the possible areas that S could have? And then S[{t}] is any part of S which has area t, and then vol' is the inverse measure of this?
So say I had a unit square in CC, then S[{t}] = null for all t except t = 1 and at that value it's the square? As you can see I am quite confused.Further to this what is a good strategy for finding the area of a triangle? Maybe start with a step function and prove the area of a box is width x height, the have a sawtooth function like f(x) = 1 - x for x = 0..1 and 0 otherwise and integrate this? This could be extended to other triangles maybe? I don't know if this is the right sort of idea.
--
--
Here would be some of the missing pieces for step 40 - Mario, I'm curious if there is a shorter way!
600::xpimasn |- ( x e. ( 0 [,] 1 ) -> ( ( ( 0 [,] 1
) X. ( 0 [,] 1 ) ) " { x } ) = ( 0 [,] 1 ) )
610::xpima1 |- ( ( ( 0 [,] 1 ) i^i { x } ) = (/)
-> ( ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) " { x } ) = (/) )
620::disjsn |- ( ( ( 0 [,] 1 ) i^i { x } ) = (/)
<-> -. x e. ( 0 [,] 1 ) )
630:620,610:sylbir |- ( -. x e. ( 0 [,] 1 ) -> ( ( (
0 [,] 1 ) X. ( 0 [,] 1 ) ) " { x } ) = (/) )
635::ovol0 |- ( vol* ` (/) ) = 0
636::mblvol |- ( (/) e. dom vol -> ( vol ` (/)
) = ( vol* ` (/) ) )
637::0mbl |- (/) e. dom vol
638:637,636:ax-mp |- ( vol ` (/) ) = ( vol* ` (/) )
639:638,635:eqtri |- ( vol ` (/) ) = 0
641:: |- ( vol ` ( 0 [,] 1 ) ) = 1
650:600:fveq2d |- ( x e. ( 0 [,] 1 ) -> ( vol ` (
( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) " { x } ) ) = ( vol ` ( 0 [,] 1 )
) )
660:630:fveq2d |- ( -. x e. ( 0 [,] 1 ) -> ( vol
` ( ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) " { x } ) ) = ( vol ` (/) ) )
670:650,641:syl6req |- ( x e. ( 0 [,] 1 ) -> 1 = ( vol
` ( ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) " { x } ) ) )
680:660,639:syl6req |- ( -. x e. ( 0 [,] 1 ) -> 0 = ( vol ` (
( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) " { x } ) ) )
d17:670:adantl |- ( ( ( ph /\ x e. RR ) /\ x e. ( 0 [,] 1 )
) -> 1 = ( vol ` ( ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) " { x } ) )
)
d18:680:adantl |- ( ( ( ph /\ x e. RR ) /\ -. x e. ( 0 [,]
1 ) ) -> 0 = ( vol ` ( ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) " { x }
) ) )
690:d17,d18:ifeqda |- ( ( ph /\ x e. RR ) -> if ( x e. ( 0
[,] 1 ) , 1 , 0 ) = ( vol ` ( ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) " {
x } ) ) )
36:sdef:imaeq1i |- ( S " { x } ) = ( ( ( 0 [,] 1 ) X. ( 0
[,] 1 ) ) " { x } )
37:36:fveq2i |- ( vol ` ( S " { x } ) ) = ( vol ` ( ( ( 0
[,] 1 ) X. ( 0 [,] 1 ) ) " { x } ) )
39:690,37:syl6reqr |- ( ( ph /\ x e. RR ) -> ( vol ` ( S " {
x } ) ) = if ( x e. ( 0 [,] 1 ) , 1 , 0 ) )
40:39:itgeq2dv |- ( ph -> S. RR ( vol ` ( S " { x
} ) ) _d x = S. RR if ( x e. ( 0 [,] 1 ) , 1 , 0 ) _d x )
Hi Jon,
The expression ` ( S " { x } ) e. ( `' vol " RR ) ` means that `
( S " { x } ) ` is in the preimage
of ` RR ` under the function ` vol `. Theorem ~ fvimacnv
shows that this is equivalent to ` ( vol ` ( S " { x } ) ) e.
RR ` . Indeed a the measure of a set could be a
non-negative real number, or +oo, so saying that it is
real basically means saying that it is not infinite.
Another way to say it is ` ( S " { x } ) ` is Lebesgue-measurable
(see ~ df-vol).
Since the measure of ` ( S " { x } ) ` is either 0 or 1, it is
obviously always a real number.
63a::fvimacnv |- ( ( Fun vol /\ ( S " { x } ) e. dom
vol ) -> ( ( vol ` ( S " { x } ) ) e. RR <-> ( S " { x
} ) e. ( `' vol " RR ) ) )
63b::volf |- vol : dom vol --> ( 0 [,] +oo )
63c::ffun |- ( vol : dom vol --> ( 0 [,] +oo )
-> Fun vol )
63d:63b,63c:ax-mp |- Fun vol
63e:63d,62,63a:mp2an |- ( ( vol ` ( S " { x } ) ) e. RR
<-> ( S " { x } ) e. ( `' vol " RR ) )
63f::ifcl |- ( ( 1 e. RR /\ 0 e. RR ) -> if ( x e.
( 0 [,] 1 ) , 1 , 0 ) e. RR )
63g:d8,d7,63f:mp2an |- if ( x e. ( 0 [,] 1 ) , 1 , 0 ) e. RR
63h:695,63g:syl6eqel |- ( x e. RR -> ( vol ` ( S " { x } ) )
e. RR )
63i:63h,63e:sylib |- ( x e. RR -> ( S " { x } ) e. ( `'
vol " RR ) )
64:63i:rgen |- A. x e. RR ( S " { x } ) e. ( `' vol "
RR )
Hi Jon,
That's great! I The best place to share your proof would be in
your Mathbox - it's quite easy to create, and your proof would be
made available as a new theorem.
I think your next steps are the correct ones, and your suggestion to tackle the two triangles in one general case seems to be a clever choice.
I would continue your proof in RR X. RR, I think it's where area
is the most naturally expressed, and it's that expression we'll
get when we'll derive it using Fubini's
theorem.
We have ~ cnref1o
to convert back-and forth, if a proof is more convenient in CC.
_
Thierry
Hi Jon,
It's true what you need to build is a bit complex :-)
Here is maybe an easier way to describe the shape:
with
|- U = ( C + ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) )
|- V = ( E + ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) )
(And in this case, A, B, C, D, E, F in RR)
This tells that S is a set of pairs <. x , y >., with x
between A and B, and y between U and V. The trick here is that U
and V actually depend on x, so you have to think of them as U(x)
and V(x).
The coordinates of the quadrilateral are: <. A , C >. and
<. A , E >. on one side, and <. B , D >. and <. B ,
F >. on the other side.
Then if you look at ( S " { x } ), a "slice" of that
quadrilateral, you should get ( S " { x } ) = ( U [,] V ), which
Lebesgue measure you already know.
The similarities between the formulas of U and V may be exploited by some appropriate lemma.
In the end, you'll have to simplify and integrate ( V - U ) ( to be thought as V(x) - U(x) ).
BR,
_
Thierry
Thanks Thierry.I have another question, how do I evaluate the image on this set definition? Before I hadh7::areaboxg.7 |- S = ( ( A [,] B ) X. ( C [,] D ) )s1:7:imaeq1i |- ( S " { x } ) = ( ( ( A [,] B ) X. ( C [,] D ) ) " { x } )s2::xpimasn |- ( x e. ( A [,] B ) -> ( ( ( A [,] B ) X. ( C [,] D ) ) " { x } ) = ( C [,] D ) )
and also with xpima1 this gave
s11:s1,s10:eqtr4i |- ( S " { x } ) = if ( x e. ( A [,] B ) , ( C [,] D ) , (/) )
I think things should be similar this time however is there something else to use in place of xpimasn? I had a look at the various defima's but couldn't quite work it out. What would apply to
13:: |- S = { <. x , y >. | ( x e. ( A [,] B ) /\ y e. ( U [,] V ) ) }If my questions become annoying please feel free not to answer :)
--
Hi Jon,
1. Here is how I would solve your step 74:
73e::df-xp |- ( RR X. RR ) = { <. x , y >. | (
x e. RR /\ y e. RR ) }
73f:72b:ssopab2i |- { <. x , y >. | ( x e. ( A
[,] B ) /\ y e. ( U [,] V ) ) } C_ { <. x , y >. | ( x e.
RR /\ y e. RR ) }
74:73f,13,73e:3sstr4i |- S C_ ( RR X. RR )
In your mail, you cannot substitute ` t ` with ` <. x , y
>. ` because ` <. x , y >. ` is a class variable (see ~
cop) and ` t ` is a setvar variable (see ~ vt). Setvar variables
are class variables (see ~ cv), but not vice-versa.
2. Since ~ iblss2 is only written in the deduction form, you need some dummy true constant wff for ph. Your choice of 0 e. RR is as good a choice as any other. I would say the usual way for this is to use ` T. ` , the constant true wff. You can then eliminate it using ~ trud.
BR,
_
Thierry
Hi Jon,
Actually, you should not need ` x e. ( A [,] B ) ` as a
hypothesis for ` ( x e. ( A [,] B ) |-> ( vol ` ( S " { x } ) )
) e. L^1 ` , because x is free in the second expression.
You could think ` x ` as local to this formula expression. It
could as well be ` ( y e. ( A [,] B ) |-> ( vol ` ( S " { y } )
) ) e. L^1 ` , or any other setvar (see ~ cbvmpt). So, I've tried
to find out where this requirement came from.
It turns out that on line 227, you apply ~ cncfmptc, like for the
square. The comment for this theorem says "a constant
function is continuous". However you apply it for ` ( V - U ) `
which is not a constant function anymore. You could also say that
x is not free in V and U (you can think of them as V(x) and U(x)).
You can however apply it on ` C ` or ` D `, because these are real
constants.
So, similar to the integral, we will have to show that ( V - U ) is integrable by splitting it out:
d77::eqid |- ( TopOpen ` CCfld ) = (
TopOpen ` CCfld )
238:d77:subcn |- - e. ( ( ( TopOpen ` CCfld ) tX
( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
d87:d77:addcn |- + e. ( ( ( TopOpen ` CCfld ) tX
( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
d78:238:a1i |- ( T. -> - e. ( ( ( TopOpen `
CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) )
d82:d87:a1i |- ( T. -> + e. ( ( ( TopOpen `
CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) )
239:10:mpteq2i |- ( x e. ( A [,] B ) |-> U ) =
( x e. ( A [,] B ) |-> ( C + ( ( ( x - A ) / ( B - A ) ) x. (
D - C ) ) ) )
240::cncfmptc |- ( ( C e. CC /\ ( A [,] B )
C_ CC /\ CC C_ CC ) -> ( x e. ( A [,] B ) |-> C ) e. ( ( A
[,] B ) -cn-> CC ) )
d96::cncfmptc |- ( ( D e. CC /\ ( A [,] B
) C_ CC /\ CC C_ CC ) -> ( x e. ( A [,] B ) |-> D ) e. ( (
A [,] B ) -cn-> CC ) )
d88:10cc,15b,228,240:mp3an |- ( x e. ( A [,] B )
|-> C ) e. ( ( A [,] B ) -cn-> CC )
d92:10dc,15b,228,d96:mp3an |- ( x e. ( A [,] B )
|-> D ) e. ( ( A [,] B ) -cn-> CC )
d83:d88:a1i |- ( T. -> ( x e. ( A
[,] B ) |-> C ) e. ( ( A [,] B ) -cn-> CC ) )
d91:d92:a1i |- ( T. -> ( x e. ( A
[,] B ) |-> D ) e. ( ( A [,] B ) -cn-> CC ) )
!d85:: |- ( T. -> ( x e. ( A
[,] B ) |-> ( ( x - A ) / ( B - A ) ) ) e. ( ( A [,] B )
-cn-> CC ) )
d86:d77,d78,d91,d83:cncfmpt2f |- ( T. -> ( x e. ( A
[,] B ) |-> ( D - C ) ) e. ( ( A [,] B ) -cn-> CC ) )
d84:d85,d86:mulcncf |- ( T. -> ( x e. ( A
[,] B ) |-> ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) ) e. (
( A [,] B ) -cn-> CC ) )
247:d77,d82,d83,d84:cncfmpt2f |- ( T. -> ( x e. ( A
[,] B ) |-> ( C + ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) )
) ) e. ( ( A [,] B ) -cn-> CC ) )
d79:239,247:syl5eqel |- ( T. -> ( x e. ( A
[,] B ) |-> U ) e. ( ( A [,] B ) -cn-> CC ) )
!d80:: |- ( T. -> ( x e. ( A
[,] B ) |-> V ) e. ( ( A [,] B ) -cn-> CC ) )
249:d77,d78,d80,d79:cncfmpt2f |- ( T. -> ( x
e. ( A [,] B ) |-> ( V - U ) ) e. ( ( A [,] B ) -cn-> CC )
)
This will remove the necessary hypothesis ` x e. ( A [,] B )
` from your line 227, and subsequently you will be able to
remove it all the way to your line 234a.
I hope this puts you on the right path!
BR,
_
Thierry
Hi Jon!
Concerning your proof of the integral X^N, your problem is with these statements (there are other similar ones) :
Here, ( x ^ N ) does not represents the function, but just the
expression at the point ' x '.
What you want instead is ` ( x e. ( A [,] B ) |-> ( x ^ N ) ) `
: this one represents the function.
I believe if you make that change, you should be unblocked.
For your 212e, I'll look at it, it shall be feasible since you
already have A =/= B as an assumption, so ( B - A ) cannot be
zero. It may involve a bit of Topology.
Just one quick comment: your 212b obviously could have been proven
using ~ cncfmptc, since ( B - A ) is a
constant. Maybe this could lead to a somewhat shorter proof (maybe
not).
_
Thierry
Hi Jon!
I've put what you need for your step 212e on pastebin.
(actually, no Topology involved!)
You're almost there!
_
Thierry
--
Hi Mario, this is quite interesting. I think maybe your post has been cutoff at the bottom maybe? It ends with line 105 and doesn't show the QED I think.
--
--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/4b8fd563-5a20-4e3f-97ca-9550253f8d89%40googlegroups.com.
--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/18bcf7ed-95fe-48a0-a280-e243485656a1%40googlegroups.com.
One very small question I think is appropriate for this thread as the area triangle stuff is moved.The theorems in my Mathbox have been moved to us.metamath.org which is nice. However there is no "structured version" for them at the moment (the button in the top right you can click to see more usual notation). Does this just take time or is there anything I can do to activate it? I'd like to show what I am doing to my old supervisor and they will get on much better with the structured versions I think.
--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/05af0812-c377-47e1-a756-b2684e43b217%40googlegroups.com.
( ( x e. ( A (,] B ) /\ x e. ( B [,) C ) )-> x e. ( B [,] B ) )
--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/e84d0c8c-4eb2-4c05-99fd-a4af1c0c3072%40googlegroups.com.
Actually, in this case, you can just skip your steps 78 and 79:
80:77:ss2abdv |- ( ( A e. RR* /\ B e. RR* /\ C e. RR* )
-> { x | ( x e. ( A (,] B ) /\ x e. ( B [,) C ) ) }
C_ { x | x e. ( B [,] B ) } )
Note that bnj1153 is discouraged!
I guess you have to revert to using elin directly.
--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/39fc1f70-e15f-4fd6-8c86-d69f14f424c5%40googlegroups.com.
With putting the theorem in deduction form with "( ph ->" how does making that change work? Would I need to replace almost all theorems in the text so they begin with "( ph ->" or is there some way of just changing the beginning and the end? Sounds like it could be quite a lot of work.
Re names I am willing to make the change, I think exp for exponential is a bit confusing in this context. Does anyone else have input? One of the reviewers suggested using the word monomial so maybe itmon is possible, itpow is fine or something else? Using exp does match with itgsinexp, though that is only in Glauco's math box. I looked for the theorem of the integral of e^x but couldn't find it :(
About "pow" vs. "exp":
The table in the "convention" lists some commonly used abbreviations.
Shall we try to make it as exhaustive as possible so that it becomes a reference, which can be used when one wants to find an existing theorem, or name a new one?
We could list there "pow" for power, "exp" for exponential, and
"itg" for integral. Same for "ico", "ioc", "icc", "ixx", etc.
which Jon has encountered recently.
On one hand I understand we might want to keep the table on that
page small and readable for those who want to get a high level
view and a generic understanding about how theorems are named, but
on the other hand I think an exhaustive reference would also have
its use. So shall there be two tables? What are your thoughts?
Re deduction form is there any way to create a general wrapper? I imagine you've considered this already.If ( A -> B ) does that imply ( ( ph -> A ) -> ( ph -> B ) )? If so could I just prove the deduction version from the current version by adding that at the start? I think that might be possible.