Metamath Proof Explorer

Theorem perpdrag

Description: Deduce a right angle from perpendicular lines. (Contributed by Thierry Arnoux, 12-Dec-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 )
perpdrag.1 
|- ( ph -> A e. D )
perpdrag.2 
|- ( ph -> B e. D )
perpdrag.3 
|- ( ph -> C e. P )
perpdrag.4 
|- ( ph -> D ( perpG ` G ) ( B L C ) )
Assertion perpdrag 
|- ( ph -> <" A B C "> e. ( raG ` G ) )

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 perpdrag.1 
 |-  ( ph -> A e. D )
7 perpdrag.2 
 |-  ( ph -> B e. D )
8 perpdrag.3 
 |-  ( ph -> C e. P )
9 perpdrag.4 
 |-  ( ph -> D ( perpG ` G ) ( B L C ) )
10 5 ad2antrr 
 |-  ( ( ( ph /\ x e. D ) /\ A =/= x ) -> G e. TarskiG )
11 9 ad2antrr 
 |-  ( ( ( ph /\ x e. D ) /\ A =/= x ) -> D ( perpG ` G ) ( B L C ) )
12 4 10 11 perpln1 
 |-  ( ( ( ph /\ x e. D ) /\ A =/= x ) -> D e. ran L )
13 6 ad2antrr 
 |-  ( ( ( ph /\ x e. D ) /\ A =/= x ) -> A e. D )
14 1 4 3 10 12 13 tglnpt 
 |-  ( ( ( ph /\ x e. D ) /\ A =/= x ) -> A e. P )
15 simplr 
 |-  ( ( ( ph /\ x e. D ) /\ A =/= x ) -> x e. D )
16 1 4 3 10 12 15 tglnpt 
 |-  ( ( ( ph /\ x e. D ) /\ A =/= x ) -> x e. P )
17 7 ad2antrr 
 |-  ( ( ( ph /\ x e. D ) /\ A =/= x ) -> B e. D )
18 simpr 
 |-  ( ( ( ph /\ x e. D ) /\ A =/= x ) -> A =/= x )
19 1 3 4 10 14 16 18 18 12 13 15 tglinethru 
 |-  ( ( ( ph /\ x e. D ) /\ A =/= x ) -> D = ( A L x ) )
20 17 19 eleqtrd 
 |-  ( ( ( ph /\ x e. D ) /\ A =/= x ) -> B e. ( A L x ) )
21 8 ad2antrr 
 |-  ( ( ( ph /\ x e. D ) /\ A =/= x ) -> C e. P )
22 19 11 eqbrtrrd 
 |-  ( ( ( ph /\ x e. D ) /\ A =/= x ) -> ( A L x ) ( perpG ` G ) ( B L C ) )
23 1 2 3 4 10 14 16 20 21 22 perprag 
 |-  ( ( ( ph /\ x e. D ) /\ A =/= x ) -> <" A B C "> e. ( raG ` G ) )
24 4 5 9 perpln1 
 |-  ( ph -> D e. ran L )
25 1 3 4 5 24 6 tglnpt2 
 |-  ( ph -> E. x e. D A =/= x )
26 23 25 r19.29a 
 |-  ( ph -> <" A B C "> e. ( raG ` G ) )