Theorem tglndim0

Description: There are no lines in dimension 0. (Contributed by Thierry Arnoux, 18-Oct-2019)

	Ref	Expression
Hypotheses	tglineelsb2.p	⊢ 𝐵 = ( Base ‘ 𝐺 )
	tglineelsb2.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	tglineelsb2.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	tglineelsb2.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	tglndim0.d	⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) = 1 )
Assertion	tglndim0	⊢ ( 𝜑 → ¬ 𝐴 ∈ ran 𝐿 )

Proof

Step	Hyp	Ref	Expression
1		tglineelsb2.p	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		tglineelsb2.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
3		tglineelsb2.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
4		tglineelsb2.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5		tglndim0.d	⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) = 1 )
6	5	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ ran 𝐿 ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → ( ♯ ‘ 𝐵 ) = 1 )
7		simpllr	⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ ran 𝐿 ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝑥 ∈ 𝐵 )
8		simplr	⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ ran 𝐿 ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝑦 ∈ 𝐵 )
9	1 6 7 8	tgldim0eq	⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ ran 𝐿 ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝑥 = 𝑦 )
10		simprr	⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ ran 𝐿 ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝑥 ≠ 𝑦 )
11	9 10	pm2.21ddne	⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ ran 𝐿 ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → ⊥ )
12	4	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ran 𝐿 ) → 𝐺 ∈ TarskiG )
13		simpr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ran 𝐿 ) → 𝐴 ∈ ran 𝐿 )
14	1 2 3 12 13	tgisline	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ran 𝐿 ) → ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) )
15	11 14	r19.29vva	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ran 𝐿 ) → ⊥ )
16	15	inegd	⊢ ( 𝜑 → ¬ 𝐴 ∈ ran 𝐿 )