PlaneLineAngleScroll.mmt

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

fixmeta ?FrameworldMeta ❚




/T
This scrolls calculates the angle between a circle and a line.

The arguments required:

C - the circle
L - the line

A - the intersection point between C and L
base - the base as a circle
top - the top as a circle

H - the height as a line

A_on_L - a proof that A is on L
A_on_C - a proof that A is on C



This Scrolls returns:

deduceAngle - the Angle between C and L


❚



theory CircleLineAngleScroll =
    meta ?MetaAnnotations?problemTheory ?CircleLineAngleScroll/Problem ❙
    meta ?MetaAnnotations?solutionTheory ?CircleLineAngleScroll/Solution ❙

    theory Problem =

          // Define the plane (circle) , line and the intersection point ❙
          C : circle ❘ meta ?MetaAnnotations?label "○C" ❙
          L : line ❘ meta ?MetaAnnotations?label "L" ❙

          A : point ❘ meta ?MetaAnnotations?label "A" ❙

          // Intersectionpoint is on the plane and the line ❙
          A_on_L : ⊦ A on L ❘ meta ?MetaAnnotations?label s" ${lverb A}∈${lverb L}"❙
          A_on_C : ⊦ A VonC C ❘ meta ?MetaAnnotations?label s" ${lverb A}∈${lverb C}"❙
    ❚

    theory Solution =
       include ?CircleLineAngleScroll/Problem ❙
        // if this gets evaluated to 90 degrees, the client will make another OrthogonalFact ❙

        deduceAngle
                     : Σ x : ℝ . ⊦ angleCircleLine C L ≐ x ❘
                     =  ⟨ radToDegree ( plcalc (  Pnormal ( planeCircle C ) )   ( directionL L )  )  , sketch "PlaneAngleScroll Scroll" ⟩ ❘
                    meta ?MetaAnnotations?label s"∠${lverb C L}" ❘
                    meta ?MetaAnnotations?description s"Caclculates the volume of a cone given the base and the height."
                ❙

                meta ?MetaAnnotations?label "CircleLineAngleScroll" ❙
                meta ?MetaAnnotations?description s" Caclculates the angle between the plane of ${lverb C} and the line ${lverb L} " ❙
    ❚
❚

/T
This scrolls convert the 90 degree angle between a circle and a line into an angle between three points.

The arguments required:

C - the circle
L - the line

orthogonalCircleLine - a proof that the angle between C and L is 90 degrees
planeLineAngle - the actual angle between C and L

A - the first point that defines the angle and also lies on H
B - the second point that defines the angle and also the intersection point between C and L
P - the first point that defines the angle  and also lies on C


A_on_L - a proof that A is on L

B_on_L - a proof that B is on L
B_on_C - a proof that B is on C

P_on_C - a proof that P is on C


This Scrolls returns:

deduceAngle - the Angle between A,B,P


❚

theory CircleLineAngleToAngleScroll =
    meta ?MetaAnnotations?problemTheory ?CircleLineAngleToAngleScroll/Problem ❙
    meta ?MetaAnnotations?solutionTheory ?CircleLineAngleToAngleScroll/Solution ❙

    theory Problem =

          // Define the plane (circle) , line and the intersection point   ❙
          C : circle ❘ meta ?MetaAnnotations?label "○C" ❙
          L : line ❘ meta ?MetaAnnotations?label "L" ❙

        orthogonalCircleLine : ⊦  orthogCL C L ❘ meta ?MetaAnnotations?label s" ${lverb C}⊥${lverb L}"  ❙


         planeLineAngle : Σ x : ℝ . ⊦ angleCircleLine C L ≐ x ❘ meta ?MetaAnnotations?label s"∠${lverb C L}" ❙

          A : point ❘ meta ?MetaAnnotations?label "A" ❙
          B : point ❘ meta ?MetaAnnotations?label "B" ❙
          P : point ❘ meta ?MetaAnnotations?label "P" ❙

          // Intersectionpoint is on the plane and the line. ❙
          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}"❙
          B_on_C : ⊦ B VonC C ❘ meta ?MetaAnnotations?label s" ${lverb B}∈${lverb C}"❙

          P_on_C : ⊦ P VonC C ❘ meta ?MetaAnnotations?label s" ${lverb P}∈${lverb C}"❙




    ❚

    theory Solution =
       include ?CircleLineAngleToAngleScroll/Problem ❙


                deduceAngle : Σ x : ℝ . ⊦ ( ∠ P,B,A ) ≐ x ❘
                     =  ⟨ πl planeLineAngle   , sketch "CastAngle" ⟩ ❘
                    meta ?MetaAnnotations?label s"∠${lverb P B A}" ❘
                    meta ?MetaAnnotations?description s"Caclculates the angle ∠${lverb P B A}"
                ❙

                meta ?MetaAnnotations?label "CircleLineAngleToAngle" ❙
                meta ?MetaAnnotations?description s"CircleLineAngle don't work as normal angles, therefore this scrolls converts a CircleLineAngle ∠${lverb C L} to a normal angle ∠${lverb P B A}, if it is 90°." ❙
    ❚
❚