Metamath Proof Explorer


Theorem ishpg

Description: Value of the half-plane relation for a given line D . (Contributed by Thierry Arnoux, 4-Mar-2020)

Ref Expression
Hypotheses ishpg.p P = Base G
ishpg.i I = Itv G
ishpg.l L = Line 𝒢 G
ishpg.o O = a b | a P D b P D t D t a I b
ishpg.g φ G 𝒢 Tarski
ishpg.d φ D ran L
Assertion ishpg φ hp 𝒢 G D = a b | c P a O c b O c

Proof

Step Hyp Ref Expression
1 ishpg.p P = Base G
2 ishpg.i I = Itv G
3 ishpg.l L = Line 𝒢 G
4 ishpg.o O = a b | a P D b P D t D t a I b
5 ishpg.g φ G 𝒢 Tarski
6 ishpg.d φ D ran L
7 elex G 𝒢 Tarski G V
8 fveq2 g = G Line 𝒢 g = Line 𝒢 G
9 8 3 eqtr4di g = G Line 𝒢 g = L
10 9 rneqd g = G ran Line 𝒢 g = ran L
11 simpl p = P i = I p = P
12 11 difeq1d p = P i = I p d = P d
13 12 eleq2d p = P i = I a p d a P d
14 12 eleq2d p = P i = I c p d c P d
15 13 14 anbi12d p = P i = I a p d c p d a P d c P d
16 simpr p = P i = I i = I
17 16 oveqd p = P i = I a i c = a I c
18 17 eleq2d p = P i = I t a i c t a I c
19 18 rexbidv p = P i = I t d t a i c t d t a I c
20 15 19 anbi12d p = P i = I a p d c p d t d t a i c a P d c P d t d t a I c
21 12 eleq2d p = P i = I b p d b P d
22 21 14 anbi12d p = P i = I b p d c p d b P d c P d
23 16 oveqd p = P i = I b i c = b I c
24 23 eleq2d p = P i = I t b i c t b I c
25 24 rexbidv p = P i = I t d t b i c t d t b I c
26 22 25 anbi12d p = P i = I b p d c p d t d t b i c b P d c P d t d t b I c
27 20 26 anbi12d p = P i = I a p d c p d t d t a i c b p d c p d t d t b i c a P d c P d t d t a I c b P d c P d t d t b I c
28 11 27 rexeqbidv p = P i = I c p a p d c p d t d t a i c b p d c p d t d t b i c c P a P d c P d t d t a I c b P d c P d t d t b I c
29 1 2 28 sbcie2s g = G [˙Base g / p]˙ [˙ Itv g / i]˙ c p a p d c p d t d t a i c b p d c p d t d t b i c c P a P d c P d t d t a I c b P d c P d t d t b I c
30 29 opabbidv g = G a b | [˙Base g / p]˙ [˙ Itv g / i]˙ c p a p d c p d t d t a i c b p d c p d t d t b i c = a b | c P a P d c P d t d t a I c b P d c P d t d t b I c
31 10 30 mpteq12dv g = G d ran Line 𝒢 g a b | [˙Base g / p]˙ [˙ Itv g / i]˙ c p a p d c p d t d t a i c b p d c p d t d t b i c = d ran L a b | c P a P d c P d t d t a I c b P d c P d t d t b I c
32 df-hpg hp 𝒢 = g V d ran Line 𝒢 g a b | [˙Base g / p]˙ [˙ Itv g / i]˙ c p a p d c p d t d t a i c b p d c p d t d t b i c
33 3 fvexi L V
34 33 rnex ran L V
35 34 mptex d ran L a b | c P a P d c P d t d t a I c b P d c P d t d t b I c V
36 31 32 35 fvmpt G V hp 𝒢 G = d ran L a b | c P a P d c P d t d t a I c b P d c P d t d t b I c
37 5 7 36 3syl φ hp 𝒢 G = d ran L a b | c P a P d c P d t d t a I c b P d c P d t d t b I c
38 difeq2 d = D P d = P D
39 38 eleq2d d = D a P d a P D
40 38 eleq2d d = D c P d c P D
41 39 40 anbi12d d = D a P d c P d a P D c P D
42 rexeq d = D t d t a I c t D t a I c
43 41 42 anbi12d d = D a P d c P d t d t a I c a P D c P D t D t a I c
44 38 eleq2d d = D b P d b P D
45 44 40 anbi12d d = D b P d c P d b P D c P D
46 rexeq d = D t d t b I c t D t b I c
47 45 46 anbi12d d = D b P d c P d t d t b I c b P D c P D t D t b I c
48 43 47 anbi12d d = D a P d c P d t d t a I c b P d c P d t d t b I c a P D c P D t D t a I c b P D c P D t D t b I c
49 48 rexbidv d = D c P a P d c P d t d t a I c b P d c P d t d t b I c c P a P D c P D t D t a I c b P D c P D t D t b I c
50 49 opabbidv d = D a b | c P a P d c P d t d t a I c b P d c P d t d t b I c = a b | c P a P D c P D t D t a I c b P D c P D t D t b I c
51 50 adantl φ d = D a b | c P a P d c P d t d t a I c b P d c P d t d t b I c = a b | c P a P D c P D t D t a I c b P D c P D t D t b I c
52 df-xp P × P = a b | a P b P
53 1 fvexi P V
54 53 53 xpex P × P V
55 52 54 eqeltrri a b | a P b P V
56 eldifi a P D a P
57 eldifi b P D b P
58 56 57 anim12i a P D b P D a P b P
59 58 ad2ant2r a P D c P D b P D c P D a P b P
60 59 ad2ant2r a P D c P D t D t a I c b P D c P D t D t b I c a P b P
61 60 rexlimivw c P a P D c P D t D t a I c b P D c P D t D t b I c a P b P
62 61 ssopab2i a b | c P a P D c P D t D t a I c b P D c P D t D t b I c a b | a P b P
63 55 62 ssexi a b | c P a P D c P D t D t a I c b P D c P D t D t b I c V
64 63 a1i φ a b | c P a P D c P D t D t a I c b P D c P D t D t b I c V
65 37 51 6 64 fvmptd φ hp 𝒢 G D = a b | c P a P D c P D t D t a I c b P D c P D t D t b I c
66 vex a V
67 vex c V
68 eleq1w e = a e P D a P D
69 68 anbi1d e = a e P D f P D a P D f P D
70 oveq1 e = a e I f = a I f
71 70 eleq2d e = a t e I f t a I f
72 71 rexbidv e = a t D t e I f t D t a I f
73 69 72 anbi12d e = a e P D f P D t D t e I f a P D f P D t D t a I f
74 eleq1w f = c f P D c P D
75 74 anbi2d f = c a P D f P D a P D c P D
76 oveq2 f = c a I f = a I c
77 76 eleq2d f = c t a I f t a I c
78 77 rexbidv f = c t D t a I f t D t a I c
79 75 78 anbi12d f = c a P D f P D t D t a I f a P D c P D t D t a I c
80 simpl a = e b = f a = e
81 80 eleq1d a = e b = f a P D e P D
82 simpr a = e b = f b = f
83 82 eleq1d a = e b = f b P D f P D
84 81 83 anbi12d a = e b = f a P D b P D e P D f P D
85 oveq12 a = e b = f a I b = e I f
86 85 eleq2d a = e b = f t a I b t e I f
87 86 rexbidv a = e b = f t D t a I b t D t e I f
88 84 87 anbi12d a = e b = f a P D b P D t D t a I b e P D f P D t D t e I f
89 88 cbvopabv a b | a P D b P D t D t a I b = e f | e P D f P D t D t e I f
90 4 89 eqtri O = e f | e P D f P D t D t e I f
91 66 67 73 79 90 brab a O c a P D c P D t D t a I c
92 vex b V
93 eleq1w e = b e P D b P D
94 93 anbi1d e = b e P D f P D b P D f P D
95 oveq1 e = b e I f = b I f
96 95 eleq2d e = b t e I f t b I f
97 96 rexbidv e = b t D t e I f t D t b I f
98 94 97 anbi12d e = b e P D f P D t D t e I f b P D f P D t D t b I f
99 74 anbi2d f = c b P D f P D b P D c P D
100 oveq2 f = c b I f = b I c
101 100 eleq2d f = c t b I f t b I c
102 101 rexbidv f = c t D t b I f t D t b I c
103 99 102 anbi12d f = c b P D f P D t D t b I f b P D c P D t D t b I c
104 92 67 98 103 90 brab b O c b P D c P D t D t b I c
105 91 104 anbi12i a O c b O c a P D c P D t D t a I c b P D c P D t D t b I c
106 105 rexbii c P a O c b O c c P a P D c P D t D t a I c b P D c P D t D t b I c
107 106 opabbii a b | c P a O c b O c = a b | c P a P D c P D t D t a I c b P D c P D t D t b I c
108 65 107 eqtr4di φ hp 𝒢 G D = a b | c P a O c b O c