colmid

Description: Colinearity and equidistance implies midpoint. Theorem 7.20 of Schwabhauser p. 52. (Contributed by Thierry Arnoux, 30-Jul-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}$
	colmid.m	$⊢ M = S (X)$
	colmid.a	$⊢ φ \to A \in P$
	colmid.b	$⊢ φ \to B \in P$
	colmid.x	$⊢ φ \to X \in P$
	colmid.c	$⊢ φ \to (X \in (A L B) \lor A = B)$
	colmid.d	$⊢ φ \to X \underset{˙}{-} A = X \underset{˙}{-} B$
Assertion	colmid	$⊢ φ \to (B = M (A) \lor A = B)$

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		colmid.m	$⊢ M = S (X)$
8		colmid.a	$⊢ φ \to A \in P$
9		colmid.b	$⊢ φ \to B \in P$
10		colmid.x	$⊢ φ \to X \in P$
11		colmid.c	$⊢ φ \to (X \in (A L B) \lor A = B)$
12		colmid.d	$⊢ φ \to X \underset{˙}{-} A = X \underset{˙}{-} B$
13		animorr	$⊢ (φ \land A = B) \to (B = M (A) \lor A = B)$
14	6	ad2antrr	$⊢ ((φ \land A \neq B) \land X \in (A I B)) \to G \in 𝒢_{Tarski}$
15	10	ad2antrr	$⊢ ((φ \land A \neq B) \land X \in (A I B)) \to X \in P$
16	8	ad2antrr	$⊢ ((φ \land A \neq B) \land X \in (A I B)) \to A \in P$
17	9	ad2antrr	$⊢ ((φ \land A \neq B) \land X \in (A I B)) \to B \in P$
18	12	ad2antrr	$⊢ ((φ \land A \neq B) \land X \in (A I B)) \to X \underset{˙}{-} A = X \underset{˙}{-} B$
19	18	eqcomd	$⊢ ((φ \land A \neq B) \land X \in (A I B)) \to X \underset{˙}{-} B = X \underset{˙}{-} A$
20		simpr	$⊢ ((φ \land A \neq B) \land X \in (A I B)) \to X \in (A I B)$
21	1 2 3 14 16 15 17 20	tgbtwncom	$⊢ ((φ \land A \neq B) \land X \in (A I B)) \to X \in (B I A)$
22	1 2 3 4 5 14 15 7 16 17 19 21	ismir	$⊢ ((φ \land A \neq B) \land X \in (A I B)) \to B = M (A)$
23	22	orcd	$⊢ ((φ \land A \neq B) \land X \in (A I B)) \to (B = M (A) \lor A = B)$
24	6	adantr	$⊢ (φ \land A \in (X I B)) \to G \in 𝒢_{Tarski}$
25	9	adantr	$⊢ (φ \land A \in (X I B)) \to B \in P$
26	8	adantr	$⊢ (φ \land A \in (X I B)) \to A \in P$
27	10	adantr	$⊢ (φ \land A \in (X I B)) \to X \in P$
28		simpr	$⊢ (φ \land A \in (X I B)) \to A \in (X I B)$
29	1 2 3 24 27 26 25 28	tgbtwncom	$⊢ (φ \land A \in (X I B)) \to A \in (B I X)$
30	1 2 3 24 26 27	tgbtwntriv1	$⊢ (φ \land A \in (X I B)) \to A \in (A I X)$
31	1 2 3 6 10 8 10 9 12	tgcgrcomlr	$⊢ φ \to A \underset{˙}{-} X = B \underset{˙}{-} X$
32	31	adantr	$⊢ (φ \land A \in (X I B)) \to A \underset{˙}{-} X = B \underset{˙}{-} X$
33	32	eqcomd	$⊢ (φ \land A \in (X I B)) \to B \underset{˙}{-} X = A \underset{˙}{-} X$
34		eqidd	$⊢ (φ \land A \in (X I B)) \to A \underset{˙}{-} X = A \underset{˙}{-} X$
35	1 2 3 24 25 26 27 26 26 27 29 30 33 34	tgcgrsub	$⊢ (φ \land A \in (X I B)) \to B \underset{˙}{-} A = A \underset{˙}{-} A$
36	1 2 3 24 25 26 26 35	axtgcgrid	$⊢ (φ \land A \in (X I B)) \to B = A$
37	36	eqcomd	$⊢ (φ \land A \in (X I B)) \to A = B$
38	37	adantlr	$⊢ ((φ \land A \neq B) \land A \in (X I B)) \to A = B$
39	38	olcd	$⊢ ((φ \land A \neq B) \land A \in (X I B)) \to (B = M (A) \lor A = B)$
40	6	adantr	$⊢ (φ \land B \in (A I X)) \to G \in 𝒢_{Tarski}$
41	8	adantr	$⊢ (φ \land B \in (A I X)) \to A \in P$
42	9	adantr	$⊢ (φ \land B \in (A I X)) \to B \in P$
43	10	adantr	$⊢ (φ \land B \in (A I X)) \to X \in P$
44		simpr	$⊢ (φ \land B \in (A I X)) \to B \in (A I X)$
45	1 2 3 40 42 43	tgbtwntriv1	$⊢ (φ \land B \in (A I X)) \to B \in (B I X)$
46	31	adantr	$⊢ (φ \land B \in (A I X)) \to A \underset{˙}{-} X = B \underset{˙}{-} X$
47		eqidd	$⊢ (φ \land B \in (A I X)) \to B \underset{˙}{-} X = B \underset{˙}{-} X$
48	1 2 3 40 41 42 43 42 42 43 44 45 46 47	tgcgrsub	$⊢ (φ \land B \in (A I X)) \to A \underset{˙}{-} B = B \underset{˙}{-} B$
49	1 2 3 40 41 42 42 48	axtgcgrid	$⊢ (φ \land B \in (A I X)) \to A = B$
50	49	adantlr	$⊢ ((φ \land A \neq B) \land B \in (A I X)) \to A = B$
51	50	olcd	$⊢ ((φ \land A \neq B) \land B \in (A I X)) \to (B = M (A) \lor A = B)$
52		df-ne	$⊢ A \neq B \leftrightarrow \neg A = B$
53	11	orcomd	$⊢ φ \to (A = B \lor X \in (A L B))$
54	53	orcanai	$⊢ (φ \land \neg A = B) \to X \in (A L B)$
55	52 54	sylan2b	$⊢ (φ \land A \neq B) \to X \in (A L B)$
56	6	adantr	$⊢ (φ \land A \neq B) \to G \in 𝒢_{Tarski}$
57	8	adantr	$⊢ (φ \land A \neq B) \to A \in P$
58	9	adantr	$⊢ (φ \land A \neq B) \to B \in P$
59		simpr	$⊢ (φ \land A \neq B) \to A \neq B$
60	10	adantr	$⊢ (φ \land A \neq B) \to X \in P$
61	1 4 3 56 57 58 59 60	tgellng	$⊢ (φ \land A \neq B) \to (X \in (A L B) \leftrightarrow (X \in (A I B) \lor A \in (X I B) \lor B \in (A I X)))$
62	55 61	mpbid	$⊢ (φ \land A \neq B) \to (X \in (A I B) \lor A \in (X I B) \lor B \in (A I X))$
63	23 39 51 62	mpjao3dan	$⊢ (φ \land A \neq B) \to (B = M (A) \lor A = B)$
64	13 63	pm2.61dane	$⊢ φ \to (B = M (A) \lor A = B)$

Metamath Proof Explorer

Theorem colmid

Proof