Theorem 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	⊢ 𝑃 = ( Base ‘ 𝐺 )
	hpg.d	⊢ − = ( dist ‘ 𝐺 )
	hpg.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	hpg.o	⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐷 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐷 ) ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
	opphl.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	opphl.d	⊢ ( 𝜑 → 𝐷 ∈ ran 𝐿 )
	opphl.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	oppcom.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
	oppcom.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
	oppcom.o	⊢ ( 𝜑 → 𝐴 𝑂 𝐵 )
Assertion	oppne3	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		hpg.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		hpg.d	⊢ − = ( dist ‘ 𝐺 )
3		hpg.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
4		hpg.o	⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐷 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐷 ) ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
5		opphl.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
6		opphl.d	⊢ ( 𝜑 → 𝐷 ∈ ran 𝐿 )
7		opphl.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
8		oppcom.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
9		oppcom.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
10		oppcom.o	⊢ ( 𝜑 → 𝐴 𝑂 𝐵 )
11	1 2 3 4 5 6 7 8 9 10	oppne1	⊢ ( 𝜑 → ¬ 𝐴 ∈ 𝐷 )
12	7	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐺 ∈ TarskiG )
13	8	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐴 ∈ 𝑃 )
14	6	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐷 ∈ ran 𝐿 )
15		simplr	⊢ ( ( ( ( 𝜑 ∧ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝑡 ∈ 𝐷 )
16	1 5 3 12 14 15	tglnpt	⊢ ( ( ( ( 𝜑 ∧ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝑡 ∈ 𝑃 )
17		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) )
18		simpllr	⊢ ( ( ( ( 𝜑 ∧ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐴 = 𝐵 )
19	18	oveq2d	⊢ ( ( ( ( 𝜑 ∧ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) ) → ( 𝐴 𝐼 𝐴 ) = ( 𝐴 𝐼 𝐵 ) )
20	17 19	eleqtrrd	⊢ ( ( ( ( 𝜑 ∧ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝑡 ∈ ( 𝐴 𝐼 𝐴 ) )
21	1 2 3 12 13 16 20	axtgbtwnid	⊢ ( ( ( ( 𝜑 ∧ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐴 = 𝑡 )
22	21 15	eqeltrd	⊢ ( ( ( ( 𝜑 ∧ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐴 ∈ 𝐷 )
23	1 2 3 4 8 9	islnopp	⊢ ( 𝜑 → ( 𝐴 𝑂 𝐵 ↔ ( ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) ) ) )
24	10 23	mpbid	⊢ ( 𝜑 → ( ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) ) )
25	24	simprd	⊢ ( 𝜑 → ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) )
26	25	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) )
27	22 26	r19.29a	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝐴 ∈ 𝐷 )
28	11 27	mtand	⊢ ( 𝜑 → ¬ 𝐴 = 𝐵 )
29	28	neqned	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )