Metamath Proof Explorer

Theorem oppperpex

Description: Restating colperpex using the "opposite side of a line" relation. (Contributed by Thierry Arnoux, 2-Aug-2020)

Ref Expression
Hypotheses hpg.p 
|- P = ( Base ` G )
hpg.d 
|- .- = ( dist ` G )
hpg.i 
|- I = ( Itv ` G )
hpg.o 
|- O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }
opphl.l 
|- L = ( LineG ` G )
opphl.d 
|- ( ph -> D e. ran L )
opphl.g 
|- ( ph -> G e. TarskiG )
opphl.k 
|- K = ( hlG ` G )
oppperpex.1 
|- ( ph -> A e. D )
oppperpex.2 
|- ( ph -> C e. P )
oppperpex.3 
|- ( ph -> -. C e. D )
oppperpex.4 
|- ( ph -> G TarskiGDim>= 2 )
Assertion oppperpex 
|- ( ph -> E. p e. P ( ( A L p ) ( perpG ` G ) D /\ C O p ) )

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 e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }
5 opphl.l 
 |-  L = ( LineG ` G )
6 opphl.d 
 |-  ( ph -> D e. ran L )
7 opphl.g 
 |-  ( ph -> G e. TarskiG )
8 opphl.k 
 |-  K = ( hlG ` G )
9 oppperpex.1 
 |-  ( ph -> A e. D )
10 oppperpex.2 
 |-  ( ph -> C e. P )
11 oppperpex.3 
 |-  ( ph -> -. C e. D )
12 oppperpex.4 
 |-  ( ph -> G TarskiGDim>= 2 )
13 simprrl 
 |-  ( ( ( ( ph /\ x e. D ) /\ A =/= x ) /\ ( p e. P /\ ( ( A L p ) ( perpG ` G ) ( A L x ) /\ E. t e. P ( ( t e. ( A L x ) \/ A = x ) /\ t e. ( C I p ) ) ) ) ) -> ( A L p ) ( perpG ` G ) ( A L x ) )
14 7 ad2antrr 
 |-  ( ( ( ph /\ x e. D ) /\ A =/= x ) -> G e. TarskiG )
15 6 ad2antrr 
 |-  ( ( ( ph /\ x e. D ) /\ A =/= x ) -> D e. ran L )
16 9 ad2antrr 
 |-  ( ( ( ph /\ x e. D ) /\ A =/= x ) -> A e. D )
17 1 5 3 14 15 16 tglnpt 
 |-  ( ( ( ph /\ x e. D ) /\ A =/= x ) -> A e. P )
18 simplr 
 |-  ( ( ( ph /\ x e. D ) /\ A =/= x ) -> x e. D )
19 1 5 3 14 15 18 tglnpt 
 |-  ( ( ( ph /\ x e. D ) /\ A =/= x ) -> x e. P )
20 simpr 
 |-  ( ( ( ph /\ x e. D ) /\ A =/= x ) -> A =/= x )
21 1 3 5 14 17 19 20 20 15 16 18 tglinethru 
 |-  ( ( ( ph /\ x e. D ) /\ A =/= x ) -> D = ( A L x ) )
22 21 adantr 
 |-  ( ( ( ( ph /\ x e. D ) /\ A =/= x ) /\ ( p e. P /\ ( ( A L p ) ( perpG ` G ) ( A L x ) /\ E. t e. P ( ( t e. ( A L x ) \/ A = x ) /\ t e. ( C I p ) ) ) ) ) -> D = ( A L x ) )
23 13 22 breqtrrd 
 |-  ( ( ( ( ph /\ x e. D ) /\ A =/= x ) /\ ( p e. P /\ ( ( A L p ) ( perpG ` G ) ( A L x ) /\ E. t e. P ( ( t e. ( A L x ) \/ A = x ) /\ t e. ( C I p ) ) ) ) ) -> ( A L p ) ( perpG ` G ) D )
24 11 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. D ) /\ A =/= x ) /\ ( p e. P /\ ( ( A L p ) ( perpG ` G ) ( A L x ) /\ E. t e. P ( ( t e. ( A L x ) \/ A = x ) /\ t e. ( C I p ) ) ) ) ) -> -. C e. D )
25 14 adantr 
 |-  ( ( ( ( ph /\ x e. D ) /\ A =/= x ) /\ ( p e. P /\ ( ( A L p ) ( perpG ` G ) ( A L x ) /\ E. t e. P ( ( t e. ( A L x ) \/ A = x ) /\ t e. ( C I p ) ) ) ) ) -> G e. TarskiG )
26 15 adantr 
 |-  ( ( ( ( ph /\ x e. D ) /\ A =/= x ) /\ ( p e. P /\ ( ( A L p ) ( perpG ` G ) ( A L x ) /\ E. t e. P ( ( t e. ( A L x ) \/ A = x ) /\ t e. ( C I p ) ) ) ) ) -> D e. ran L )
27 16 adantr 
 |-  ( ( ( ( ph /\ x e. D ) /\ A =/= x ) /\ ( p e. P /\ ( ( A L p ) ( perpG ` G ) ( A L x ) /\ E. t e. P ( ( t e. ( A L x ) \/ A = x ) /\ t e. ( C I p ) ) ) ) ) -> A e. D )
28 simprl 
 |-  ( ( ( ( ph /\ x e. D ) /\ A =/= x ) /\ ( p e. P /\ ( ( A L p ) ( perpG ` G ) ( A L x ) /\ E. t e. P ( ( t e. ( A L x ) \/ A = x ) /\ t e. ( C I p ) ) ) ) ) -> p e. P )
29 1 2 3 5 25 26 27 28 23 footne 
 |-  ( ( ( ( ph /\ x e. D ) /\ A =/= x ) /\ ( p e. P /\ ( ( A L p ) ( perpG ` G ) ( A L x ) /\ E. t e. P ( ( t e. ( A L x ) \/ A = x ) /\ t e. ( C I p ) ) ) ) ) -> -. p e. D )
30 20 ad3antrrr 
 |-  ( ( ( ( ( ( ph /\ x e. D ) /\ A =/= x ) /\ p e. P ) /\ ( A L p ) ( perpG ` G ) ( A L x ) ) /\ ( t e. P /\ ( ( t e. ( A L x ) \/ A = x ) /\ t e. ( C I p ) ) ) ) -> A =/= x )
31 30 neneqd 
 |-  ( ( ( ( ( ( ph /\ x e. D ) /\ A =/= x ) /\ p e. P ) /\ ( A L p ) ( perpG ` G ) ( A L x ) ) /\ ( t e. P /\ ( ( t e. ( A L x ) \/ A = x ) /\ t e. ( C I p ) ) ) ) -> -. A = x )
32 simprrl 
 |-  ( ( ( ( ( ( ph /\ x e. D ) /\ A =/= x ) /\ p e. P ) /\ ( A L p ) ( perpG ` G ) ( A L x ) ) /\ ( t e. P /\ ( ( t e. ( A L x ) \/ A = x ) /\ t e. ( C I p ) ) ) ) -> ( t e. ( A L x ) \/ A = x ) )
33 32 orcomd 
 |-  ( ( ( ( ( ( ph /\ x e. D ) /\ A =/= x ) /\ p e. P ) /\ ( A L p ) ( perpG ` G ) ( A L x ) ) /\ ( t e. P /\ ( ( t e. ( A L x ) \/ A = x ) /\ t e. ( C I p ) ) ) ) -> ( A = x \/ t e. ( A L x ) ) )
34 33 ord 
 |-  ( ( ( ( ( ( ph /\ x e. D ) /\ A =/= x ) /\ p e. P ) /\ ( A L p ) ( perpG ` G ) ( A L x ) ) /\ ( t e. P /\ ( ( t e. ( A L x ) \/ A = x ) /\ t e. ( C I p ) ) ) ) -> ( -. A = x -> t e. ( A L x ) ) )
35 31 34 mpd 
 |-  ( ( ( ( ( ( ph /\ x e. D ) /\ A =/= x ) /\ p e. P ) /\ ( A L p ) ( perpG ` G ) ( A L x ) ) /\ ( t e. P /\ ( ( t e. ( A L x ) \/ A = x ) /\ t e. ( C I p ) ) ) ) -> t e. ( A L x ) )
36 21 ad3antrrr 
 |-  ( ( ( ( ( ( ph /\ x e. D ) /\ A =/= x ) /\ p e. P ) /\ ( A L p ) ( perpG ` G ) ( A L x ) ) /\ ( t e. P /\ ( ( t e. ( A L x ) \/ A = x ) /\ t e. ( C I p ) ) ) ) -> D = ( A L x ) )
37 35 36 eleqtrrd 
 |-  ( ( ( ( ( ( ph /\ x e. D ) /\ A =/= x ) /\ p e. P ) /\ ( A L p ) ( perpG ` G ) ( A L x ) ) /\ ( t e. P /\ ( ( t e. ( A L x ) \/ A = x ) /\ t e. ( C I p ) ) ) ) -> t e. D )
38 simprrr 
 |-  ( ( ( ( ( ( ph /\ x e. D ) /\ A =/= x ) /\ p e. P ) /\ ( A L p ) ( perpG ` G ) ( A L x ) ) /\ ( t e. P /\ ( ( t e. ( A L x ) \/ A = x ) /\ t e. ( C I p ) ) ) ) -> t e. ( C I p ) )
39 37 38 jca 
 |-  ( ( ( ( ( ( ph /\ x e. D ) /\ A =/= x ) /\ p e. P ) /\ ( A L p ) ( perpG ` G ) ( A L x ) ) /\ ( t e. P /\ ( ( t e. ( A L x ) \/ A = x ) /\ t e. ( C I p ) ) ) ) -> ( t e. D /\ t e. ( C I p ) ) )
40 39 ex 
 |-  ( ( ( ( ( ph /\ x e. D ) /\ A =/= x ) /\ p e. P ) /\ ( A L p ) ( perpG ` G ) ( A L x ) ) -> ( ( t e. P /\ ( ( t e. ( A L x ) \/ A = x ) /\ t e. ( C I p ) ) ) -> ( t e. D /\ t e. ( C I p ) ) ) )
41 40 reximdv2 
 |-  ( ( ( ( ( ph /\ x e. D ) /\ A =/= x ) /\ p e. P ) /\ ( A L p ) ( perpG ` G ) ( A L x ) ) -> ( E. t e. P ( ( t e. ( A L x ) \/ A = x ) /\ t e. ( C I p ) ) -> E. t e. D t e. ( C I p ) ) )
42 41 impr 
 |-  ( ( ( ( ( ph /\ x e. D ) /\ A =/= x ) /\ p e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L x ) /\ E. t e. P ( ( t e. ( A L x ) \/ A = x ) /\ t e. ( C I p ) ) ) ) -> E. t e. D t e. ( C I p ) )
43 42 anasss 
 |-  ( ( ( ( ph /\ x e. D ) /\ A =/= x ) /\ ( p e. P /\ ( ( A L p ) ( perpG ` G ) ( A L x ) /\ E. t e. P ( ( t e. ( A L x ) \/ A = x ) /\ t e. ( C I p ) ) ) ) ) -> E. t e. D t e. ( C I p ) )
44 24 29 43 jca31 
 |-  ( ( ( ( ph /\ x e. D ) /\ A =/= x ) /\ ( p e. P /\ ( ( A L p ) ( perpG ` G ) ( A L x ) /\ E. t e. P ( ( t e. ( A L x ) \/ A = x ) /\ t e. ( C I p ) ) ) ) ) -> ( ( -. C e. D /\ -. p e. D ) /\ E. t e. D t e. ( C I p ) ) )
45 10 ad2antrr 
 |-  ( ( ( ph /\ x e. D ) /\ A =/= x ) -> C e. P )
46 45 ad2antrr 
 |-  ( ( ( ( ( ph /\ x e. D ) /\ A =/= x ) /\ p e. P ) /\ ( A L p ) ( perpG ` G ) ( A L x ) ) -> C e. P )
47 simplr 
 |-  ( ( ( ( ( ph /\ x e. D ) /\ A =/= x ) /\ p e. P ) /\ ( A L p ) ( perpG ` G ) ( A L x ) ) -> p e. P )
48 1 2 3 4 46 47 islnopp 
 |-  ( ( ( ( ( ph /\ x e. D ) /\ A =/= x ) /\ p e. P ) /\ ( A L p ) ( perpG ` G ) ( A L x ) ) -> ( C O p <-> ( ( -. C e. D /\ -. p e. D ) /\ E. t e. D t e. ( C I p ) ) ) )
49 48 adantrr 
 |-  ( ( ( ( ( ph /\ x e. D ) /\ A =/= x ) /\ p e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L x ) /\ E. t e. P ( ( t e. ( A L x ) \/ A = x ) /\ t e. ( C I p ) ) ) ) -> ( C O p <-> ( ( -. C e. D /\ -. p e. D ) /\ E. t e. D t e. ( C I p ) ) ) )
50 49 anasss 
 |-  ( ( ( ( ph /\ x e. D ) /\ A =/= x ) /\ ( p e. P /\ ( ( A L p ) ( perpG ` G ) ( A L x ) /\ E. t e. P ( ( t e. ( A L x ) \/ A = x ) /\ t e. ( C I p ) ) ) ) ) -> ( C O p <-> ( ( -. C e. D /\ -. p e. D ) /\ E. t e. D t e. ( C I p ) ) ) )
51 44 50 mpbird 
 |-  ( ( ( ( ph /\ x e. D ) /\ A =/= x ) /\ ( p e. P /\ ( ( A L p ) ( perpG ` G ) ( A L x ) /\ E. t e. P ( ( t e. ( A L x ) \/ A = x ) /\ t e. ( C I p ) ) ) ) ) -> C O p )
52 23 51 jca 
 |-  ( ( ( ( ph /\ x e. D ) /\ A =/= x ) /\ ( p e. P /\ ( ( A L p ) ( perpG ` G ) ( A L x ) /\ E. t e. P ( ( t e. ( A L x ) \/ A = x ) /\ t e. ( C I p ) ) ) ) ) -> ( ( A L p ) ( perpG ` G ) D /\ C O p ) )
53 12 ad2antrr 
 |-  ( ( ( ph /\ x e. D ) /\ A =/= x ) -> G TarskiGDim>= 2 )
54 1 2 3 5 14 17 19 45 20 53 colperpex 
 |-  ( ( ( ph /\ x e. D ) /\ A =/= x ) -> E. p e. P ( ( A L p ) ( perpG ` G ) ( A L x ) /\ E. t e. P ( ( t e. ( A L x ) \/ A = x ) /\ t e. ( C I p ) ) ) )
55 52 54 reximddv 
 |-  ( ( ( ph /\ x e. D ) /\ A =/= x ) -> E. p e. P ( ( A L p ) ( perpG ` G ) D /\ C O p ) )
56 1 3 5 7 6 9 tglnpt2 
 |-  ( ph -> E. x e. D A =/= x )
57 55 56 r19.29a 
 |-  ( ph -> E. p e. P ( ( A L p ) ( perpG ` G ) D /\ C O p ) )