Theorem tglowdim2l

Description: Reformulation of the lower dimension axiom for dimension two. There exist three non-colinear points. Theorem 6.24 of Schwabhauser p. 46. (Contributed by Thierry Arnoux, 30-May-2019)

	Ref	Expression
Hypotheses	tglineintmo.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	tglineintmo.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	tglineintmo.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	tglineintmo.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	tglowdim2l.1	⊢ ( 𝜑 → 𝐺 DimTarskiG≥ 2 )
Assertion	tglowdim2l	⊢ ( 𝜑 → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ¬ ( 𝑐 ∈ ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) )

Proof

Step	Hyp	Ref	Expression
1		tglineintmo.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		tglineintmo.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
3		tglineintmo.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
4		tglineintmo.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5		tglowdim2l.1	⊢ ( 𝜑 → 𝐺 DimTarskiG≥ 2 )
6		eqid	⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
7	1 6 2 4 5	axtglowdim2	⊢ ( 𝜑 → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ¬ ( 𝑐 ∈ ( 𝑎 𝐼 𝑏 ) ∨ 𝑎 ∈ ( 𝑐 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝑎 𝐼 𝑐 ) ) )
8	4	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) → 𝐺 ∈ TarskiG )
9		simpllr	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) → 𝑎 ∈ 𝑃 )
10		simplr	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) → 𝑏 ∈ 𝑃 )
11		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) → 𝑐 ∈ 𝑃 )
12	1 3 2 8 9 10 11	tgcolg	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) → ( ( 𝑐 ∈ ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ↔ ( 𝑐 ∈ ( 𝑎 𝐼 𝑏 ) ∨ 𝑎 ∈ ( 𝑐 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝑎 𝐼 𝑐 ) ) ) )
13	12	notbid	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) → ( ¬ ( 𝑐 ∈ ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ↔ ¬ ( 𝑐 ∈ ( 𝑎 𝐼 𝑏 ) ∨ 𝑎 ∈ ( 𝑐 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝑎 𝐼 𝑐 ) ) ) )
14	13	rexbidva	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) → ( ∃ 𝑐 ∈ 𝑃 ¬ ( 𝑐 ∈ ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ↔ ∃ 𝑐 ∈ 𝑃 ¬ ( 𝑐 ∈ ( 𝑎 𝐼 𝑏 ) ∨ 𝑎 ∈ ( 𝑐 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝑎 𝐼 𝑐 ) ) ) )
15	14	rexbidva	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) → ( ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ¬ ( 𝑐 ∈ ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ↔ ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ¬ ( 𝑐 ∈ ( 𝑎 𝐼 𝑏 ) ∨ 𝑎 ∈ ( 𝑐 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝑎 𝐼 𝑐 ) ) ) )
16	15	rexbidva	⊢ ( 𝜑 → ( ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ¬ ( 𝑐 ∈ ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ↔ ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ¬ ( 𝑐 ∈ ( 𝑎 𝐼 𝑏 ) ∨ 𝑎 ∈ ( 𝑐 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝑎 𝐼 𝑐 ) ) ) )
17	7 16	mpbird	⊢ ( 𝜑 → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ¬ ( 𝑐 ∈ ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) )