Hi David, Thanks for this!
First, the middle main bullet on slide 7 should use congruence instead of = , I think? 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' . 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; 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). Thanks again! -Marnix Op vr 17 jul. 2020 05:11 schreef David A. Wheeler <[email protected]>: > My thanks to everyone for their constructive criticism on my draft > prresentation on Schwabhauser 4.6! I've fixed everything I know > about, and added another slide to briefly explain the key theorems/axiom > the proof depends on. > > The new draft video is here: > https://youtu.be/sNXgTh-8OhQ > > Any last-minute comments before I post it "officially"? > > --- 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/E1jwGmg-0005Tc-Oi%40rmmprod06.runbox > . > -- 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/CAF7V2P-Mx5KqDD9nvSnRY8WMZsQw3stwEkhtk489BQGqC2O4-w%40mail.gmail.com.
