tglineinteq

Description: Two distinct lines intersect in at most one point. Theorem 6.21 of Schwabhauser p. 46. (Contributed by Thierry Arnoux, 6-Aug-2019)

	Ref	Expression
Hypotheses	tglineintmo.p	$⊢ P = {Base}_{G}$
	tglineintmo.i	$⊢ I = Itv (G)$
	tglineintmo.l	$⊢ L = {Line}_{𝒢} (G)$
	tglineintmo.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	tglineinteq.a	$⊢ φ \to A \in P$
	tglineinteq.b	$⊢ φ \to B \in P$
	tglineinteq.c	$⊢ φ \to C \in P$
	tglineinteq.d	$⊢ φ \to D \in P$
	tglineinteq.e	$⊢ φ \to \neg (A \in (B L C) \lor B = C)$
	tglineinteq.1	$⊢ φ \to X \in (A L B)$
	tglineinteq.2	$⊢ φ \to Y \in (A L B)$
	tglineinteq.3	$⊢ φ \to X \in (C L D)$
	tglineinteq.4	$⊢ φ \to Y \in (C L D)$
Assertion	tglineinteq	$⊢ φ \to X = Y$

Proof

Step	Hyp	Ref	Expression
1		tglineintmo.p	$⊢ P = {Base}_{G}$
2		tglineintmo.i	$⊢ I = Itv (G)$
3		tglineintmo.l	$⊢ L = {Line}_{𝒢} (G)$
4		tglineintmo.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		tglineinteq.a	$⊢ φ \to A \in P$
6		tglineinteq.b	$⊢ φ \to B \in P$
7		tglineinteq.c	$⊢ φ \to C \in P$
8		tglineinteq.d	$⊢ φ \to D \in P$
9		tglineinteq.e	$⊢ φ \to \neg (A \in (B L C) \lor B = C)$
10		tglineinteq.1	$⊢ φ \to X \in (A L B)$
11		tglineinteq.2	$⊢ φ \to Y \in (A L B)$
12		tglineinteq.3	$⊢ φ \to X \in (C L D)$
13		tglineinteq.4	$⊢ φ \to Y \in (C L D)$
14	1 3 2 4 5 6 10	tglngne	$⊢ φ \to A \neq B$
15	1 2 3 4 5 6 14	tgelrnln	$⊢ φ \to A L B \in ran L$
16	1 3 2 4 7 8 12	tglngne	$⊢ φ \to C \neq D$
17	1 2 3 4 7 8 16	tgelrnln	$⊢ φ \to C L D \in ran L$
18	1 2 3 4 5 6 7 8 9	tglineneq	$⊢ φ \to A L B \neq C L D$
19	1 2 3 4 15 17 18	tglineintmo	$⊢ φ \to \exists^{*} x (x \in (A L B) \land x \in (C L D))$
20	10 12	jca	$⊢ φ \to (X \in (A L B) \land X \in (C L D))$
21	11 13	jca	$⊢ φ \to (Y \in (A L B) \land Y \in (C L D))$
22		eleq1	$⊢ x = X \to (x \in (A L B) \leftrightarrow X \in (A L B))$
23		eleq1	$⊢ x = X \to (x \in (C L D) \leftrightarrow X \in (C L D))$
24	22 23	anbi12d	$⊢ x = X \to ((x \in (A L B) \land x \in (C L D)) \leftrightarrow (X \in (A L B) \land X \in (C L D)))$
25		eleq1	$⊢ x = Y \to (x \in (A L B) \leftrightarrow Y \in (A L B))$
26		eleq1	$⊢ x = Y \to (x \in (C L D) \leftrightarrow Y \in (C L D))$
27	25 26	anbi12d	$⊢ x = Y \to ((x \in (A L B) \land x \in (C L D)) \leftrightarrow (Y \in (A L B) \land Y \in (C L D)))$
28	24 27	moi	$⊢ ((X \in (A L B) \land Y \in (A L B)) \land \exists^{*} x (x \in (A L B) \land x \in (C L D)) \land ((X \in (A L B) \land X \in (C L D)) \land (Y \in (A L B) \land Y \in (C L D)))) \to X = Y$
29	10 11 19 20 21 28	syl212anc	$⊢ φ \to X = Y$

Metamath Proof Explorer

Theorem tglineinteq

Proof