Theorem motcgr

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

	Ref	Expression
Hypotheses	ismot.p	$$⊢P={\mathrm{Base}}_G$$
	ismot.m	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
	motgrp.1	$$⊢\phi \to G\in V$$
	motcgr.a	$$⊢\phi \to A\in P$$
	motcgr.b	$$⊢\phi \to B\in P$$
	motcgr.f	$$⊢\phi \to F\in \left(GIsmtG\right)$$
Assertion	motcgr	$$⊢\phi \to F\left(A\right)\underset{\dot{}}{-}F\left(B\right)=A\underset{\dot{}}{-}B$$

Proof

Step	Hyp	Ref	Expression
1		ismot.p	$$⊢P={\mathrm{Base}}_G$$
2		ismot.m	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
3		motgrp.1	$$⊢\phi \to G\in V$$
4		motcgr.a	$$⊢\phi \to A\in P$$
5		motcgr.b	$$⊢\phi \to B\in P$$
6		motcgr.f	$$⊢\phi \to F\in \left(GIsmtG\right)$$
7	1 2	ismot	$$⊢G\in V\to \left(F\in \left(GIsmtG\right)\leftrightarrow \left(F:P\underset{1-1\; onto}{⟶}P\wedge \forall a\in P\forall b\in PF\left(a\right)\underset{\dot{}}{-}F\left(b\right)=a\underset{\dot{}}{-}b\right)\right)$$
8	3 7	syl	$$⊢\phi \to \left(F\in \left(GIsmtG\right)\leftrightarrow \left(F:P\underset{1-1\; onto}{⟶}P\wedge \forall a\in P\forall b\in PF\left(a\right)\underset{\dot{}}{-}F\left(b\right)=a\underset{\dot{}}{-}b\right)\right)$$
9	6 8	mpbid	$$⊢\phi \to \left(F:P\underset{1-1\; onto}{⟶}P\wedge \forall a\in P\forall b\in PF\left(a\right)\underset{\dot{}}{-}F\left(b\right)=a\underset{\dot{}}{-}b\right)$$
10	9	simprd	$$⊢\phi \to \forall a\in P\forall b\in PF\left(a\right)\underset{\dot{}}{-}F\left(b\right)=a\underset{\dot{}}{-}b$$
11		fveq2	$$⊢a=A\to F\left(a\right)=F\left(A\right)$$
12	11	oveq1d	$$⊢a=A\to F\left(a\right)\underset{\dot{}}{-}F\left(b\right)=F\left(A\right)\underset{\dot{}}{-}F\left(b\right)$$
13		oveq1	$$⊢a=A\to a\underset{\dot{}}{-}b=A\underset{\dot{}}{-}b$$
14	12 13	eqeq12d	$$⊢a=A\to \left(F\left(a\right)\underset{\dot{}}{-}F\left(b\right)=a\underset{\dot{}}{-}b\leftrightarrow F\left(A\right)\underset{\dot{}}{-}F\left(b\right)=A\underset{\dot{}}{-}b\right)$$
15		fveq2	$$⊢b=B\to F\left(b\right)=F\left(B\right)$$
16	15	oveq2d	$$⊢b=B\to F\left(A\right)\underset{\dot{}}{-}F\left(b\right)=F\left(A\right)\underset{\dot{}}{-}F\left(B\right)$$
17		oveq2	$$⊢b=B\to A\underset{\dot{}}{-}b=A\underset{\dot{}}{-}B$$
18	16 17	eqeq12d	$$⊢b=B\to \left(F\left(A\right)\underset{\dot{}}{-}F\left(b\right)=A\underset{\dot{}}{-}b\leftrightarrow F\left(A\right)\underset{\dot{}}{-}F\left(B\right)=A\underset{\dot{}}{-}B\right)$$
19	14 18	rspc2va	$$⊢\left(\left(A\in P\wedge B\in P\right)\wedge \forall a\in P\forall b\in PF\left(a\right)\underset{\dot{}}{-}F\left(b\right)=a\underset{\dot{}}{-}b\right)\to F\left(A\right)\underset{\dot{}}{-}F\left(B\right)=A\underset{\dot{}}{-}B$$
20	4 5 10 19	syl21anc	$$⊢\phi \to F\left(A\right)\underset{\dot{}}{-}F\left(B\right)=A\underset{\dot{}}{-}B$$