Theorem 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	⊢ 𝑃 = ( Base ‘ 𝐺 )
	mirval.d	⊢ − = ( dist ‘ 𝐺 )
	mirval.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	mirval.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	mirval.s	⊢ 𝑆 = ( pInvG ‘ 𝐺 )
	mirval.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	colmid.m	⊢ 𝑀 = ( 𝑆 ‘ 𝑋 )
	colmid.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
	colmid.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
	colmid.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
	colmid.c	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
	colmid.d	⊢ ( 𝜑 → ( 𝑋 − 𝐴 ) = ( 𝑋 − 𝐵 ) )
Assertion	colmid	⊢ ( 𝜑 → ( 𝐵 = ( 𝑀 ‘ 𝐴 ) ∨ 𝐴 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		mirval.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		mirval.d	⊢ − = ( dist ‘ 𝐺 )
3		mirval.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
4		mirval.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
5		mirval.s	⊢ 𝑆 = ( pInvG ‘ 𝐺 )
6		mirval.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
7		colmid.m	⊢ 𝑀 = ( 𝑆 ‘ 𝑋 )
8		colmid.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
9		colmid.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
10		colmid.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
11		colmid.c	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
12		colmid.d	⊢ ( 𝜑 → ( 𝑋 − 𝐴 ) = ( 𝑋 − 𝐵 ) )
13		animorr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → ( 𝐵 = ( 𝑀 ‘ 𝐴 ) ∨ 𝐴 = 𝐵 ) )
14	6	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑋 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐺 ∈ TarskiG )
15	10	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑋 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝑋 ∈ 𝑃 )
16	8	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑋 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐴 ∈ 𝑃 )
17	9	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑋 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐵 ∈ 𝑃 )
18	12	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑋 ∈ ( 𝐴 𝐼 𝐵 ) ) → ( 𝑋 − 𝐴 ) = ( 𝑋 − 𝐵 ) )
19	18	eqcomd	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑋 ∈ ( 𝐴 𝐼 𝐵 ) ) → ( 𝑋 − 𝐵 ) = ( 𝑋 − 𝐴 ) )
20		simpr	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑋 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝑋 ∈ ( 𝐴 𝐼 𝐵 ) )
21	1 2 3 14 16 15 17 20	tgbtwncom	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑋 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝑋 ∈ ( 𝐵 𝐼 𝐴 ) )
22	1 2 3 4 5 14 15 7 16 17 19 21	ismir	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑋 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐵 = ( 𝑀 ‘ 𝐴 ) )
23	22	orcd	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑋 ∈ ( 𝐴 𝐼 𝐵 ) ) → ( 𝐵 = ( 𝑀 ‘ 𝐴 ) ∨ 𝐴 = 𝐵 ) )
24	6	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝑋 𝐼 𝐵 ) ) → 𝐺 ∈ TarskiG )
25	9	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝑋 𝐼 𝐵 ) ) → 𝐵 ∈ 𝑃 )
26	8	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝑋 𝐼 𝐵 ) ) → 𝐴 ∈ 𝑃 )
27	10	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝑋 𝐼 𝐵 ) ) → 𝑋 ∈ 𝑃 )
28		simpr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝑋 𝐼 𝐵 ) ) → 𝐴 ∈ ( 𝑋 𝐼 𝐵 ) )
29	1 2 3 24 27 26 25 28	tgbtwncom	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝑋 𝐼 𝐵 ) ) → 𝐴 ∈ ( 𝐵 𝐼 𝑋 ) )
30	1 2 3 24 26 27	tgbtwntriv1	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝑋 𝐼 𝐵 ) ) → 𝐴 ∈ ( 𝐴 𝐼 𝑋 ) )
31	1 2 3 6 10 8 10 9 12	tgcgrcomlr	⊢ ( 𝜑 → ( 𝐴 − 𝑋 ) = ( 𝐵 − 𝑋 ) )
32	31	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝑋 𝐼 𝐵 ) ) → ( 𝐴 − 𝑋 ) = ( 𝐵 − 𝑋 ) )
33	32	eqcomd	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝑋 𝐼 𝐵 ) ) → ( 𝐵 − 𝑋 ) = ( 𝐴 − 𝑋 ) )
34		eqidd	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝑋 𝐼 𝐵 ) ) → ( 𝐴 − 𝑋 ) = ( 𝐴 − 𝑋 ) )
35	1 2 3 24 25 26 27 26 26 27 29 30 33 34	tgcgrsub	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝑋 𝐼 𝐵 ) ) → ( 𝐵 − 𝐴 ) = ( 𝐴 − 𝐴 ) )
36	1 2 3 24 25 26 26 35	axtgcgrid	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝑋 𝐼 𝐵 ) ) → 𝐵 = 𝐴 )
37	36	eqcomd	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝑋 𝐼 𝐵 ) ) → 𝐴 = 𝐵 )
38	37	adantlr	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝐴 ∈ ( 𝑋 𝐼 𝐵 ) ) → 𝐴 = 𝐵 )
39	38	olcd	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝐴 ∈ ( 𝑋 𝐼 𝐵 ) ) → ( 𝐵 = ( 𝑀 ‘ 𝐴 ) ∨ 𝐴 = 𝐵 ) )
40	6	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐴 𝐼 𝑋 ) ) → 𝐺 ∈ TarskiG )
41	8	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐴 𝐼 𝑋 ) ) → 𝐴 ∈ 𝑃 )
42	9	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐴 𝐼 𝑋 ) ) → 𝐵 ∈ 𝑃 )
43	10	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐴 𝐼 𝑋 ) ) → 𝑋 ∈ 𝑃 )
44		simpr	⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐴 𝐼 𝑋 ) ) → 𝐵 ∈ ( 𝐴 𝐼 𝑋 ) )
45	1 2 3 40 42 43	tgbtwntriv1	⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐴 𝐼 𝑋 ) ) → 𝐵 ∈ ( 𝐵 𝐼 𝑋 ) )
46	31	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐴 𝐼 𝑋 ) ) → ( 𝐴 − 𝑋 ) = ( 𝐵 − 𝑋 ) )
47		eqidd	⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐴 𝐼 𝑋 ) ) → ( 𝐵 − 𝑋 ) = ( 𝐵 − 𝑋 ) )
48	1 2 3 40 41 42 43 42 42 43 44 45 46 47	tgcgrsub	⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐴 𝐼 𝑋 ) ) → ( 𝐴 − 𝐵 ) = ( 𝐵 − 𝐵 ) )
49	1 2 3 40 41 42 42 48	axtgcgrid	⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐴 𝐼 𝑋 ) ) → 𝐴 = 𝐵 )
50	49	adantlr	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝐵 ∈ ( 𝐴 𝐼 𝑋 ) ) → 𝐴 = 𝐵 )
51	50	olcd	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝐵 ∈ ( 𝐴 𝐼 𝑋 ) ) → ( 𝐵 = ( 𝑀 ‘ 𝐴 ) ∨ 𝐴 = 𝐵 ) )
52		df-ne	⊢ ( 𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵 )
53	11	orcomd	⊢ ( 𝜑 → ( 𝐴 = 𝐵 ∨ 𝑋 ∈ ( 𝐴 𝐿 𝐵 ) ) )
54	53	orcanai	⊢ ( ( 𝜑 ∧ ¬ 𝐴 = 𝐵 ) → 𝑋 ∈ ( 𝐴 𝐿 𝐵 ) )
55	52 54	sylan2b	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝑋 ∈ ( 𝐴 𝐿 𝐵 ) )
56	6	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐺 ∈ TarskiG )
57	8	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ∈ 𝑃 )
58	9	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐵 ∈ 𝑃 )
59		simpr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ≠ 𝐵 )
60	10	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝑋 ∈ 𝑃 )
61	1 4 3 56 57 58 59 60	tgellng	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → ( 𝑋 ∈ ( 𝐴 𝐿 𝐵 ) ↔ ( 𝑋 ∈ ( 𝐴 𝐼 𝐵 ) ∨ 𝐴 ∈ ( 𝑋 𝐼 𝐵 ) ∨ 𝐵 ∈ ( 𝐴 𝐼 𝑋 ) ) ) )
62	55 61	mpbid	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → ( 𝑋 ∈ ( 𝐴 𝐼 𝐵 ) ∨ 𝐴 ∈ ( 𝑋 𝐼 𝐵 ) ∨ 𝐵 ∈ ( 𝐴 𝐼 𝑋 ) ) )
63	23 39 51 62	mpjao3dan	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → ( 𝐵 = ( 𝑀 ‘ 𝐴 ) ∨ 𝐴 = 𝐵 ) )
64	13 63	pm2.61dane	⊢ ( 𝜑 → ( 𝐵 = ( 𝑀 ‘ 𝐴 ) ∨ 𝐴 = 𝐵 ) )