Metamath Proof Explorer

Theorem colopp

Description: Opposite sides of a line for colinear points. Theorem 9.18 of Schwabhauser p. 73. (Contributed by Thierry Arnoux, 3-Aug-2020)

Ref Expression
Hypotheses hpgid.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
hpgid.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
hpgid.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
hpgid.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
hpgid.d ⊢ ( 𝜑 → 𝐷 ∈ ran 𝐿 )
hpgid.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
hpgid.o ⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐷 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐷 ) ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
colopp.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
colopp.p ⊢ ( 𝜑 → 𝐶 ∈ 𝐷 )
colopp.1 ⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
Assertion colopp ( 𝜑 → ( 𝐴 𝑂 𝐵 ↔ ( 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ∧ ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 hpgid.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 hpgid.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
3 hpgid.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
4 hpgid.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5 hpgid.d ⊢ ( 𝜑 → 𝐷 ∈ ran 𝐿 )
6 hpgid.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
7 hpgid.o ⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐷 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐷 ) ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
8 colopp.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
9 colopp.p ⊢ ( 𝜑 → 𝐶 ∈ 𝐷 )
10 colopp.1 ⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
11 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐺 ∈ TarskiG )
12 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐴 ∈ 𝑃 )
13 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐵 ∈ 𝑃 )
14 eqid ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
15 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐷 ∈ ran 𝐿 )
16 simpllr ⊢ ( ( ( ( 𝜑 ∧ ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ) → ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ) )
17 simplr ⊢ ( ( ( ( 𝜑 ∧ ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝑦 ∈ 𝐷 )
18 eleq1w ⊢ ( 𝑡 = 𝑦 → ( 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) ↔ 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ) )
19 18 adantl ⊢ ( ( ( ( ( 𝜑 ∧ ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ 𝑡 = 𝑦 ) → ( 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) ↔ 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ) )
20 simpr ⊢ ( ( ( ( 𝜑 ∧ ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) )
21 17 19 20 rspcedvd ⊢ ( ( ( ( 𝜑 ∧ ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ) → ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) )
22 1 14 2 7 6 8 islnopp ⊢ ( 𝜑 → ( 𝐴 𝑂 𝐵 ↔ ( ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) ) ) )
23 22 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ) → ( 𝐴 𝑂 𝐵 ↔ ( ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) ) ) )
24 16 21 23 mpbir2and ⊢ ( ( ( ( 𝜑 ∧ ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐴 𝑂 𝐵 )
25 1 14 2 7 3 15 11 12 13 24 oppne3 ⊢ ( ( ( ( 𝜑 ∧ ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐴 ≠ 𝐵 )
26 1 2 3 11 12 13 25 tgelrnln ⊢ ( ( ( ( 𝜑 ∧ ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ) → ( 𝐴 𝐿 𝐵 ) ∈ ran 𝐿 )
27 1 2 3 11 12 13 25 tglinerflx1 ⊢ ( ( ( ( 𝜑 ∧ ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐴 ∈ ( 𝐴 𝐿 𝐵 ) )
28 16 simpld ⊢ ( ( ( ( 𝜑 ∧ ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ) → ¬ 𝐴 ∈ 𝐷 )
29 nelne1 ⊢ ( ( 𝐴 ∈ ( 𝐴 𝐿 𝐵 ) ∧ ¬ 𝐴 ∈ 𝐷 ) → ( 𝐴 𝐿 𝐵 ) ≠ 𝐷 )
30 27 28 29 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ) → ( 𝐴 𝐿 𝐵 ) ≠ 𝐷 )
31 25 neneqd ⊢ ( ( ( ( 𝜑 ∧ ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ) → ¬ 𝐴 = 𝐵 )
32 10 orcomd ⊢ ( 𝜑 → ( 𝐴 = 𝐵 ∨ 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ) )
33 32 ord ⊢ ( 𝜑 → ( ¬ 𝐴 = 𝐵 → 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ) )
34 33 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ) → ( ¬ 𝐴 = 𝐵 → 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ) )
35 31 34 mpd ⊢ ( ( ( ( 𝜑 ∧ ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) )
36 9 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐶 ∈ 𝐷 )
37 35 36 elind ⊢ ( ( ( ( 𝜑 ∧ ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐶 ∈ ( ( 𝐴 𝐿 𝐵 ) ∩ 𝐷 ) )
38 1 3 2 11 15 17 tglnpt ⊢ ( ( ( ( 𝜑 ∧ ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝑦 ∈ 𝑃 )
39 1 2 3 11 12 13 38 25 20 btwnlng1 ⊢ ( ( ( ( 𝜑 ∧ ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝑦 ∈ ( 𝐴 𝐿 𝐵 ) )
40 39 17 elind ⊢ ( ( ( ( 𝜑 ∧ ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝑦 ∈ ( ( 𝐴 𝐿 𝐵 ) ∩ 𝐷 ) )
41 1 2 3 11 26 15 30 37 40 tglineineq ⊢ ( ( ( ( 𝜑 ∧ ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐶 = 𝑦 )
42 41 20 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) )
43 42 adantllr ⊢ ( ( ( ( ( 𝜑 ∧ ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ) ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) )
44 simpr ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ) ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) ) → ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) )
45 18 cbvrexvw ⊢ ( ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) ↔ ∃ 𝑦 ∈ 𝐷 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) )
46 44 45 sylib ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ) ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) ) → ∃ 𝑦 ∈ 𝐷 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) )
47 43 46 r19.29a ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ) ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) )
48 9 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐶 ∈ 𝐷 )
49 simpr ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ 𝑡 = 𝐶 ) → 𝑡 = 𝐶 )
50 49 eleq1d ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ 𝑡 = 𝐶 ) → ( 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) ↔ 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) )
51 simpr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) )
52 48 50 51 rspcedvd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) → ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) )
53 52 adantlr ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ) ) ∧ 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) → ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) )
54 47 53 impbida ⊢ ( ( 𝜑 ∧ ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ) ) → ( ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) ↔ 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) )
55 54 pm5.32da ⊢ ( 𝜑 → ( ( ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) ) ↔ ( ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ) ∧ 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) ) )
56 3anrot ⊢ ( ( 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ∧ ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ) ↔ ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) )
57 df-3an ⊢ ( ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) ↔ ( ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ) ∧ 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) )
58 56 57 bitri ⊢ ( ( 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ∧ ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ) ↔ ( ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ) ∧ 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) )
59 58 a1i ⊢ ( 𝜑 → ( ( 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ∧ ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ) ↔ ( ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ) ∧ 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) ) )
60 55 22 59 3bitr4d ⊢ ( 𝜑 → ( 𝐴 𝑂 𝐵 ↔ ( 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ∧ ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ) ) )