Metamath Proof Explorer


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 ( 𝜑 → ∃ 𝑎𝑃𝑏𝑃𝑐𝑃 ¬ ( 𝑐 ∈ ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) )