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 ( 𝜑 → ( 𝐴 𝑂 𝐵 ↔ ( 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ∧ ¬ 𝐴𝐷 ∧ ¬ 𝐵𝐷 ) ) )