InterceptTheorem.mmt

namespace http://mathhub.info/FrameIT/frameworld ❚

fixmeta ?FrameworldMeta ❚


/T
           S
          /|
         / |
        /  |
       /___|
      A    C
     /     |
    /______|
   B       D

The scroll encodes the InterceptTheorem
❚
theory InterceptTheorem =
    meta ?MetaAnnotations?problemTheory  ?InterceptTheorem/Problem ❙
    meta ?MetaAnnotations?solutionTheory ?InterceptTheorem/Solution ❙

    theory Problem =
        S: point ❘ meta ?MetaAnnotations?label "S" ❙
        A: point ❘ meta ?MetaAnnotations?label "A" ❙
        B: point ❘ meta ?MetaAnnotations?label "B" ❙
        C: point ❘ meta ?MetaAnnotations?label "C" ❙
        D: point ❘ meta ?MetaAnnotations?label "D" ❙

        H: line ❘ meta ?MetaAnnotations?label "H"❙
        G: line ❘ meta ?MetaAnnotations?label "G"❙

        L: line ❘ meta ?MetaAnnotations?label "L"❙
        M: line ❘ meta ?MetaAnnotations?label "M"❙


        // annoying on proofs which are unfortunately necessary. A possible solution is to make it into two scrolls. One scroll just to build the geometric construction. One scroll to calculate the distances❙
        A_on_H : ⊦ A on H ❘ meta ?MetaAnnotations?label s" ${lverb A}∈${lverb H}"❙
        C_on_H : ⊦ C on H ❘ meta ?MetaAnnotations?label s" ${lverb C}∈${lverb H}"❙
        B_on_G : ⊦ B on G ❘ meta ?MetaAnnotations?label s" ${lverb B}∈${lverb G}"❙
        D_on_G : ⊦ D on G ❘ meta ?MetaAnnotations?label s" ${lverb D}∈${lverb G}"❙


       // TODO more proofs that the S is also on  AB and CD ...    ❙
        S_on_L : ⊦ S on L ❘ meta ?MetaAnnotations?label s" ${lverb S}∈${lverb L}"❙
        A_on_L : ⊦ A on L ❘ meta ?MetaAnnotations?label s" ${lverb A}∈${lverb L}"❙
        B_on_L : ⊦ B on L ❘ meta ?MetaAnnotations?label s" ${lverb B}∈${lverb L}"❙

        S_on_M : ⊦ S on M ❘ meta ?MetaAnnotations?label s" ${lverb S}∈${lverb M}"❙
        C_on_M : ⊦ C on M ❘ meta ?MetaAnnotations?label s" ${lverb C}∈${lverb M}"❙
        D_on_M : ⊦ D on M ❘ meta ?MetaAnnotations?label s" ${lverb D}∈${lverb M}"❙


        distanceSA : Σ x:ℝ . ⊦ ( d- S A ) ≐ x ❘
                    meta ?MetaAnnotations?label s"${lverb S A}" ❘
                    meta ?MetaAnnotations?description s"Length of leg ${lverb S A}"
        ❙
        distanceAC : Σ x:ℝ . ⊦ ( d- A C ) ≐ x ❘
                    meta ?MetaAnnotations?label s"${lverb A C}" ❘
                    meta ?MetaAnnotations?description s"Length of leg ${lverb A C}"
        ❙
        distanceSB : Σ x:ℝ . ⊦ ( d- S B ) ≐ x ❘
                     meta ?MetaAnnotations?label s"${lverb S B}" ❘
                     meta ?MetaAnnotations?description s"Length of leg ${lverb S B}"
        ❙

        // TODO S € AB und S € CD. Dafuer muesste man dann auch noch die beiden anderen Geraden angeben. Mehr Variablen yay ❙


       AC_||_BD :  ⊦ paraL H G ❘
                    meta ?MetaAnnotations?label s"${lverb H}||${lverb G}" ❘
                    meta ?MetaAnnotations?description s"ParallelFact {lverb H} and {lverb G}"
        ❙
    ❚

    theory Solution =
       include ?InterceptTheorem/Problem ❙


        // Problem, there is no divison defined in math.mmt, so I can't divide the line to get the correct answer   ❙



        //  ⟨((πl distanceAC) ⋅ (πl distanceSB)) / (πl distanceSA) , sketch "InterceptTheorem Scroll"⟩ Divison funktioniert aber leider noch nicht :) ❙
        deduceLineBD
            : Σ x:ℝ . ⊦ ( d- B D) ≐ x  ❘
                    =  ⟨ doTheDif ((πl distanceAC) ⋅ (πl distanceSB))  (πl distanceSA) , sketch "InterceptTheorem Scroll"⟩ ❘
            meta ?MetaAnnotations?label s"PlaceHolder${lverb S A B C D}" ❘
            meta ?MetaAnnotations?description s"xThe deduced distance of BD by using BD*SA = AC*SB "
        ❙

        // the description verbalizes InterceptTheorem, hence must come after its declaration ❙
                meta ?MetaAnnotations?label s"InterceptTheorem" ❙
                meta ?MetaAnnotations?description s" The Interceptheorem is calculating the length of ${lverb G}" ❙
    ❚
❚