On Fri, 17 Jul 2020 16:20:24 +0200, Marnix Klooster <[email protected]> wrote: > Thanks for this! > > First, the middle main bullet on slide 7 should use congruence instead of > = , I think?
Yes! Thanks for telling me. Fixed. > Second, I had a bit of a hard time following what was being used exactly. > > Specifically, I had to find a copy of the book to find out that "IFS" > stands for "inner five segments [configuration]", i.e., a triangle acd > with b on ac , together with a congruent a'c'd' with b' . Okay, I've added text that explains what IFS means earlier. > But working through the proof, it seems that all that is _really_ being > used, is that abc ~ a'b'c' implies ab ~ a'b' and bc ~ b'c' (which > directly follows from the definition of congruence). > So (1) using IFS here seems kind of heavy and indirect machinery; ... Well, we also need to prove bd ~ b'd'. But that's not really the point (ha?). The point was to try to follow the original proof "relatively closely", to show how to use an informal proof to help create a formal proof. We need to use something like IFS since that's what the book used. > but given > that the goal is to follow the book closely, (2) a definition would help > (with picture? e.g. Abb. 11 from page 34, but without the dotted lines). You read my mind! You must have seen the first draft video. The second draft video adds a new slide 8 that includes a figure that basically does that. (It's the "obvious" way to illustrate IFS.) I'll add some tic marks so the new figure is easier to follow. My goal was, in part, to show how to "translate" an informal proof into Metamath. There are no doubts many ways to prove something :-). --- David A. Wheeler -- 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/E1jwTKZ-0003Yo-2c%40rmmprod06.runbox.
