G.545 there equal plane

XI.35

If there be two equal plane angles, and on their vertices there be set up elevated segments containing equal angles with the original segments respectively, if on the elevated segments points be taken at random and perpendiculars be drawn from them to the planes in which the original angles are, and if from the points so arising in the planes segments be joined to the vertices of the original angles, they will contain, with the elevated segments, equal angles.

there_equal_plane()

prove < G A L ) = < M D N )

construct segment() → < B A C ), segment() → < E D F ), segment() → A, segment() → D, segment(A, G) → / A G /, segment(D, M) → / D M /, segment() → < M D E ), segment() → < G A B ), segment() → < M D F ), segment() → < G A C ), segment() → G, segment() → M, segment(A, G) → / A G /, segment(D, M) → / D M /, segment(G, L) → / G L /, segment(M, N) → / M N /, segment() → G, segment() → M, segment(B, A) → / B A /, segment(A, C) → / A C /, segment(E, D) → / E D /, segment(D, F) → / D F /, segment() → L, segment() → N, segment(L, A) → / L A /, segment(N, D) → / N D /

construct cut_equal_segment(/ D M /) → / A H / (equal)

construct parallel_line(H, / G L /) → / H K /

assert / G L / is perpendicular to the plane through / B A /, / A C /

∵ segments_parallel_rightassert / H K / is also perpendicular to the plane through / B A /, / A C /

construct From K, N let / K C /, / N F /, / K B /, / N E / be drawn perpendicular to / A C /, / D F /, / A B /, / D E /, and let / H C /, / C B /, / M F /, / F E / be joined.

∵ pythagorean_theoremassert the square on / H A / is equal to the squares on / H K /, / K A /, and the squares on / K C /, / C A / are equal to the square on / K A /

assert the square on / H A / is also equal to the squares on / H K /, / K C /, / C A /

∵ pythagorean_theoremassert The square on / H C / is equal to the squares on / H K /, / K C /

assert the square on / H A / is equal to the squares on / H C /, / C A /

∵ converse_pythagoreanassert < H C A ) is right

assert For the same reason < D F M ) is also right

assert < A C H ) = < D F M )

assert < H A C ) = < M D F )

∵ asa_aas_congruenceassert < M D F >, < H A C > are two triangles which have two angles equal to two angles, and one side equal to one side, namely, that subtending one of the equal angles, that is, / H A / = to / M D /; therefore they will also have the remaining sides equal to the remaining sides

assert / A C / = / D F /

assert Similarly we can prove that / A B / = / D E /

assert then / A C / = / D F /, and / A B / to / D E /, / C A /, / A B / = / F D /, / D E /

assert < C A B ) = < F D E )

∵ sas_congruenceassert / B C / = / E F /, the triangle to the triangle, and the remaining angles to the remaining angles; therefore < A C B ) = < D F E )

assert The right angle < A C K ) = the right angle < D F N )

assert < B C K ) = < E F N )

assert For the same reason < C B K ) = < F E N )

∵ asa_aas_congruenceassert < B C K >, < E F N > are two triangles which have two angles equal to two angles, and one side equal to one side, namely, that adjacent to the equal angles, that is, / B C / = to / E F /; therefore they will also have the remaining sides equal to the remaining sides

assert / C K / = / F N /

assert / A C / = / D F /

assert / A C /, / C K / = / D F /, / F N /; and they contain right angles

∵ sas_congruenceassert / A K / = / D N /

assert since / A H / = / D M /,

assert The square on / A H / = the square on / D M /

∵ pythagorean_theoremassert The squares on / A K /, / K H / are equal to the square on / A H /, for < A K H ) is right; and the squares on / D N /, / N M / are equal to the square on / D M /, for < D N M ) is right

assert the squares on / A K /, / K H / are equal to the squares on / D N /, / N M /; and of these the square on / A K / = the square on / D N /; therefore the remaining square on / K H / = the square on / N M /; therefore / H K / = / M N /

assert since / H A /, / A K / = / M D /, / D N /, and / H K / = / M N /,

∵ sss_congruenceassert < H A K ) = < M D N )

∴ etc

Dependency Graph

Required for

G.546