Metamath Proof Explorer

Theorem tglowdim2ln

Description: There is always one point outside of any line. Theorem 6.25 of Schwabhauser p. 46. (Contributed by Thierry Arnoux, 16-Nov-2019)

Ref Expression
Hypotheses tglineintmo.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
tglineintmo.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
tglineintmo.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
tglineintmo.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
tglowdim2l.1 ⊢ ( 𝜑 → 𝐺 DimTarskiG≥ 2 )
tglowdim2ln.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
tglowdim2ln.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
tglowdim2ln.1 ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
Assertion tglowdim2ln ( 𝜑 → ∃ 𝑐 ∈ 𝑃 ¬ 𝑐 ∈ ( 𝐴 𝐿 𝐵 ) )

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 tglowdim2ln.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
7 tglowdim2ln.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
8 tglowdim2ln.1 ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
9 1 2 3 4 5 tglowdim2l ⊢ ( 𝜑 → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ¬ ( 𝑧 ∈ ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) )
10 9 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑐 ∈ 𝑃 𝑐 ∈ ( 𝐴 𝐿 𝐵 ) ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ¬ ( 𝑧 ∈ ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) )
11 eleq1w ⊢ ( 𝑐 = 𝑧 → ( 𝑐 ∈ ( 𝐴 𝐿 𝐵 ) ↔ 𝑧 ∈ ( 𝐴 𝐿 𝐵 ) ) )
12 simpllr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑐 ∈ 𝑃 𝑐 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃 ) ) ∧ ¬ 𝑎 = 𝑏 ) → ∀ 𝑐 ∈ 𝑃 𝑐 ∈ ( 𝐴 𝐿 𝐵 ) )
13 simplr3 ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑐 ∈ 𝑃 𝑐 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃 ) ) ∧ ¬ 𝑎 = 𝑏 ) → 𝑧 ∈ 𝑃 )
14 11 12 13 rspcdva ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑐 ∈ 𝑃 𝑐 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃 ) ) ∧ ¬ 𝑎 = 𝑏 ) → 𝑧 ∈ ( 𝐴 𝐿 𝐵 ) )
15 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑐 ∈ 𝑃 𝑐 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃 ) ) ∧ ¬ 𝑎 = 𝑏 ) → 𝐺 ∈ TarskiG )
16 simplr1 ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑐 ∈ 𝑃 𝑐 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃 ) ) ∧ ¬ 𝑎 = 𝑏 ) → 𝑎 ∈ 𝑃 )
17 simplr2 ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑐 ∈ 𝑃 𝑐 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃 ) ) ∧ ¬ 𝑎 = 𝑏 ) → 𝑏 ∈ 𝑃 )
18 simpr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑐 ∈ 𝑃 𝑐 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃 ) ) ∧ ¬ 𝑎 = 𝑏 ) → ¬ 𝑎 = 𝑏 )
19 18 neqned ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑐 ∈ 𝑃 𝑐 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃 ) ) ∧ ¬ 𝑎 = 𝑏 ) → 𝑎 ≠ 𝑏 )
20 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑐 ∈ 𝑃 𝑐 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃 ) ) ∧ ¬ 𝑎 = 𝑏 ) → 𝐴 ∈ 𝑃 )
21 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑐 ∈ 𝑃 𝑐 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃 ) ) ∧ ¬ 𝑎 = 𝑏 ) → 𝐵 ∈ 𝑃 )
22 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑐 ∈ 𝑃 𝑐 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃 ) ) ∧ ¬ 𝑎 = 𝑏 ) → 𝐴 ≠ 𝐵 )
23 1 2 3 15 20 21 22 tgelrnln ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑐 ∈ 𝑃 𝑐 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃 ) ) ∧ ¬ 𝑎 = 𝑏 ) → ( 𝐴 𝐿 𝐵 ) ∈ ran 𝐿 )
24 eleq1w ⊢ ( 𝑐 = 𝑎 → ( 𝑐 ∈ ( 𝐴 𝐿 𝐵 ) ↔ 𝑎 ∈ ( 𝐴 𝐿 𝐵 ) ) )
25 24 12 16 rspcdva ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑐 ∈ 𝑃 𝑐 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃 ) ) ∧ ¬ 𝑎 = 𝑏 ) → 𝑎 ∈ ( 𝐴 𝐿 𝐵 ) )
26 eleq1w ⊢ ( 𝑐 = 𝑏 → ( 𝑐 ∈ ( 𝐴 𝐿 𝐵 ) ↔ 𝑏 ∈ ( 𝐴 𝐿 𝐵 ) ) )
27 26 12 17 rspcdva ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑐 ∈ 𝑃 𝑐 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃 ) ) ∧ ¬ 𝑎 = 𝑏 ) → 𝑏 ∈ ( 𝐴 𝐿 𝐵 ) )
28 1 2 3 15 16 17 19 19 23 25 27 tglinethru ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑐 ∈ 𝑃 𝑐 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃 ) ) ∧ ¬ 𝑎 = 𝑏 ) → ( 𝐴 𝐿 𝐵 ) = ( 𝑎 𝐿 𝑏 ) )
29 14 28 eleqtrd ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑐 ∈ 𝑃 𝑐 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃 ) ) ∧ ¬ 𝑎 = 𝑏 ) → 𝑧 ∈ ( 𝑎 𝐿 𝑏 ) )
30 29 ex ⊢ ( ( ( 𝜑 ∧ ∀ 𝑐 ∈ 𝑃 𝑐 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃 ) ) → ( ¬ 𝑎 = 𝑏 → 𝑧 ∈ ( 𝑎 𝐿 𝑏 ) ) )
31 30 orrd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑐 ∈ 𝑃 𝑐 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃 ) ) → ( 𝑎 = 𝑏 ∨ 𝑧 ∈ ( 𝑎 𝐿 𝑏 ) ) )
32 31 orcomd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑐 ∈ 𝑃 𝑐 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃 ) ) → ( 𝑧 ∈ ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) )
33 32 ralrimivvva ⊢ ( ( 𝜑 ∧ ∀ 𝑐 ∈ 𝑃 𝑐 ∈ ( 𝐴 𝐿 𝐵 ) ) → ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) )
34 dfral2 ⊢ ( ∀ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ↔ ¬ ∃ 𝑧 ∈ 𝑃 ¬ ( 𝑧 ∈ ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) )
35 34 ralbii ⊢ ( ∀ 𝑏 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ↔ ∀ 𝑏 ∈ 𝑃 ¬ ∃ 𝑧 ∈ 𝑃 ¬ ( 𝑧 ∈ ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) )
36 ralnex ⊢ ( ∀ 𝑏 ∈ 𝑃 ¬ ∃ 𝑧 ∈ 𝑃 ¬ ( 𝑧 ∈ ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ↔ ¬ ∃ 𝑏 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ¬ ( 𝑧 ∈ ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) )
37 35 36 bitri ⊢ ( ∀ 𝑏 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ↔ ¬ ∃ 𝑏 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ¬ ( 𝑧 ∈ ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) )
38 37 ralbii ⊢ ( ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ↔ ∀ 𝑎 ∈ 𝑃 ¬ ∃ 𝑏 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ¬ ( 𝑧 ∈ ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) )
39 ralnex ⊢ ( ∀ 𝑎 ∈ 𝑃 ¬ ∃ 𝑏 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ¬ ( 𝑧 ∈ ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ↔ ¬ ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ¬ ( 𝑧 ∈ ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) )
40 38 39 bitri ⊢ ( ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ↔ ¬ ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ¬ ( 𝑧 ∈ ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) )
41 33 40 sylib ⊢ ( ( 𝜑 ∧ ∀ 𝑐 ∈ 𝑃 𝑐 ∈ ( 𝐴 𝐿 𝐵 ) ) → ¬ ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ¬ ( 𝑧 ∈ ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) )
42 10 41 pm2.65da ⊢ ( 𝜑 → ¬ ∀ 𝑐 ∈ 𝑃 𝑐 ∈ ( 𝐴 𝐿 𝐵 ) )
43 rexnal ⊢ ( ∃ 𝑐 ∈ 𝑃 ¬ 𝑐 ∈ ( 𝐴 𝐿 𝐵 ) ↔ ¬ ∀ 𝑐 ∈ 𝑃 𝑐 ∈ ( 𝐴 𝐿 𝐵 ) )
44 42 43 sylibr ⊢ ( 𝜑 → ∃ 𝑐 ∈ 𝑃 ¬ 𝑐 ∈ ( 𝐴 𝐿 𝐵 ) )