tgcolg

Description: We choose the notation ( Z e. ( X L Y ) \/ X = Y ) instead of "colinear" in order to avoid defining an additional symbol for colinearity because LineG is a common structure slot for other axiomatizations of geometry. (Contributed by Thierry Arnoux, 25-May-2019)

	Ref	Expression
Hypotheses	tglngval.p	$⊢ P = {Base}_{G}$
	tglngval.l	$⊢ L = {Line}_{𝒢} (G)$
	tglngval.i	$⊢ I = Itv (G)$
	tglngval.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	tglngval.x	$⊢ φ \to X \in P$
	tglngval.y	$⊢ φ \to Y \in P$
	tgcolg.z	$⊢ φ \to Z \in P$
Assertion	tgcolg	$⊢ φ \to ((Z \in (X L Y) \lor X = Y) \leftrightarrow (Z \in (X I Y) \lor X \in (Z I Y) \lor Y \in (X I Z)))$

Proof

Step	Hyp	Ref	Expression
1		tglngval.p	$⊢ P = {Base}_{G}$
2		tglngval.l	$⊢ L = {Line}_{𝒢} (G)$
3		tglngval.i	$⊢ I = Itv (G)$
4		tglngval.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		tglngval.x	$⊢ φ \to X \in P$
6		tglngval.y	$⊢ φ \to Y \in P$
7		tgcolg.z	$⊢ φ \to Z \in P$
8		animorr	$⊢ (φ \land X = Y) \to (Z \in (X L Y) \lor X = Y)$
9		eqid	$⊢ dist (G) = dist (G)$
10	4	adantr	$⊢ (φ \land X = Y) \to G \in 𝒢_{Tarski}$
11	7	adantr	$⊢ (φ \land X = Y) \to Z \in P$
12	5	adantr	$⊢ (φ \land X = Y) \to X \in P$
13	1 9 3 10 11 12	tgbtwntriv2	$⊢ (φ \land X = Y) \to X \in (Z I X)$
14		simpr	$⊢ (φ \land X = Y) \to X = Y$
15	14	oveq2d	$⊢ (φ \land X = Y) \to Z I X = Z I Y$
16	13 15	eleqtrd	$⊢ (φ \land X = Y) \to X \in (Z I Y)$
17	16	3mix2d	$⊢ (φ \land X = Y) \to (Z \in (X I Y) \lor X \in (Z I Y) \lor Y \in (X I Z))$
18	8 17	2thd	$⊢ (φ \land X = Y) \to ((Z \in (X L Y) \lor X = Y) \leftrightarrow (Z \in (X I Y) \lor X \in (Z I Y) \lor Y \in (X I Z)))$
19		simpr	$⊢ (φ \land X \neq Y) \to X \neq Y$
20	19	neneqd	$⊢ (φ \land X \neq Y) \to \neg X = Y$
21		biorf	$⊢ \neg X = Y \to (Z \in (X L Y) \leftrightarrow (X = Y \lor Z \in (X L Y)))$
22	20 21	syl	$⊢ (φ \land X \neq Y) \to (Z \in (X L Y) \leftrightarrow (X = Y \lor Z \in (X L Y)))$
23		orcom	$⊢ (X = Y \lor Z \in (X L Y)) \leftrightarrow (Z \in (X L Y) \lor X = Y)$
24	22 23	bitrdi	$⊢ (φ \land X \neq Y) \to (Z \in (X L Y) \leftrightarrow (Z \in (X L Y) \lor X = Y))$
25	4	adantr	$⊢ (φ \land X \neq Y) \to G \in 𝒢_{Tarski}$
26	5	adantr	$⊢ (φ \land X \neq Y) \to X \in P$
27	6	adantr	$⊢ (φ \land X \neq Y) \to Y \in P$
28	7	adantr	$⊢ (φ \land X \neq Y) \to Z \in P$
29	1 2 3 25 26 27 19 28	tgellng	$⊢ (φ \land X \neq Y) \to (Z \in (X L Y) \leftrightarrow (Z \in (X I Y) \lor X \in (Z I Y) \lor Y \in (X I Z)))$
30	24 29	bitr3d	$⊢ (φ \land X \neq Y) \to ((Z \in (X L Y) \lor X = Y) \leftrightarrow (Z \in (X I Y) \lor X \in (Z I Y) \lor Y \in (X I Z)))$
31	18 30	pm2.61dane	$⊢ φ \to ((Z \in (X L Y) \lor X = Y) \leftrightarrow (Z \in (X I Y) \lor X \in (Z I Y) \lor Y \in (X I Z)))$

Metamath Proof Explorer

Theorem tgcolg

Proof