mirbtwnb

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

	Ref	Expression
Hypotheses	mirval.p	$⊢ P = {Base}_{G}$
	mirval.d	$⊢ \underset{˙}{-} = dist (G)$
	mirval.i	$⊢ I = Itv (G)$
	mirval.l	$⊢ L = {Line}_{𝒢} (G)$
	mirval.s	$⊢ S = {pInv}_{𝒢} (G)$
	mirval.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	mirval.a	$⊢ φ \to A \in P$
	mirfv.m	$⊢ M = S (A)$
	miriso.1	$⊢ φ \to X \in P$
	miriso.2	$⊢ φ \to Y \in P$
	mirbtwnb.z	$⊢ φ \to Z \in P$
Assertion	mirbtwnb	$⊢ φ \to (Y \in (X I Z) \leftrightarrow M (Y) \in (M (X) I M (Z)))$

Proof

Step	Hyp	Ref	Expression
1		mirval.p	$⊢ P = {Base}_{G}$
2		mirval.d	$⊢ \underset{˙}{-} = dist (G)$
3		mirval.i	$⊢ I = Itv (G)$
4		mirval.l	$⊢ L = {Line}_{𝒢} (G)$
5		mirval.s	$⊢ S = {pInv}_{𝒢} (G)$
6		mirval.g	$⊢ φ \to G \in 𝒢_{Tarski}$
7		mirval.a	$⊢ φ \to A \in P$
8		mirfv.m	$⊢ M = S (A)$
9		miriso.1	$⊢ φ \to X \in P$
10		miriso.2	$⊢ φ \to Y \in P$
11		mirbtwnb.z	$⊢ φ \to Z \in P$
12	6	adantr	$⊢ (φ \land Y \in (X I Z)) \to G \in 𝒢_{Tarski}$
13	7	adantr	$⊢ (φ \land Y \in (X I Z)) \to A \in P$
14	9	adantr	$⊢ (φ \land Y \in (X I Z)) \to X \in P$
15	10	adantr	$⊢ (φ \land Y \in (X I Z)) \to Y \in P$
16	11	adantr	$⊢ (φ \land Y \in (X I Z)) \to Z \in P$
17		simpr	$⊢ (φ \land Y \in (X I Z)) \to Y \in (X I Z)$
18	1 2 3 4 5 12 13 8 14 15 16 17	mirbtwni	$⊢ (φ \land Y \in (X I Z)) \to M (Y) \in (M (X) I M (Z))$
19	6	adantr	$⊢ (φ \land M (Y) \in (M (X) I M (Z))) \to G \in 𝒢_{Tarski}$
20	7	adantr	$⊢ (φ \land M (Y) \in (M (X) I M (Z))) \to A \in P$
21	1 2 3 4 5 19 20 8	mirf	$⊢ (φ \land M (Y) \in (M (X) I M (Z))) \to M : P ⟶ P$
22	9	adantr	$⊢ (φ \land M (Y) \in (M (X) I M (Z))) \to X \in P$
23	21 22	ffvelrnd	$⊢ (φ \land M (Y) \in (M (X) I M (Z))) \to M (X) \in P$
24	10	adantr	$⊢ (φ \land M (Y) \in (M (X) I M (Z))) \to Y \in P$
25	21 24	ffvelrnd	$⊢ (φ \land M (Y) \in (M (X) I M (Z))) \to M (Y) \in P$
26	11	adantr	$⊢ (φ \land M (Y) \in (M (X) I M (Z))) \to Z \in P$
27	21 26	ffvelrnd	$⊢ (φ \land M (Y) \in (M (X) I M (Z))) \to M (Z) \in P$
28		simpr	$⊢ (φ \land M (Y) \in (M (X) I M (Z))) \to M (Y) \in (M (X) I M (Z))$
29	1 2 3 4 5 19 20 8 23 25 27 28	mirbtwni	$⊢ (φ \land M (Y) \in (M (X) I M (Z))) \to M (M (Y)) \in (M (M (X)) I M (M (Z)))$
30	1 2 3 4 5 6 7 8 10	mirmir	$⊢ φ \to M (M (Y)) = Y$
31	1 2 3 4 5 6 7 8 9	mirmir	$⊢ φ \to M (M (X)) = X$
32	1 2 3 4 5 6 7 8 11	mirmir	$⊢ φ \to M (M (Z)) = Z$
33	31 32	oveq12d	$⊢ φ \to M (M (X)) I M (M (Z)) = X I Z$
34	30 33	eleq12d	$⊢ φ \to (M (M (Y)) \in (M (M (X)) I M (M (Z))) \leftrightarrow Y \in (X I Z))$
35	34	adantr	$⊢ (φ \land M (Y) \in (M (X) I M (Z))) \to (M (M (Y)) \in (M (M (X)) I M (M (Z))) \leftrightarrow Y \in (X I Z))$
36	29 35	mpbid	$⊢ (φ \land M (Y) \in (M (X) I M (Z))) \to Y \in (X I Z)$
37	18 36	impbida	$⊢ φ \to (Y \in (X I Z) \leftrightarrow M (Y) \in (M (X) I M (Z)))$

Metamath Proof Explorer

Theorem mirbtwnb

Proof