Theorem lmimot

Description: Line mirroring is a motion of the geometric space. Theorem 10.11 of Schwabhauser p. 90. (Contributed by Thierry Arnoux, 15-Dec-2019)

	Ref	Expression
Hypotheses	ismid.p	$$⊢P={\mathrm{Base}}_G$$
	ismid.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
	ismid.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
	ismid.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	ismid.1	$$⊢\phi \to G{\mathrm{Dim}}_{𝒢}\ge 2$$
	lmif.m	$$⊢M={lInv}_{𝒢}\left(G\right)\left(D\right)$$
	lmif.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
	lmif.d	$$⊢\phi \to D\in \mathrm{ran}L$$
Assertion	lmimot	$$⊢\phi \to M\in \left(GIsmtG\right)$$

Proof

Step	Hyp	Ref	Expression
1		ismid.p	$$⊢P={\mathrm{Base}}_G$$
2		ismid.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
3		ismid.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
4		ismid.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
5		ismid.1	$$⊢\phi \to G{\mathrm{Dim}}_{𝒢}\ge 2$$
6		lmif.m	$$⊢M={lInv}_{𝒢}\left(G\right)\left(D\right)$$
7		lmif.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
8		lmif.d	$$⊢\phi \to D\in \mathrm{ran}L$$
9	1 2 3 4 5 6 7 8	lmif1o	$$⊢\phi \to M:P\underset{1-1\; onto}{⟶}P$$
10	4	adantr	$$⊢\left(\phi \wedge \left(a\in P\wedge b\in P\right)\right)\to G\in {𝒢}_{\mathrm{Tarski}}$$
11	5	adantr	$$⊢\left(\phi \wedge \left(a\in P\wedge b\in P\right)\right)\to G{\mathrm{Dim}}_{𝒢}\ge 2$$
12	8	adantr	$$⊢\left(\phi \wedge \left(a\in P\wedge b\in P\right)\right)\to D\in \mathrm{ran}L$$
13		simprl	$$⊢\left(\phi \wedge \left(a\in P\wedge b\in P\right)\right)\to a\in P$$
14		simprr	$$⊢\left(\phi \wedge \left(a\in P\wedge b\in P\right)\right)\to b\in P$$
15	1 2 3 10 11 6 7 12 13 14	lmiiso	$$⊢\left(\phi \wedge \left(a\in P\wedge b\in P\right)\right)\to M\left(a\right)\underset{\dot{}}{-}M\left(b\right)=a\underset{\dot{}}{-}b$$
16	15	ralrimivva	$$⊢\phi \to \forall a\in P\forall b\in PM\left(a\right)\underset{\dot{}}{-}M\left(b\right)=a\underset{\dot{}}{-}b$$
17	1 2	ismot	$$⊢G\in {𝒢}_{\mathrm{Tarski}}\to \left(M\in \left(GIsmtG\right)\leftrightarrow \left(M:P\underset{1-1\; onto}{⟶}P\wedge \forall a\in P\forall b\in PM\left(a\right)\underset{\dot{}}{-}M\left(b\right)=a\underset{\dot{}}{-}b\right)\right)$$
18	4 17	syl	$$⊢\phi \to \left(M\in \left(GIsmtG\right)\leftrightarrow \left(M:P\underset{1-1\; onto}{⟶}P\wedge \forall a\in P\forall b\in PM\left(a\right)\underset{\dot{}}{-}M\left(b\right)=a\underset{\dot{}}{-}b\right)\right)$$
19	9 16 18	mpbir2and	$$⊢\phi \to M\in \left(GIsmtG\right)$$