Metamath Proof Explorer


Theorem dfcgrg2

Description: Congruence for two triangles can also be defined as congruence of sides and angles (6 parts). This is often the actual textbook definition of triangle congruence, see for example https://en.wikipedia.org/wiki/Congruence_(geometry)#Congruence_of_triangles . With this definition, the "SSS" congruence theorem has an additional part, namely, that triangle congruence implies congruence of the sides (which means equality of the lengths). Because our development of elementary geometry strives to closely follow Schwabhaeuser's, our original definition of shape congruence, df-cgrg , already covers that part: see trgcgr . This theorem is also named "CPCTC", which stands for "Corresponding Parts of Congruent Triangles are Congruent", see https://en.wikipedia.org/wiki/Congruence_(geometry)#CPCTC . (Contributed by Thierry Arnoux, 18-Jan-2023)

Ref Expression
Hypotheses dfcgrg2.p 𝑃 = ( Base ‘ 𝐺 )
dfcgrg2.m = ( dist ‘ 𝐺 )
dfcgrg2.g ( 𝜑𝐺 ∈ TarskiG )
dfcgrg2.a ( 𝜑𝐴𝑃 )
dfcgrg2.b ( 𝜑𝐵𝑃 )
dfcgrg2.c ( 𝜑𝐶𝑃 )
dfcgrg2.d ( 𝜑𝐷𝑃 )
dfcgrg2.e ( 𝜑𝐸𝑃 )
dfcgrg2.f ( 𝜑𝐹𝑃 )
dfcgrg2.1 ( 𝜑𝐴𝐵 )
dfcgrg2.2 ( 𝜑𝐵𝐶 )
dfcgrg2.3 ( 𝜑𝐶𝐴 )
Assertion dfcgrg2 ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ↔ ( ( ( 𝐴 𝐵 ) = ( 𝐷 𝐸 ) ∧ ( 𝐵 𝐶 ) = ( 𝐸 𝐹 ) ∧ ( 𝐶 𝐴 ) = ( 𝐹 𝐷 ) ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐶 𝐴 𝐵 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐹 𝐷 𝐸 ”⟩ ∧ ⟨“ 𝐵 𝐶 𝐴 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐸 𝐹 𝐷 ”⟩ ) ) ) )

Proof

Step Hyp Ref Expression
1 dfcgrg2.p 𝑃 = ( Base ‘ 𝐺 )
2 dfcgrg2.m = ( dist ‘ 𝐺 )
3 dfcgrg2.g ( 𝜑𝐺 ∈ TarskiG )
4 dfcgrg2.a ( 𝜑𝐴𝑃 )
5 dfcgrg2.b ( 𝜑𝐵𝑃 )
6 dfcgrg2.c ( 𝜑𝐶𝑃 )
7 dfcgrg2.d ( 𝜑𝐷𝑃 )
8 dfcgrg2.e ( 𝜑𝐸𝑃 )
9 dfcgrg2.f ( 𝜑𝐹𝑃 )
10 dfcgrg2.1 ( 𝜑𝐴𝐵 )
11 dfcgrg2.2 ( 𝜑𝐵𝐶 )
12 dfcgrg2.3 ( 𝜑𝐶𝐴 )
13 eqid ( Itv ‘ 𝐺 ) = ( Itv ‘ 𝐺 )
14 3 adantr ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → 𝐺 ∈ TarskiG )
15 4 adantr ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → 𝐴𝑃 )
16 5 adantr ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → 𝐵𝑃 )
17 6 adantr ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → 𝐶𝑃 )
18 7 adantr ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → 𝐷𝑃 )
19 8 adantr ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → 𝐸𝑃 )
20 9 adantr ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → 𝐹𝑃 )
21 eqid ( cgrG ‘ 𝐺 ) = ( cgrG ‘ 𝐺 )
22 1 2 21 3 4 5 6 7 8 9 trgcgrg ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ↔ ( ( 𝐴 𝐵 ) = ( 𝐷 𝐸 ) ∧ ( 𝐵 𝐶 ) = ( 𝐸 𝐹 ) ∧ ( 𝐶 𝐴 ) = ( 𝐹 𝐷 ) ) ) )
23 22 biimpa ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → ( ( 𝐴 𝐵 ) = ( 𝐷 𝐸 ) ∧ ( 𝐵 𝐶 ) = ( 𝐸 𝐹 ) ∧ ( 𝐶 𝐴 ) = ( 𝐹 𝐷 ) ) )
24 23 simp1d ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → ( 𝐴 𝐵 ) = ( 𝐷 𝐸 ) )
25 23 simp2d ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → ( 𝐵 𝐶 ) = ( 𝐸 𝐹 ) )
26 23 simp3d ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → ( 𝐶 𝐴 ) = ( 𝐹 𝐷 ) )
27 10 adantr ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → 𝐴𝐵 )
28 11 adantr ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → 𝐵𝐶 )
29 12 adantr ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → 𝐶𝐴 )
30 1 2 13 14 15 16 17 18 19 20 24 25 26 27 28 29 tgsss1 ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
31 1 2 13 14 17 15 16 20 18 19 26 24 25 29 27 28 tgsss1 ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → ⟨“ 𝐶 𝐴 𝐵 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐹 𝐷 𝐸 ”⟩ )
32 1 2 13 14 16 17 15 19 20 18 25 26 24 28 29 27 tgsss1 ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → ⟨“ 𝐵 𝐶 𝐴 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐸 𝐹 𝐷 ”⟩ )
33 30 31 32 3jca ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐶 𝐴 𝐵 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐹 𝐷 𝐸 ”⟩ ∧ ⟨“ 𝐵 𝐶 𝐴 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐸 𝐹 𝐷 ”⟩ ) )
34 33 ex ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐶 𝐴 𝐵 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐹 𝐷 𝐸 ”⟩ ∧ ⟨“ 𝐵 𝐶 𝐴 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐸 𝐹 𝐷 ”⟩ ) ) )
35 34 pm4.71d ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ↔ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐶 𝐴 𝐵 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐹 𝐷 𝐸 ”⟩ ∧ ⟨“ 𝐵 𝐶 𝐴 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐸 𝐹 𝐷 ”⟩ ) ) ) )
36 22 anbi1d ( 𝜑 → ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐶 𝐴 𝐵 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐹 𝐷 𝐸 ”⟩ ∧ ⟨“ 𝐵 𝐶 𝐴 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐸 𝐹 𝐷 ”⟩ ) ) ↔ ( ( ( 𝐴 𝐵 ) = ( 𝐷 𝐸 ) ∧ ( 𝐵 𝐶 ) = ( 𝐸 𝐹 ) ∧ ( 𝐶 𝐴 ) = ( 𝐹 𝐷 ) ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐶 𝐴 𝐵 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐹 𝐷 𝐸 ”⟩ ∧ ⟨“ 𝐵 𝐶 𝐴 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐸 𝐹 𝐷 ”⟩ ) ) ) )
37 35 36 bitrd ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ↔ ( ( ( 𝐴 𝐵 ) = ( 𝐷 𝐸 ) ∧ ( 𝐵 𝐶 ) = ( 𝐸 𝐹 ) ∧ ( 𝐶 𝐴 ) = ( 𝐹 𝐷 ) ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐶 𝐴 𝐵 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐹 𝐷 𝐸 ”⟩ ∧ ⟨“ 𝐵 𝐶 𝐴 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐸 𝐹 𝐷 ”⟩ ) ) ) )