Geometry proofs on congruency - propose adding "rotation" and completing CPCTC

[david-a-wheeler]

While looking at the geometry proofs involving congruence, I found some omissions involving CPCTC.

The problem is that the proof cgrcgra ("Triangle congruence implies angle congruence.") only handles one of the 3 angle cases of the theorem that "corresponding parts of congruent triangles are congruent" (CPCTC). Proof cgrcgra shows that if ABC is congruent-as-a-triangle with DEF, then ABC is conguent-as-angle with DEF. That is, given ⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹”⟩) you can prove ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩). However, we don't have proofs of the 2 other angle versions of CPCTC, that is, if ABC is conguent-as-a-triangle with DEF, then (1) BCA is conguent-as-an-angle with EFD, and also that (2) CAB is congruent-as-an-angle with FDE.

We do have all 3 segment versions of CPCTC, namely cgr3simp1, cgr3simp2, and cgr3simp3; we're just missing two of the CPCTC angle forms.

I propose adding a few more theorems to make proving congruency of triangles and angles of congruent triangles very direct. The obvious way is to first prove that "rotations" of congruent triansl are congruent, which seem so useful that they should exist on their own anway. So I recommend that we add these 4 theorems:

• if ABC is conguent-as-a-triangle with DEF, then (1) BCA is conguent-as-an-triangle with EFD (rotated). Then it's easily proven (as a separate theorm) that BCA is conguent-as-an-angle with EFD.
• if ABC is conguent-as-a-triangle with DEF, then CAB is congruent-as-an-triangle with FDE. Then it's easily proven (as a separate theorem) than CAB is congruent-as-an-angle with FDE.

Lots of geometry problems involve proving congruence of triangles and then use congruence of specific angles following from that, so making this extremely easy & direct seems appropriate. Some of these proofs will be really small, but I think CPCTC is so widely-referenced that it makes sense to have it directly and fully implemented.

[tirix]

You should be able to obtain your new theorems by applying cgraswaplr to the final statements of cgr3simp1, cgr3simp2, and cgr3simp3 respectively.

It might indeed be interesting to introduce those as new theorems. Feel free to do so!

[tirix]

The comments recently added by @david-a-wheeler in ~ df-cgrg through #3028 mention:

For example, see ~ cgr3simp1 , ~ cgr3simp2 , ~ cgr3simp3 , ~ cgrcgra , and permutation laws such as ~ cgr3swap12 and ~ dfcgrg2 .

Is that enough to cover this issue?

I would generally be reluctant to add two-step proofs, but there might be a case if:

• they are well-known theorems, that might e.g. be referenced outside the database itself,
• they are used very often and "pay their own costs" in terms of byte-size of set.mm

Here, we might be in the first case.

[benjub]

I didn't check so sorry if this is not to the point, but we should have that triangle congruence (our definition) is implied by either:

• two sides, one angle: only if it is the angle formed by the two sides (note in comment that other configurations do not imply congruence);
• one side, two angles: any configuration;

(three sides: this is just our definition of congruence). And note somewhere that three equal angles does not imply congruence (in cartesian geometry: only "similarity").

Also, in #3028, I insisted on one fundamental theorem and its corollary. Can you emphasize it somehow in comments?

[david-a-wheeler]

@tirix - I've been thinking the same thing myself, basically, we should add the other two angle proofs that represent CPCTC. CPCTC is probably one of the most common proof statements in at least the US. High school students have to take geometry, and geometry proofs are often of the form "prove 2 triangles are congruent, then use CPCTC".

Currently we have direct proofs of all 3 segment versions (~ cgr3simp1 , ~ cgr3simp2 , ~ cgr3simp3). We have one of the angle versions ~ cgrcgra. What's missing are the other two angles, which you can get but it requires multiple steps. These are really common and known by many, so I think we should add the other two CPCTC angle versions ("given 2 congruent triangles, these angles are congruent").

@benjub - SAS is already proven in tgsas1 and tgsas. ASA is proven in tgasa1 and tgasa. We don't actually have a proof of AAS (Angle-Angle-Side), Theorem 11.50 of [Schwabhauser] p. 108, we just have a placeholder. Contributions welcome :-).

[tirix]

I've added some blueprint pages to show the remaining steps to prove AAS and ASS. You can find them here: https://tirix.github.io/metamath-blueprints/Triangle%20Congruences/

And more generally, you can check more about what blueprints could be useful for here: https://tirix.github.io/metamath-blueprints/