Metamath Proof Explorer


Theorem opphl

Description: If two points A and C lie on opposite sides of a line D , then any point of the half line ( R A ) also lies opposite to C . Theorem 9.5 of Schwabhauser p. 69. (Contributed by Thierry Arnoux, 3-Mar-2019)

Ref Expression
Hypotheses hpg.p P = Base G
hpg.d - ˙ = dist G
hpg.i I = Itv G
hpg.o O = a b | a P D b P D t D t a I b
opphl.l L = Line 𝒢 G
opphl.d φ D ran L
opphl.g φ G 𝒢 Tarski
opphl.k K = hl 𝒢 G
opphl.a φ A P
opphl.b φ B P
opphl.c φ C P
opphl.1 φ A O C
opphl.2 φ R D
opphl.3 φ A K R B
Assertion opphl φ B O C

Proof

Step Hyp Ref Expression
1 hpg.p P = Base G
2 hpg.d - ˙ = dist G
3 hpg.i I = Itv G
4 hpg.o O = a b | a P D b P D t D t a I b
5 opphl.l L = Line 𝒢 G
6 opphl.d φ D ran L
7 opphl.g φ G 𝒢 Tarski
8 opphl.k K = hl 𝒢 G
9 opphl.a φ A P
10 opphl.b φ B P
11 opphl.c φ C P
12 opphl.1 φ A O C
13 opphl.2 φ R D
14 opphl.3 φ A K R B
15 6 ad8antr φ x D A L x 𝒢 G D z D C L z 𝒢 G D m P z = pInv 𝒢 G m x y D B L y 𝒢 G D D ran L
16 7 ad8antr φ x D A L x 𝒢 G D z D C L z 𝒢 G D m P z = pInv 𝒢 G m x y D B L y 𝒢 G D G 𝒢 Tarski
17 eqid pInv 𝒢 G m = pInv 𝒢 G m
18 10 ad8antr φ x D A L x 𝒢 G D z D C L z 𝒢 G D m P z = pInv 𝒢 G m x y D B L y 𝒢 G D B P
19 eqid pInv 𝒢 G = pInv 𝒢 G
20 simp-4r φ x D A L x 𝒢 G D z D C L z 𝒢 G D m P z = pInv 𝒢 G m x y D B L y 𝒢 G D m P
21 9 ad8antr φ x D A L x 𝒢 G D z D C L z 𝒢 G D m P z = pInv 𝒢 G m x y D B L y 𝒢 G D A P
22 1 2 3 5 19 16 20 17 21 mircl φ x D A L x 𝒢 G D z D C L z 𝒢 G D m P z = pInv 𝒢 G m x y D B L y 𝒢 G D pInv 𝒢 G m A P
23 simplr φ x D A L x 𝒢 G D z D C L z 𝒢 G D m P z = pInv 𝒢 G m x y D B L y 𝒢 G D y D
24 simp-6r φ x D A L x 𝒢 G D z D C L z 𝒢 G D m P z = pInv 𝒢 G m x y D B L y 𝒢 G D z D
25 13 ad8antr φ x D A L x 𝒢 G D z D C L z 𝒢 G D m P z = pInv 𝒢 G m x y D B L y 𝒢 G D R D
26 11 ad8antr φ x D A L x 𝒢 G D z D C L z 𝒢 G D m P z = pInv 𝒢 G m x y D B L y 𝒢 G D C P
27 simp-8r φ x D A L x 𝒢 G D z D C L z 𝒢 G D m P z = pInv 𝒢 G m x y D B L y 𝒢 G D x D
28 12 ad8antr φ x D A L x 𝒢 G D z D C L z 𝒢 G D m P z = pInv 𝒢 G m x y D B L y 𝒢 G D A O C
29 simp-7r φ x D A L x 𝒢 G D z D C L z 𝒢 G D m P z = pInv 𝒢 G m x y D B L y 𝒢 G D A L x 𝒢 G D
30 5 16 29 perpln1 φ x D A L x 𝒢 G D z D C L z 𝒢 G D m P z = pInv 𝒢 G m x y D B L y 𝒢 G D A L x ran L
31 1 2 3 5 16 30 15 29 perpcom φ x D A L x 𝒢 G D z D C L z 𝒢 G D m P z = pInv 𝒢 G m x y D B L y 𝒢 G D D 𝒢 G A L x
32 simp-5r φ x D A L x 𝒢 G D z D C L z 𝒢 G D m P z = pInv 𝒢 G m x y D B L y 𝒢 G D C L z 𝒢 G D
33 5 16 32 perpln1 φ x D A L x 𝒢 G D z D C L z 𝒢 G D m P z = pInv 𝒢 G m x y D B L y 𝒢 G D C L z ran L
34 1 2 3 5 16 33 15 32 perpcom φ x D A L x 𝒢 G D z D C L z 𝒢 G D m P z = pInv 𝒢 G m x y D B L y 𝒢 G D D 𝒢 G C L z
35 1 5 3 16 15 27 tglnpt φ x D A L x 𝒢 G D z D C L z 𝒢 G D m P z = pInv 𝒢 G m x y D B L y 𝒢 G D x P
36 1 3 5 16 21 35 30 tglnne φ x D A L x 𝒢 G D z D C L z 𝒢 G D m P z = pInv 𝒢 G m x y D B L y 𝒢 G D A x
37 1 3 8 21 21 35 16 36 hlid φ x D A L x 𝒢 G D z D C L z 𝒢 G D m P z = pInv 𝒢 G m x y D B L y 𝒢 G D A K x A
38 simpllr φ x D A L x 𝒢 G D z D C L z 𝒢 G D m P z = pInv 𝒢 G m x y D B L y 𝒢 G D z = pInv 𝒢 G m x
39 38 eqcomd φ x D A L x 𝒢 G D z D C L z 𝒢 G D m P z = pInv 𝒢 G m x y D B L y 𝒢 G D pInv 𝒢 G m x = z
40 1 2 3 4 5 15 16 8 17 21 26 27 24 20 28 31 34 21 39 opphllem6 φ x D A L x 𝒢 G D z D C L z 𝒢 G D m P z = pInv 𝒢 G m x y D B L y 𝒢 G D A K x A pInv 𝒢 G m A K z C
41 37 40 mpbid φ x D A L x 𝒢 G D z D C L z 𝒢 G D m P z = pInv 𝒢 G m x y D B L y 𝒢 G D pInv 𝒢 G m A K z C
42 1 2 3 4 5 15 16 8 17 21 26 27 24 20 28 31 34 21 22 37 41 opphllem5 φ x D A L x 𝒢 G D z D C L z 𝒢 G D m P z = pInv 𝒢 G m x y D B L y 𝒢 G D A O pInv 𝒢 G m A
43 39 24 eqeltrd φ x D A L x 𝒢 G D z D C L z 𝒢 G D m P z = pInv 𝒢 G m x y D B L y 𝒢 G D pInv 𝒢 G m x D
44 1 2 3 5 19 16 17 15 20 27 43 mirln2 φ x D A L x 𝒢 G D z D C L z 𝒢 G D m P z = pInv 𝒢 G m x y D B L y 𝒢 G D m D
45 1 2 3 5 19 16 20 17 21 mirmir φ x D A L x 𝒢 G D z D C L z 𝒢 G D m P z = pInv 𝒢 G m x y D B L y 𝒢 G D pInv 𝒢 G m pInv 𝒢 G m A = A
46 45 eqcomd φ x D A L x 𝒢 G D z D C L z 𝒢 G D m P z = pInv 𝒢 G m x y D B L y 𝒢 G D A = pInv 𝒢 G m pInv 𝒢 G m A
47 1 5 3 7 6 13 tglnpt φ R P
48 1 3 8 9 10 47 7 14 hlne1 φ A R
49 48 ad8antr φ x D A L x 𝒢 G D z D C L z 𝒢 G D m P z = pInv 𝒢 G m x y D B L y 𝒢 G D A R
50 1 3 8 9 10 47 7 14 hlne2 φ B R
51 50 ad8antr φ x D A L x 𝒢 G D z D C L z 𝒢 G D m P z = pInv 𝒢 G m x y D B L y 𝒢 G D B R
52 1 3 8 9 10 47 7 ishlg φ A K R B A R B R A R I B B R I A
53 14 52 mpbid φ A R B R A R I B B R I A
54 53 simp3d φ A R I B B R I A
55 54 ad8antr φ x D A L x 𝒢 G D z D C L z 𝒢 G D m P z = pInv 𝒢 G m x y D B L y 𝒢 G D A R I B B R I A
56 1 2 3 4 5 15 16 17 21 18 22 25 42 44 46 49 51 55 opphllem2 φ x D A L x 𝒢 G D z D C L z 𝒢 G D m P z = pInv 𝒢 G m x y D B L y 𝒢 G D B O pInv 𝒢 G m A
57 simpr φ x D A L x 𝒢 G D z D C L z 𝒢 G D m P z = pInv 𝒢 G m x y D B L y 𝒢 G D B L y 𝒢 G D
58 5 16 57 perpln1 φ x D A L x 𝒢 G D z D C L z 𝒢 G D m P z = pInv 𝒢 G m x y D B L y 𝒢 G D B L y ran L
59 1 2 3 5 16 58 15 57 perpcom φ x D A L x 𝒢 G D z D C L z 𝒢 G D m P z = pInv 𝒢 G m x y D B L y 𝒢 G D D 𝒢 G B L y
60 1 5 3 16 15 24 tglnpt φ x D A L x 𝒢 G D z D C L z 𝒢 G D m P z = pInv 𝒢 G m x y D B L y 𝒢 G D z P
61 1 3 8 22 26 60 16 41 hlne1 φ x D A L x 𝒢 G D z D C L z 𝒢 G D m P z = pInv 𝒢 G m x y D B L y 𝒢 G D pInv 𝒢 G m A z
62 1 3 8 22 26 60 16 5 41 hlln φ x D A L x 𝒢 G D z D C L z 𝒢 G D m P z = pInv 𝒢 G m x y D B L y 𝒢 G D pInv 𝒢 G m A C L z
63 1 3 5 16 26 60 33 tglnne φ x D A L x 𝒢 G D z D C L z 𝒢 G D m P z = pInv 𝒢 G m x y D B L y 𝒢 G D C z
64 1 3 5 16 26 60 63 tglinerflx2 φ x D A L x 𝒢 G D z D C L z 𝒢 G D m P z = pInv 𝒢 G m x y D B L y 𝒢 G D z C L z
65 1 3 5 16 22 60 61 61 33 62 64 tglinethru φ x D A L x 𝒢 G D z D C L z 𝒢 G D m P z = pInv 𝒢 G m x y D B L y 𝒢 G D C L z = pInv 𝒢 G m A L z
66 34 65 breqtrd φ x D A L x 𝒢 G D z D C L z 𝒢 G D m P z = pInv 𝒢 G m x y D B L y 𝒢 G D D 𝒢 G pInv 𝒢 G m A L z
67 1 5 3 16 15 23 tglnpt φ x D A L x 𝒢 G D z D C L z 𝒢 G D m P z = pInv 𝒢 G m x y D B L y 𝒢 G D y P
68 1 3 5 16 18 67 58 tglnne φ x D A L x 𝒢 G D z D C L z 𝒢 G D m P z = pInv 𝒢 G m x y D B L y 𝒢 G D B y
69 1 3 8 18 21 67 16 68 hlid φ x D A L x 𝒢 G D z D C L z 𝒢 G D m P z = pInv 𝒢 G m x y D B L y 𝒢 G D B K y B
70 1 3 8 22 26 60 16 41 hlcomd φ x D A L x 𝒢 G D z D C L z 𝒢 G D m P z = pInv 𝒢 G m x y D B L y 𝒢 G D C K z pInv 𝒢 G m A
71 1 2 3 4 5 15 16 8 17 18 22 23 24 20 56 59 66 18 26 69 70 opphllem5 φ x D A L x 𝒢 G D z D C L z 𝒢 G D m P z = pInv 𝒢 G m x y D B L y 𝒢 G D B O C
72 1 2 3 4 5 6 7 9 11 12 oppne1 φ ¬ A D
73 1 3 8 9 10 47 7 5 14 hlln φ A B L R
74 73 adantr φ B D A B L R
75 7 adantr φ B D G 𝒢 Tarski
76 10 adantr φ B D B P
77 47 adantr φ B D R P
78 50 adantr φ B D B R
79 6 adantr φ B D D ran L
80 simpr φ B D B D
81 13 adantr φ B D R D
82 1 3 5 75 76 77 78 78 79 80 81 tglinethru φ B D D = B L R
83 74 82 eleqtrrd φ B D A D
84 72 83 mtand φ ¬ B D
85 1 2 3 5 7 6 10 84 footex φ y D B L y 𝒢 G D
86 85 ad6antr φ x D A L x 𝒢 G D z D C L z 𝒢 G D m P z = pInv 𝒢 G m x y D B L y 𝒢 G D
87 71 86 r19.29a φ x D A L x 𝒢 G D z D C L z 𝒢 G D m P z = pInv 𝒢 G m x B O C
88 7 ad4antr φ x D A L x 𝒢 G D z D C L z 𝒢 G D G 𝒢 Tarski
89 6 ad4antr φ x D A L x 𝒢 G D z D C L z 𝒢 G D D ran L
90 simp-4r φ x D A L x 𝒢 G D z D C L z 𝒢 G D x D
91 1 5 3 88 89 90 tglnpt φ x D A L x 𝒢 G D z D C L z 𝒢 G D x P
92 simplr φ x D A L x 𝒢 G D z D C L z 𝒢 G D z D
93 1 5 3 88 89 92 tglnpt φ x D A L x 𝒢 G D z D C L z 𝒢 G D z P
94 1 2 3 4 5 6 7 9 11 12 opptgdim2 φ G Dim 𝒢 2
95 94 ad4antr φ x D A L x 𝒢 G D z D C L z 𝒢 G D G Dim 𝒢 2
96 1 2 3 5 88 19 91 93 95 midex φ x D A L x 𝒢 G D z D C L z 𝒢 G D m P z = pInv 𝒢 G m x
97 87 96 r19.29a φ x D A L x 𝒢 G D z D C L z 𝒢 G D B O C
98 1 2 3 4 5 6 7 9 11 12 oppne2 φ ¬ C D
99 1 2 3 5 7 6 11 98 footex φ z D C L z 𝒢 G D
100 99 ad2antrr φ x D A L x 𝒢 G D z D C L z 𝒢 G D
101 97 100 r19.29a φ x D A L x 𝒢 G D B O C
102 1 2 3 5 7 6 9 72 footex φ x D A L x 𝒢 G D
103 101 102 r19.29a φ B O C