Theorem coltr3

Description: A transitivity law for colinearity. (Contributed by Thierry Arnoux, 27-Nov-2019)

	Ref	Expression
Hypotheses	tglineintmo.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	tglineintmo.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	tglineintmo.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	tglineintmo.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	coltr.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
	coltr.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
	coltr.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
	coltr.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
	coltr.1	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) )
	coltr3.2	⊢ ( 𝜑 → 𝐷 ∈ ( 𝐴 𝐼 𝐶 ) )
Assertion	coltr3	⊢ ( 𝜑 → 𝐷 ∈ ( 𝐵 𝐿 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		tglineintmo.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		tglineintmo.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
3		tglineintmo.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
4		tglineintmo.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5		coltr.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
6		coltr.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
7		coltr.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
8		coltr.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
9		coltr.1	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) )
10		coltr3.2	⊢ ( 𝜑 → 𝐷 ∈ ( 𝐴 𝐼 𝐶 ) )
11		eqid	⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
12	4	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → 𝐺 ∈ TarskiG )
13	5	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → 𝐴 ∈ 𝑃 )
14	8	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → 𝐷 ∈ 𝑃 )
15	10	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → 𝐷 ∈ ( 𝐴 𝐼 𝐶 ) )
16		simpr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → 𝐴 = 𝐶 )
17	16	oveq2d	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → ( 𝐴 𝐼 𝐴 ) = ( 𝐴 𝐼 𝐶 ) )
18	15 17	eleqtrrd	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → 𝐷 ∈ ( 𝐴 𝐼 𝐴 ) )
19	1 11 2 12 13 14 18	axtgbtwnid	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → 𝐴 = 𝐷 )
20	9	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) )
21	19 20	eqeltrrd	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → 𝐷 ∈ ( 𝐵 𝐿 𝐶 ) )
22	4	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) → 𝐺 ∈ TarskiG )
23	5	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) → 𝐴 ∈ 𝑃 )
24	7	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) → 𝐶 ∈ 𝑃 )
25	8	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) → 𝐷 ∈ 𝑃 )
26		simpr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) → 𝐴 ≠ 𝐶 )
27	10	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) → 𝐷 ∈ ( 𝐴 𝐼 𝐶 ) )
28	1 2 3 22 23 24 25 26 27	btwnlng1	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) → 𝐷 ∈ ( 𝐴 𝐿 𝐶 ) )
29	26	necomd	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) → 𝐶 ≠ 𝐴 )
30	6	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) → 𝐵 ∈ 𝑃 )
31	1 3 2 4 6 7 9	tglngne	⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
32	31	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) → 𝐵 ≠ 𝐶 )
33	9	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) → 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) )
34	1 2 3 22 24 23 30 29 33 32	lnrot1	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) → 𝐵 ∈ ( 𝐶 𝐿 𝐴 ) )
35	1 2 3 22 24 23 29 30 32 34	tglineelsb2	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) → ( 𝐶 𝐿 𝐴 ) = ( 𝐶 𝐿 𝐵 ) )
36	1 2 3 22 23 24 26	tglinecom	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) → ( 𝐴 𝐿 𝐶 ) = ( 𝐶 𝐿 𝐴 ) )
37	1 2 3 4 6 7 31	tglinecom	⊢ ( 𝜑 → ( 𝐵 𝐿 𝐶 ) = ( 𝐶 𝐿 𝐵 ) )
38	37	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) → ( 𝐵 𝐿 𝐶 ) = ( 𝐶 𝐿 𝐵 ) )
39	35 36 38	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) → ( 𝐴 𝐿 𝐶 ) = ( 𝐵 𝐿 𝐶 ) )
40	28 39	eleqtrd	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) → 𝐷 ∈ ( 𝐵 𝐿 𝐶 ) )
41	21 40	pm2.61dane	⊢ ( 𝜑 → 𝐷 ∈ ( 𝐵 𝐿 𝐶 ) )