Theorem mirbtwni

Description: Point inversion preserves betweenness, first half of Theorem 7.15 of Schwabhauser p. 51. (Contributed by Thierry Arnoux, 9-Jun-2019)

	Ref	Expression
Hypotheses	mirval.p	$$⊢P={\mathrm{Base}}_G$$
	mirval.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
	mirval.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
	mirval.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
	mirval.s	$$⊢S={pInv}_{𝒢}\left(G\right)$$
	mirval.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	mirval.a	$$⊢\phi \to A\in P$$
	mirfv.m	$$⊢M=S\left(A\right)$$
	miriso.1	$$⊢\phi \to X\in P$$
	miriso.2	$$⊢\phi \to Y\in P$$
	mirbtwni.z	$$⊢\phi \to Z\in P$$
	mirbtwni.b	$$⊢\phi \to Y\in \left(XIZ\right)$$
Assertion	mirbtwni	$$⊢\phi \to M\left(Y\right)\in \left(M\left(X\right)IM\left(Z\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		mirval.p	$$⊢P={\mathrm{Base}}_G$$
2		mirval.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
3		mirval.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
4		mirval.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
5		mirval.s	$$⊢S={pInv}_{𝒢}\left(G\right)$$
6		mirval.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
7		mirval.a	$$⊢\phi \to A\in P$$
8		mirfv.m	$$⊢M=S\left(A\right)$$
9		miriso.1	$$⊢\phi \to X\in P$$
10		miriso.2	$$⊢\phi \to Y\in P$$
11		mirbtwni.z	$$⊢\phi \to Z\in P$$
12		mirbtwni.b	$$⊢\phi \to Y\in \left(XIZ\right)$$
13		eqid	$$⊢{\sim }_{𝒢}\left(G\right)={\sim }_{𝒢}\left(G\right)$$
14	1 2 3 4 5 6 7 8	mirf	$$⊢\phi \to M:P⟶P$$
15	14 9	ffvelrnd	$$⊢\phi \to M\left(X\right)\in P$$
16	14 10	ffvelrnd	$$⊢\phi \to M\left(Y\right)\in P$$
17	14 11	ffvelrnd	$$⊢\phi \to M\left(Z\right)\in P$$
18	1 2 3 4 5 6 7 8 9 10	miriso	$$⊢\phi \to M\left(X\right)\underset{\dot{}}{-}M\left(Y\right)=X\underset{\dot{}}{-}Y$$
19	18	eqcomd	$$⊢\phi \to X\underset{\dot{}}{-}Y=M\left(X\right)\underset{\dot{}}{-}M\left(Y\right)$$
20	1 2 3 4 5 6 7 8 10 11	miriso	$$⊢\phi \to M\left(Y\right)\underset{\dot{}}{-}M\left(Z\right)=Y\underset{\dot{}}{-}Z$$
21	20	eqcomd	$$⊢\phi \to Y\underset{\dot{}}{-}Z=M\left(Y\right)\underset{\dot{}}{-}M\left(Z\right)$$
22	1 2 3 4 5 6 7 8 11 9	miriso	$$⊢\phi \to M\left(Z\right)\underset{\dot{}}{-}M\left(X\right)=Z\underset{\dot{}}{-}X$$
23	22	eqcomd	$$⊢\phi \to Z\underset{\dot{}}{-}X=M\left(Z\right)\underset{\dot{}}{-}M\left(X\right)$$
24	1 2 13 6 9 10 11 15 16 17 19 21 23	trgcgr	$$⊢\phi \to ⟨“XYZ”⟩{\sim }_{𝒢}\left(G\right)⟨“M\left(X\right)M\left(Y\right)M\left(Z\right)”⟩$$
25	1 2 3 13 6 9 10 11 15 16 17 24 12	tgbtwnxfr	$$⊢\phi \to M\left(Y\right)\in \left(M\left(X\right)IM\left(Z\right)\right)$$