Metamath Proof Explorer

Theorem colperpex

Description: In dimension 2 and above, on a line ( A L B ) there is always a perpendicular P from A on a given plane (here given by C , in case C does not lie on the line). Theorem 8.21 of Schwabhauser p. 63. (Contributed by Thierry Arnoux, 20-Nov-2019)

Ref Expression
Hypotheses colperpex.p 
|- P = ( Base ` G )
colperpex.d 
|- .- = ( dist ` G )
colperpex.i 
|- I = ( Itv ` G )
colperpex.l 
|- L = ( LineG ` G )
colperpex.g 
|- ( ph -> G e. TarskiG )
colperpex.1 
|- ( ph -> A e. P )
colperpex.2 
|- ( ph -> B e. P )
colperpex.3 
|- ( ph -> C e. P )
colperpex.4 
|- ( ph -> A =/= B )
colperpex.5 
|- ( ph -> G TarskiGDim>= 2 )
Assertion colperpex 
|- ( ph -> E. p e. P ( ( A L p ) ( perpG ` G ) ( A L B ) /\ E. t e. P ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( C I p ) ) ) )

Proof

Step Hyp Ref Expression
1 colperpex.p 
 |-  P = ( Base ` G )
2 colperpex.d 
 |-  .- = ( dist ` G )
3 colperpex.i 
 |-  I = ( Itv ` G )
4 colperpex.l 
 |-  L = ( LineG ` G )
5 colperpex.g 
 |-  ( ph -> G e. TarskiG )
6 colperpex.1 
 |-  ( ph -> A e. P )
7 colperpex.2 
 |-  ( ph -> B e. P )
8 colperpex.3 
 |-  ( ph -> C e. P )
9 colperpex.4 
 |-  ( ph -> A =/= B )
10 colperpex.5 
 |-  ( ph -> G TarskiGDim>= 2 )
11 5 ad3antrrr 
 |-  ( ( ( ( ph /\ C e. ( A L B ) ) /\ d e. P ) /\ -. d e. ( A L B ) ) -> G e. TarskiG )
12 6 ad3antrrr 
 |-  ( ( ( ( ph /\ C e. ( A L B ) ) /\ d e. P ) /\ -. d e. ( A L B ) ) -> A e. P )
13 7 ad3antrrr 
 |-  ( ( ( ( ph /\ C e. ( A L B ) ) /\ d e. P ) /\ -. d e. ( A L B ) ) -> B e. P )
14 simplr 
 |-  ( ( ( ( ph /\ C e. ( A L B ) ) /\ d e. P ) /\ -. d e. ( A L B ) ) -> d e. P )
15 9 ad3antrrr 
 |-  ( ( ( ( ph /\ C e. ( A L B ) ) /\ d e. P ) /\ -. d e. ( A L B ) ) -> A =/= B )
16 simpr 
 |-  ( ( ( ( ph /\ C e. ( A L B ) ) /\ d e. P ) /\ -. d e. ( A L B ) ) -> -. d e. ( A L B ) )
17 1 2 3 4 11 12 13 14 15 16 colperpexlem3 
 |-  ( ( ( ( ph /\ C e. ( A L B ) ) /\ d e. P ) /\ -. d e. ( A L B ) ) -> E. p e. P ( ( A L p ) ( perpG ` G ) ( A L B ) /\ E. s e. P ( ( s e. ( A L B ) \/ A = B ) /\ s e. ( d I p ) ) ) )
18 simprl 
 |-  ( ( ( ( ( ( ph /\ C e. ( A L B ) ) /\ d e. P ) /\ -. d e. ( A L B ) ) /\ p e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ E. s e. P ( ( s e. ( A L B ) \/ A = B ) /\ s e. ( d I p ) ) ) ) -> ( A L p ) ( perpG ` G ) ( A L B ) )
19 8 ad5antr 
 |-  ( ( ( ( ( ( ph /\ C e. ( A L B ) ) /\ d e. P ) /\ -. d e. ( A L B ) ) /\ p e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ E. s e. P ( ( s e. ( A L B ) \/ A = B ) /\ s e. ( d I p ) ) ) ) -> C e. P )
20 simp-5r 
 |-  ( ( ( ( ( ( ph /\ C e. ( A L B ) ) /\ d e. P ) /\ -. d e. ( A L B ) ) /\ p e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ E. s e. P ( ( s e. ( A L B ) \/ A = B ) /\ s e. ( d I p ) ) ) ) -> C e. ( A L B ) )
21 20 orcd 
 |-  ( ( ( ( ( ( ph /\ C e. ( A L B ) ) /\ d e. P ) /\ -. d e. ( A L B ) ) /\ p e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ E. s e. P ( ( s e. ( A L B ) \/ A = B ) /\ s e. ( d I p ) ) ) ) -> ( C e. ( A L B ) \/ A = B ) )
22 5 ad5antr 
 |-  ( ( ( ( ( ( ph /\ C e. ( A L B ) ) /\ d e. P ) /\ -. d e. ( A L B ) ) /\ p e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ E. s e. P ( ( s e. ( A L B ) \/ A = B ) /\ s e. ( d I p ) ) ) ) -> G e. TarskiG )
23 simplr 
 |-  ( ( ( ( ( ( ph /\ C e. ( A L B ) ) /\ d e. P ) /\ -. d e. ( A L B ) ) /\ p e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ E. s e. P ( ( s e. ( A L B ) \/ A = B ) /\ s e. ( d I p ) ) ) ) -> p e. P )
24 1 2 3 22 19 23 tgbtwntriv1 
 |-  ( ( ( ( ( ( ph /\ C e. ( A L B ) ) /\ d e. P ) /\ -. d e. ( A L B ) ) /\ p e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ E. s e. P ( ( s e. ( A L B ) \/ A = B ) /\ s e. ( d I p ) ) ) ) -> C e. ( C I p ) )
25 eleq1 
 |-  ( t = C -> ( t e. ( A L B ) <-> C e. ( A L B ) ) )
26 25 orbi1d 
 |-  ( t = C -> ( ( t e. ( A L B ) \/ A = B ) <-> ( C e. ( A L B ) \/ A = B ) ) )
27 eleq1 
 |-  ( t = C -> ( t e. ( C I p ) <-> C e. ( C I p ) ) )
28 26 27 anbi12d 
 |-  ( t = C -> ( ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( C I p ) ) <-> ( ( C e. ( A L B ) \/ A = B ) /\ C e. ( C I p ) ) ) )
29 28 rspcev 
 |-  ( ( C e. P /\ ( ( C e. ( A L B ) \/ A = B ) /\ C e. ( C I p ) ) ) -> E. t e. P ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( C I p ) ) )
30 19 21 24 29 syl12anc 
 |-  ( ( ( ( ( ( ph /\ C e. ( A L B ) ) /\ d e. P ) /\ -. d e. ( A L B ) ) /\ p e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ E. s e. P ( ( s e. ( A L B ) \/ A = B ) /\ s e. ( d I p ) ) ) ) -> E. t e. P ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( C I p ) ) )
31 18 30 jca 
 |-  ( ( ( ( ( ( ph /\ C e. ( A L B ) ) /\ d e. P ) /\ -. d e. ( A L B ) ) /\ p e. P ) /\ ( ( A L p ) ( perpG ` G ) ( A L B ) /\ E. s e. P ( ( s e. ( A L B ) \/ A = B ) /\ s e. ( d I p ) ) ) ) -> ( ( A L p ) ( perpG ` G ) ( A L B ) /\ E. t e. P ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( C I p ) ) ) )
32 31 ex 
 |-  ( ( ( ( ( ph /\ C e. ( A L B ) ) /\ d e. P ) /\ -. d e. ( A L B ) ) /\ p e. P ) -> ( ( ( A L p ) ( perpG ` G ) ( A L B ) /\ E. s e. P ( ( s e. ( A L B ) \/ A = B ) /\ s e. ( d I p ) ) ) -> ( ( A L p ) ( perpG ` G ) ( A L B ) /\ E. t e. P ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( C I p ) ) ) ) )
33 32 reximdva 
 |-  ( ( ( ( ph /\ C e. ( A L B ) ) /\ d e. P ) /\ -. d e. ( A L B ) ) -> ( E. p e. P ( ( A L p ) ( perpG ` G ) ( A L B ) /\ E. s e. P ( ( s e. ( A L B ) \/ A = B ) /\ s e. ( d I p ) ) ) -> E. p e. P ( ( A L p ) ( perpG ` G ) ( A L B ) /\ E. t e. P ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( C I p ) ) ) ) )
34 17 33 mpd 
 |-  ( ( ( ( ph /\ C e. ( A L B ) ) /\ d e. P ) /\ -. d e. ( A L B ) ) -> E. p e. P ( ( A L p ) ( perpG ` G ) ( A L B ) /\ E. t e. P ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( C I p ) ) ) )
35 5 adantr 
 |-  ( ( ph /\ C e. ( A L B ) ) -> G e. TarskiG )
36 10 adantr 
 |-  ( ( ph /\ C e. ( A L B ) ) -> G TarskiGDim>= 2 )
37 6 adantr 
 |-  ( ( ph /\ C e. ( A L B ) ) -> A e. P )
38 7 adantr 
 |-  ( ( ph /\ C e. ( A L B ) ) -> B e. P )
39 9 adantr 
 |-  ( ( ph /\ C e. ( A L B ) ) -> A =/= B )
40 1 3 4 35 36 37 38 39 tglowdim2ln 
 |-  ( ( ph /\ C e. ( A L B ) ) -> E. d e. P -. d e. ( A L B ) )
41 34 40 r19.29a 
 |-  ( ( ph /\ C e. ( A L B ) ) -> E. p e. P ( ( A L p ) ( perpG ` G ) ( A L B ) /\ E. t e. P ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( C I p ) ) ) )
42 5 adantr 
 |-  ( ( ph /\ -. C e. ( A L B ) ) -> G e. TarskiG )
43 6 adantr 
 |-  ( ( ph /\ -. C e. ( A L B ) ) -> A e. P )
44 7 adantr 
 |-  ( ( ph /\ -. C e. ( A L B ) ) -> B e. P )
45 8 adantr 
 |-  ( ( ph /\ -. C e. ( A L B ) ) -> C e. P )
46 9 adantr 
 |-  ( ( ph /\ -. C e. ( A L B ) ) -> A =/= B )
47 simpr 
 |-  ( ( ph /\ -. C e. ( A L B ) ) -> -. C e. ( A L B ) )
48 1 2 3 4 42 43 44 45 46 47 colperpexlem3 
 |-  ( ( ph /\ -. C e. ( A L B ) ) -> E. p e. P ( ( A L p ) ( perpG ` G ) ( A L B ) /\ E. t e. P ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( C I p ) ) ) )
49 41 48 pm2.61dan 
 |-  ( ph -> E. p e. P ( ( A L p ) ( perpG ` G ) ( A L B ) /\ E. t e. P ( ( t e. ( A L B ) \/ A = B ) /\ t e. ( C I p ) ) ) )