oppnid

Description: The "opposite to a line" relation is irreflexive. (Contributed by Thierry Arnoux, 4-Mar-2020)

	Ref	Expression
Hypotheses	hpg.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	hpg.d	⊢ − = ( dist ‘ 𝐺 )
	hpg.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	hpg.o	⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐷 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐷 ) ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
	opphl.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	opphl.d	⊢ ( 𝜑 → 𝐷 ∈ ran 𝐿 )
	opphl.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	oppnid.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
Assertion	oppnid	⊢ ( 𝜑 → ¬ 𝐴 𝑂 𝐴 )

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		oppnid.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
9	7	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝐴 𝑂 𝐴 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐴 ) ) → 𝐺 ∈ TarskiG )
10	8	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝐴 𝑂 𝐴 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐴 ) ) → 𝐴 ∈ 𝑃 )
11	6	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝐴 𝑂 𝐴 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐴 ) ) → 𝐷 ∈ ran 𝐿 )
12		simplr	⊢ ( ( ( ( 𝜑 ∧ 𝐴 𝑂 𝐴 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐴 ) ) → 𝑡 ∈ 𝐷 )
13	1 5 3 9 11 12	tglnpt	⊢ ( ( ( ( 𝜑 ∧ 𝐴 𝑂 𝐴 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐴 ) ) → 𝑡 ∈ 𝑃 )
14		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝐴 𝑂 𝐴 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐴 ) ) → 𝑡 ∈ ( 𝐴 𝐼 𝐴 ) )
15	1 2 3 9 10 13 14	axtgbtwnid	⊢ ( ( ( ( 𝜑 ∧ 𝐴 𝑂 𝐴 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐴 ) ) → 𝐴 = 𝑡 )
16	15 12	eqeltrd	⊢ ( ( ( ( 𝜑 ∧ 𝐴 𝑂 𝐴 ) ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐴 ) ) → 𝐴 ∈ 𝐷 )
17	1 2 3 4 8 8	islnopp	⊢ ( 𝜑 → ( 𝐴 𝑂 𝐴 ↔ ( ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 𝐴 ) ) ) )
18	17	simplbda	⊢ ( ( 𝜑 ∧ 𝐴 𝑂 𝐴 ) → ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 𝐴 ) )
19	16 18	r19.29a	⊢ ( ( 𝜑 ∧ 𝐴 𝑂 𝐴 ) → 𝐴 ∈ 𝐷 )
20	17	simprbda	⊢ ( ( 𝜑 ∧ 𝐴 𝑂 𝐴 ) → ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐴 ∈ 𝐷 ) )
21	20	simpld	⊢ ( ( 𝜑 ∧ 𝐴 𝑂 𝐴 ) → ¬ 𝐴 ∈ 𝐷 )
22	19 21	pm2.65da	⊢ ( 𝜑 → ¬ 𝐴 𝑂 𝐴 )

Metamath Proof Explorer

Theorem oppnid

Proof