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	|- P = ( Base ` G )
	motcgr3.m	|- .- = ( dist ` G )
	motcgr3.r	|- .~ = ( cgrG ` G )
	motcgr3.g	|- ( ph -> G e. TarskiG )
	motcgr3.a	|- ( ph -> A e. P )
	motcgr3.b	|- ( ph -> B e. P )
	motcgr3.c	|- ( ph -> C e. P )
	motcgr3.d	|- ( ph -> D = ( H ` A ) )
	motcgr3.e	|- ( ph -> E = ( H ` B ) )
	motcgr3.f	|- ( ph -> F = ( H ` C ) )
	motcgr3.h	|- ( ph -> H e. ( G Ismt G ) )
Assertion	motcgr3	|- ( ph -> <" A B C "> .~ <" D E F "> )

Proof

Step	Hyp	Ref	Expression
1		motcgr3.p	|- P = ( Base ` G )
2		motcgr3.m	|- .- = ( dist ` G )
3		motcgr3.r	|- .~ = ( cgrG ` G )
4		motcgr3.g	|- ( ph -> G e. TarskiG )
5		motcgr3.a	|- ( ph -> A e. P )
6		motcgr3.b	|- ( ph -> B e. P )
7		motcgr3.c	|- ( ph -> C e. P )
8		motcgr3.d	|- ( ph -> D = ( H ` A ) )
9		motcgr3.e	|- ( ph -> E = ( H ` B ) )
10		motcgr3.f	|- ( ph -> F = ( H ` C ) )
11		motcgr3.h	|- ( ph -> H e. ( G Ismt G ) )
12	1 2 4 11 5	motcl	|- ( ph -> ( H ` A ) e. P )
13	8 12	eqeltrd	|- ( ph -> D e. P )
14	1 2 4 11 6	motcl	|- ( ph -> ( H ` B ) e. P )
15	9 14	eqeltrd	|- ( ph -> E e. P )
16	1 2 4 11 7	motcl	|- ( ph -> ( H ` C ) e. P )
17	10 16	eqeltrd	|- ( ph -> F e. P )
18	8 9	oveq12d	|- ( ph -> ( D .- E ) = ( ( H ` A ) .- ( H ` B ) ) )
19	1 2 4 5 6 11	motcgr	|- ( ph -> ( ( H ` A ) .- ( H ` B ) ) = ( A .- B ) )
20	18 19	eqtr2d	|- ( ph -> ( A .- B ) = ( D .- E ) )
21	9 10	oveq12d	|- ( ph -> ( E .- F ) = ( ( H ` B ) .- ( H ` C ) ) )
22	1 2 4 6 7 11	motcgr	|- ( ph -> ( ( H ` B ) .- ( H ` C ) ) = ( B .- C ) )
23	21 22	eqtr2d	|- ( ph -> ( B .- C ) = ( E .- F ) )
24	10 8	oveq12d	|- ( ph -> ( F .- D ) = ( ( H ` C ) .- ( H ` A ) ) )
25	1 2 4 7 5 11	motcgr	|- ( ph -> ( ( H ` C ) .- ( H ` A ) ) = ( C .- A ) )
26	24 25	eqtr2d	|- ( ph -> ( C .- A ) = ( F .- D ) )
27	1 2 3 4 5 6 7 13 15 17 20 23 26	trgcgr	|- ( ph -> <" A B C "> .~ <" D E F "> )