Theorem trgcgr

Description: Triangle congruence. (Contributed by Thierry Arnoux, 27-Apr-2019)

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

Proof

Step	Hyp	Ref	Expression
1		trgcgrg.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		trgcgrg.m	⊢ − = ( dist ‘ 𝐺 )
3		trgcgrg.r	⊢ ∼ = ( cgrG ‘ 𝐺 )
4		trgcgrg.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5		trgcgrg.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
6		trgcgrg.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
7		trgcgrg.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
8		trgcgrg.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
9		trgcgrg.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
10		trgcgrg.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
11		trgcgr.1	⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = ( 𝐷 − 𝐸 ) )
12		trgcgr.2	⊢ ( 𝜑 → ( 𝐵 − 𝐶 ) = ( 𝐸 − 𝐹 ) )
13		trgcgr.3	⊢ ( 𝜑 → ( 𝐶 − 𝐴 ) = ( 𝐹 − 𝐷 ) )
14	1 2 3 4 5 6 7 8 9 10	trgcgrg	⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝐸 𝐹 ”⟩ ↔ ( ( 𝐴 − 𝐵 ) = ( 𝐷 − 𝐸 ) ∧ ( 𝐵 − 𝐶 ) = ( 𝐸 − 𝐹 ) ∧ ( 𝐶 − 𝐴 ) = ( 𝐹 − 𝐷 ) ) ) )
15	11 12 13 14	mpbir3and	⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝐸 𝐹 ”⟩ )