Theorem motcgr3

Description: Property of a motion: distances are preserved, special case of triangles. (Contributed by Thierry Arnoux, 15-Dec-2019)

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

Proof

Step	Hyp	Ref	Expression
1		motcgr3.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		motcgr3.m	⊢ − = ( dist ‘ 𝐺 )
3		motcgr3.r	⊢ ∼ = ( cgrG ‘ 𝐺 )
4		motcgr3.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5		motcgr3.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
6		motcgr3.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
7		motcgr3.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
8		motcgr3.d	⊢ ( 𝜑 → 𝐷 = ( 𝐻 ‘ 𝐴 ) )
9		motcgr3.e	⊢ ( 𝜑 → 𝐸 = ( 𝐻 ‘ 𝐵 ) )
10		motcgr3.f	⊢ ( 𝜑 → 𝐹 = ( 𝐻 ‘ 𝐶 ) )
11		motcgr3.h	⊢ ( 𝜑 → 𝐻 ∈ ( 𝐺 Ismt 𝐺 ) )
12	1 2 4 11 5	motcl	⊢ ( 𝜑 → ( 𝐻 ‘ 𝐴 ) ∈ 𝑃 )
13	8 12	eqeltrd	⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
14	1 2 4 11 6	motcl	⊢ ( 𝜑 → ( 𝐻 ‘ 𝐵 ) ∈ 𝑃 )
15	9 14	eqeltrd	⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
16	1 2 4 11 7	motcl	⊢ ( 𝜑 → ( 𝐻 ‘ 𝐶 ) ∈ 𝑃 )
17	10 16	eqeltrd	⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
18	8 9	oveq12d	⊢ ( 𝜑 → ( 𝐷 − 𝐸 ) = ( ( 𝐻 ‘ 𝐴 ) − ( 𝐻 ‘ 𝐵 ) ) )
19	1 2 4 5 6 11	motcgr	⊢ ( 𝜑 → ( ( 𝐻 ‘ 𝐴 ) − ( 𝐻 ‘ 𝐵 ) ) = ( 𝐴 − 𝐵 ) )
20	18 19	eqtr2d	⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = ( 𝐷 − 𝐸 ) )
21	9 10	oveq12d	⊢ ( 𝜑 → ( 𝐸 − 𝐹 ) = ( ( 𝐻 ‘ 𝐵 ) − ( 𝐻 ‘ 𝐶 ) ) )
22	1 2 4 6 7 11	motcgr	⊢ ( 𝜑 → ( ( 𝐻 ‘ 𝐵 ) − ( 𝐻 ‘ 𝐶 ) ) = ( 𝐵 − 𝐶 ) )
23	21 22	eqtr2d	⊢ ( 𝜑 → ( 𝐵 − 𝐶 ) = ( 𝐸 − 𝐹 ) )
24	10 8	oveq12d	⊢ ( 𝜑 → ( 𝐹 − 𝐷 ) = ( ( 𝐻 ‘ 𝐶 ) − ( 𝐻 ‘ 𝐴 ) ) )
25	1 2 4 7 5 11	motcgr	⊢ ( 𝜑 → ( ( 𝐻 ‘ 𝐶 ) − ( 𝐻 ‘ 𝐴 ) ) = ( 𝐶 − 𝐴 ) )
26	24 25	eqtr2d	⊢ ( 𝜑 → ( 𝐶 − 𝐴 ) = ( 𝐹 − 𝐷 ) )
27	1 2 3 4 5 6 7 13 15 17 20 23 26	trgcgr	⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝐸 𝐹 ”⟩ )