Theorem motcgr

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

	Ref	Expression
Hypotheses	ismot.p	|- P = ( Base ` G )
	ismot.m	|- .- = ( dist ` G )
	motgrp.1	|- ( ph -> G e. V )
	motcgr.a	|- ( ph -> A e. P )
	motcgr.b	|- ( ph -> B e. P )
	motcgr.f	|- ( ph -> F e. ( G Ismt G ) )
Assertion	motcgr	|- ( ph -> ( ( F ` A ) .- ( F ` B ) ) = ( A .- B ) )

Proof

Step	Hyp	Ref	Expression
1		ismot.p	|- P = ( Base ` G )
2		ismot.m	|- .- = ( dist ` G )
3		motgrp.1	|- ( ph -> G e. V )
4		motcgr.a	|- ( ph -> A e. P )
5		motcgr.b	|- ( ph -> B e. P )
6		motcgr.f	|- ( ph -> F e. ( G Ismt G ) )
7	1 2	ismot	|- ( G e. V -> ( F e. ( G Ismt G ) <-> ( F : P -1-1-onto-> P /\ A. a e. P A. b e. P ( ( F ` a ) .- ( F ` b ) ) = ( a .- b ) ) ) )
8	3 7	syl	|- ( ph -> ( F e. ( G Ismt G ) <-> ( F : P -1-1-onto-> P /\ A. a e. P A. b e. P ( ( F ` a ) .- ( F ` b ) ) = ( a .- b ) ) ) )
9	6 8	mpbid	|- ( ph -> ( F : P -1-1-onto-> P /\ A. a e. P A. b e. P ( ( F ` a ) .- ( F ` b ) ) = ( a .- b ) ) )
10	9	simprd	|- ( ph -> A. a e. P A. b e. P ( ( F ` a ) .- ( F ` b ) ) = ( a .- b ) )
11		fveq2	|- ( a = A -> ( F ` a ) = ( F ` A ) )
12	11	oveq1d	|- ( a = A -> ( ( F ` a ) .- ( F ` b ) ) = ( ( F ` A ) .- ( F ` b ) ) )
13		oveq1	|- ( a = A -> ( a .- b ) = ( A .- b ) )
14	12 13	eqeq12d	|- ( a = A -> ( ( ( F ` a ) .- ( F ` b ) ) = ( a .- b ) <-> ( ( F ` A ) .- ( F ` b ) ) = ( A .- b ) ) )
15		fveq2	|- ( b = B -> ( F ` b ) = ( F ` B ) )
16	15	oveq2d	|- ( b = B -> ( ( F ` A ) .- ( F ` b ) ) = ( ( F ` A ) .- ( F ` B ) ) )
17		oveq2	|- ( b = B -> ( A .- b ) = ( A .- B ) )
18	16 17	eqeq12d	|- ( b = B -> ( ( ( F ` A ) .- ( F ` b ) ) = ( A .- b ) <-> ( ( F ` A ) .- ( F ` B ) ) = ( A .- B ) ) )
19	14 18	rspc2va	|- ( ( ( A e. P /\ B e. P ) /\ A. a e. P A. b e. P ( ( F ` a ) .- ( F ` b ) ) = ( a .- b ) ) -> ( ( F ` A ) .- ( F ` B ) ) = ( A .- B ) )
20	4 5 10 19	syl21anc	|- ( ph -> ( ( F ` A ) .- ( F ` B ) ) = ( A .- B ) )