Theorem ismot

Description: Property of being an isometry mapping to the same space. In geometry, this is also called a motion. (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)$$
Assertion	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)$$

Proof

Step	Hyp	Ref	Expression
1		ismot.p	$$⊢P={\mathrm{Base}}_G$$
2		ismot.m	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
3	1 1 2 2	isismt	$$⊢\left(G\in V\wedge G\in V\right)\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)$$
4	3	anidms	$$⊢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)$$