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 ) )