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 ‘ 𝐺 ) ⟨“ 𝐸 𝐹 𝐷 ”⟩ ) ) ) )