Theorem cnvmot

Description: The converse of a motion is 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)$$
	motgrp.1	$$⊢\phi \to G\in V$$
	motco.2	$$⊢\phi \to F\in \left(GIsmtG\right)$$
Assertion	cnvmot	$$⊢\phi \to F^{-1}\in \left(GIsmtG\right)$$

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		motco.2	$$⊢\phi \to F\in \left(GIsmtG\right)$$
5	1 2 3 4	motf1o	$$⊢\phi \to F:P\underset{1-1\; onto}{⟶}P$$
6		f1ocnv	$$⊢F:P\underset{1-1\; onto}{⟶}P\to F^{-1}:P\underset{1-1\; onto}{⟶}P$$
7	5 6	syl	$$⊢\phi \to F^{-1}:P\underset{1-1\; onto}{⟶}P$$
8	3	adantr	$$⊢\left(\phi \wedge \left(a\in P\wedge b\in P\right)\right)\to G\in V$$
9		f1of	$$⊢F^{-1}:P\underset{1-1\; onto}{⟶}P\to F^{-1}:P⟶P$$
10	7 9	syl	$$⊢\phi \to F^{-1}:P⟶P$$
11	10	adantr	$$⊢\left(\phi \wedge \left(a\in P\wedge b\in P\right)\right)\to F^{-1}:P⟶P$$
12		simprl	$$⊢\left(\phi \wedge \left(a\in P\wedge b\in P\right)\right)\to a\in P$$
13	11 12	ffvelcdmd	$$⊢\left(\phi \wedge \left(a\in P\wedge b\in P\right)\right)\to F^{-1}\left(a\right)\in P$$
14		simprr	$$⊢\left(\phi \wedge \left(a\in P\wedge b\in P\right)\right)\to b\in P$$
15	11 14	ffvelcdmd	$$⊢\left(\phi \wedge \left(a\in P\wedge b\in P\right)\right)\to F^{-1}\left(b\right)\in P$$
16	4	adantr	$$⊢\left(\phi \wedge \left(a\in P\wedge b\in P\right)\right)\to F\in \left(GIsmtG\right)$$
17	1 2 8 13 15 16	motcgr	$$⊢\left(\phi \wedge \left(a\in P\wedge b\in P\right)\right)\to F\left(F^{-1}\left(a\right)\right)\underset{\dot{}}{-}F\left(F^{-1}\left(b\right)\right)=F^{-1}\left(a\right)\underset{\dot{}}{-}{F}^{-1}\left(b\right)$$
18		f1ocnvfv2	$$⊢\left(F:P\underset{1-1\; onto}{⟶}P\wedge a\in P\right)\to F\left(F^{-1}\left(a\right)\right)=a$$
19	5 12 18	syl2an2r	$$⊢\left(\phi \wedge \left(a\in P\wedge b\in P\right)\right)\to F\left(F^{-1}\left(a\right)\right)=a$$
20		f1ocnvfv2	$$⊢\left(F:P\underset{1-1\; onto}{⟶}P\wedge b\in P\right)\to F\left(F^{-1}\left(b\right)\right)=b$$
21	5 14 20	syl2an2r	$$⊢\left(\phi \wedge \left(a\in P\wedge b\in P\right)\right)\to F\left(F^{-1}\left(b\right)\right)=b$$
22	19 21	oveq12d	$$⊢\left(\phi \wedge \left(a\in P\wedge b\in P\right)\right)\to F\left(F^{-1}\left(a\right)\right)\underset{\dot{}}{-}F\left(F^{-1}\left(b\right)\right)=a\underset{\dot{}}{-}b$$
23	17 22	eqtr3d	$$⊢\left(\phi \wedge \left(a\in P\wedge b\in P\right)\right)\to F^{-1}\left(a\right)\underset{\dot{}}{-}{F}^{-1}\left(b\right)=a\underset{\dot{}}{-}b$$
24	23	ralrimivva	$$⊢\phi \to \forall a\in P\forall b\in P{F}^{-1}\left(a\right)\underset{\dot{}}{-}{F}^{-1}\left(b\right)=a\underset{\dot{}}{-}b$$
25	1 2	ismot	$$⊢G\in V\to \left(F^{-1}\in \left(GIsmtG\right)\leftrightarrow \left(F^{-1}:P\underset{1-1\; onto}{⟶}P\wedge \forall a\in P\forall b\in P{F}^{-1}\left(a\right)\underset{\dot{}}{-}{F}^{-1}\left(b\right)=a\underset{\dot{}}{-}b\right)\right)$$
26	3 25	syl	$$⊢\phi \to \left(F^{-1}\in \left(GIsmtG\right)\leftrightarrow \left(F^{-1}:P\underset{1-1\; onto}{⟶}P\wedge \forall a\in P\forall b\in P{F}^{-1}\left(a\right)\underset{\dot{}}{-}{F}^{-1}\left(b\right)=a\underset{\dot{}}{-}b\right)\right)$$
27	7 24 26	mpbir2and	$$⊢\phi \to F^{-1}\in \left(GIsmtG\right)$$