oppne3

Description: Points lying on opposite sides of a line cannot be equal. (Contributed by Thierry Arnoux, 3-Aug-2020)

	Ref	Expression
Hypotheses	hpg.p	$⊢ P = {Base}_{G}$
	hpg.d	$⊢ \underset{˙}{-} = dist (G)$
	hpg.i	$⊢ I = Itv (G)$
	hpg.o	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ D) \land b \in (P ∖ D)) \land \exists t \in D t \in (a I b))\}$
	opphl.l	$⊢ L = {Line}_{𝒢} (G)$
	opphl.d	$⊢ φ \to D \in ran L$
	opphl.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	oppcom.a	$⊢ φ \to A \in P$
	oppcom.b	$⊢ φ \to B \in P$
	oppcom.o	$⊢ φ \to A O B$
Assertion	oppne3	$⊢ φ \to A \neq B$

Proof

Step	Hyp	Ref	Expression
1		hpg.p	$⊢ P = {Base}_{G}$
2		hpg.d	$⊢ \underset{˙}{-} = dist (G)$
3		hpg.i	$⊢ I = Itv (G)$
4		hpg.o	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ D) \land b \in (P ∖ D)) \land \exists t \in D t \in (a I b))\}$
5		opphl.l	$⊢ L = {Line}_{𝒢} (G)$
6		opphl.d	$⊢ φ \to D \in ran L$
7		opphl.g	$⊢ φ \to G \in 𝒢_{Tarski}$
8		oppcom.a	$⊢ φ \to A \in P$
9		oppcom.b	$⊢ φ \to B \in P$
10		oppcom.o	$⊢ φ \to A O B$
11	1 2 3 4 5 6 7 8 9 10	oppne1	$⊢ φ \to \neg A \in D$
12	7	ad3antrrr	$⊢ (((φ \land A = B) \land t \in D) \land t \in (A I B)) \to G \in 𝒢_{Tarski}$
13	8	ad3antrrr	$⊢ (((φ \land A = B) \land t \in D) \land t \in (A I B)) \to A \in P$
14	6	ad3antrrr	$⊢ (((φ \land A = B) \land t \in D) \land t \in (A I B)) \to D \in ran L$
15		simplr	$⊢ (((φ \land A = B) \land t \in D) \land t \in (A I B)) \to t \in D$
16	1 5 3 12 14 15	tglnpt	$⊢ (((φ \land A = B) \land t \in D) \land t \in (A I B)) \to t \in P$
17		simpr	$⊢ (((φ \land A = B) \land t \in D) \land t \in (A I B)) \to t \in (A I B)$
18		simpllr	$⊢ (((φ \land A = B) \land t \in D) \land t \in (A I B)) \to A = B$
19	18	oveq2d	$⊢ (((φ \land A = B) \land t \in D) \land t \in (A I B)) \to A I A = A I B$
20	17 19	eleqtrrd	$⊢ (((φ \land A = B) \land t \in D) \land t \in (A I B)) \to t \in (A I A)$
21	1 2 3 12 13 16 20	axtgbtwnid	$⊢ (((φ \land A = B) \land t \in D) \land t \in (A I B)) \to A = t$
22	21 15	eqeltrd	$⊢ (((φ \land A = B) \land t \in D) \land t \in (A I B)) \to A \in D$
23	1 2 3 4 8 9	islnopp	$⊢ φ \to (A O B \leftrightarrow ((\neg A \in D \land \neg B \in D) \land \exists t \in D t \in (A I B)))$
24	10 23	mpbid	$⊢ φ \to ((\neg A \in D \land \neg B \in D) \land \exists t \in D t \in (A I B))$
25	24	simprd	$⊢ φ \to \exists t \in D t \in (A I B)$
26	25	adantr	$⊢ (φ \land A = B) \to \exists t \in D t \in (A I B)$
27	22 26	r19.29a	$⊢ (φ \land A = B) \to A \in D$
28	11 27	mtand	$⊢ φ \to \neg A = B$
29	28	neqned	$⊢ φ \to A \neq B$

Metamath Proof Explorer

Theorem oppne3

Proof