Theorem opptgdim2

Description: If two points opposite to a line exist, dimension must be 2 or more. (Contributed by Thierry Arnoux, 3-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 )
	oppcom.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
	oppcom.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
	oppcom.o	⊢ ( 𝜑 → 𝐴 𝑂 𝐵 )
Assertion	opptgdim2	⊢ ( 𝜑 → 𝐺 DimTarskiG≥ 2 )

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	7	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝐷 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝐺 ∈ TarskiG )
12		simpllr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝐷 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝑥 ∈ 𝑃 )
13		simplr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝐷 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝑦 ∈ 𝑃 )
14	8	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝐷 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝐴 ∈ 𝑃 )
15	1 2 3 4 5 6 7 8 9 10	oppne1	⊢ ( 𝜑 → ¬ 𝐴 ∈ 𝐷 )
16	15	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝐷 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → ¬ 𝐴 ∈ 𝐷 )
17		simprl	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝐷 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝐷 = ( 𝑥 𝐿 𝑦 ) )
18	16 17	neleqtrd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝐷 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → ¬ 𝐴 ∈ ( 𝑥 𝐿 𝑦 ) )
19		simprr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝐷 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝑥 ≠ 𝑦 )
20	19	neneqd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝐷 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → ¬ 𝑥 = 𝑦 )
21		ioran	⊢ ( ¬ ( 𝐴 ∈ ( 𝑥 𝐿 𝑦 ) ∨ 𝑥 = 𝑦 ) ↔ ( ¬ 𝐴 ∈ ( 𝑥 𝐿 𝑦 ) ∧ ¬ 𝑥 = 𝑦 ) )
22	18 20 21	sylanbrc	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝐷 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → ¬ ( 𝐴 ∈ ( 𝑥 𝐿 𝑦 ) ∨ 𝑥 = 𝑦 ) )
23	1 5 3 11 12 13 14 22	ncoltgdim2	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝐷 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝐺 DimTarskiG≥ 2 )
24	1 3 5 7 6	tgisline	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝐷 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) )
25	23 24	r19.29vva	⊢ ( 𝜑 → 𝐺 DimTarskiG≥ 2 )