Theorem lmiopp

Description: Line mirroring produces points on the opposite side of the mirroring line. Theorem 10.14 of Schwabhauser p. 92. (Contributed by Thierry Arnoux, 2-Aug-2020)

	Ref	Expression
Hypotheses	lmiopp.p	$$⊢P={\mathrm{Base}}_G$$
	lmiopp.m	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
	lmiopp.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
	lmiopp.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
	lmiopp.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	lmiopp.h	$$⊢\phi \to G{\mathrm{Dim}}_{𝒢}\ge 2$$
	lmiopp.d	$$⊢\phi \to D\in \mathrm{ran}L$$
	lmiopp.o	$$⊢O=\left\{⟨a,b⟩|\left(\left(a\in \left(P\setminus D\right)\wedge b\in \left(P\setminus D\right)\right)\wedge \exists t\in Dt\in \left(aIb\right)\right)\right\}$$
	lmiopp.n	$$⊢M={lInv}_{𝒢}\left(G\right)\left(D\right)$$
	lmiopp.a	$$⊢\phi \to A\in P$$
	lmiopp.1	$$⊢\phi \to \neg A\in D$$
Assertion	lmiopp	$$⊢\phi \to AOM\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		lmiopp.p	$$⊢P={\mathrm{Base}}_G$$
2		lmiopp.m	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
3		lmiopp.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
4		lmiopp.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
5		lmiopp.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
6		lmiopp.h	$$⊢\phi \to G{\mathrm{Dim}}_{𝒢}\ge 2$$
7		lmiopp.d	$$⊢\phi \to D\in \mathrm{ran}L$$
8		lmiopp.o	$$⊢O=\left\{⟨a,b⟩|\left(\left(a\in \left(P\setminus D\right)\wedge b\in \left(P\setminus D\right)\right)\wedge \exists t\in Dt\in \left(aIb\right)\right)\right\}$$
9		lmiopp.n	$$⊢M={lInv}_{𝒢}\left(G\right)\left(D\right)$$
10		lmiopp.a	$$⊢\phi \to A\in P$$
11		lmiopp.1	$$⊢\phi \to \neg A\in D$$
12	1 2 3 5 6 9 4 7 10	lmicl	$$⊢\phi \to M\left(A\right)\in P$$
13		eqidd	$$⊢\phi \to M\left(A\right)=M\left(A\right)$$
14	1 2 3 5 6 9 4 7 10 12	islmib	$$⊢\phi \to \left(M\left(A\right)=M\left(A\right)\leftrightarrow \left(A{mid}_{𝒢}\left(G\right)M\left(A\right)\in D\wedge \left(D{⟂}_{𝒢}\left(G\right)\left(ALM\left(A\right)\right)\vee A=M\left(A\right)\right)\right)\right)$$
15	13 14	mpbid	$$⊢\phi \to \left(A{mid}_{𝒢}\left(G\right)M\left(A\right)\in D\wedge \left(D{⟂}_{𝒢}\left(G\right)\left(ALM\left(A\right)\right)\vee A=M\left(A\right)\right)\right)$$
16	15	simpld	$$⊢\phi \to A{mid}_{𝒢}\left(G\right)M\left(A\right)\in D$$
17	1 2 3 5 6 9 4 7 10	lmilmi	$$⊢\phi \to M\left(M\left(A\right)\right)=A$$
18	17	eqeq1d	$$⊢\phi \to \left(M\left(M\left(A\right)\right)=M\left(A\right)\leftrightarrow A=M\left(A\right)\right)$$
19	1 2 3 5 6 9 4 7 12	lmiinv	$$⊢\phi \to \left(M\left(M\left(A\right)\right)=M\left(A\right)\leftrightarrow M\left(A\right)\in D\right)$$
20		eqcom	$$⊢A=M\left(A\right)\leftrightarrow M\left(A\right)=A$$
21	20	a1i	$$⊢\phi \to \left(A=M\left(A\right)\leftrightarrow M\left(A\right)=A\right)$$
22	18 19 21	3bitr3d	$$⊢\phi \to \left(M\left(A\right)\in D\leftrightarrow M\left(A\right)=A\right)$$
23	1 2 3 5 6 9 4 7 10	lmiinv	$$⊢\phi \to \left(M\left(A\right)=A\leftrightarrow A\in D\right)$$
24	22 23	bitrd	$$⊢\phi \to \left(M\left(A\right)\in D\leftrightarrow A\in D\right)$$
25	11 24	mtbird	$$⊢\phi \to \neg M\left(A\right)\in D$$
26	1 2 3 5 6 10 12	midbtwn	$$⊢\phi \to A{mid}_{𝒢}\left(G\right)M\left(A\right)\in \left(AIM\left(A\right)\right)$$
27	1 2 3 8 10 12 16 11 25 26	islnoppd	$$⊢\phi \to AOM\left(A\right)$$