Metamath Proof Explorer

Theorem perpdragALT

Description: Deduce a right angle from perpendicular lines. (Contributed by Thierry Arnoux, 12-Dec-2019) (New usage is discouraged.) (Proof modification is discouraged.)

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 perpdragALT 
|- ( 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 eqidd 
 |-  ( ( ph /\ A = B ) -> A = A )
11 simpr 
 |-  ( ( ph /\ A = B ) -> A = B )
12 eqidd 
 |-  ( ( ph /\ A = B ) -> C = C )
13 10 11 12 s3eqd 
 |-  ( ( ph /\ A = B ) -> <" A A C "> = <" A B C "> )
14 eqid 
 |-  ( pInvG ` G ) = ( pInvG ` G )
15 4 5 9 perpln1 
 |-  ( ph -> D e. ran L )
16 1 4 3 5 15 6 tglnpt 
 |-  ( ph -> A e. P )
17 1 2 3 4 14 5 8 16 8 ragtrivb 
 |-  ( ph -> <" C A A "> e. ( raG ` G ) )
18 1 2 3 4 14 5 8 16 16 17 ragcom 
 |-  ( ph -> <" A A C "> e. ( raG ` G ) )
19 18 adantr 
 |-  ( ( ph /\ A = B ) -> <" A A C "> e. ( raG ` G ) )
20 13 19 eqeltrrd 
 |-  ( ( ph /\ A = B ) -> <" A B C "> e. ( raG ` G ) )
21 5 adantr 
 |-  ( ( ph /\ A =/= B ) -> G e. TarskiG )
22 16 adantr 
 |-  ( ( ph /\ A =/= B ) -> A e. P )
23 1 4 3 5 15 7 tglnpt 
 |-  ( ph -> B e. P )
24 23 adantr 
 |-  ( ( ph /\ A =/= B ) -> B e. P )
25 7 adantr 
 |-  ( ( ph /\ A =/= B ) -> B e. D )
26 simpr 
 |-  ( ( ph /\ A =/= B ) -> A =/= B )
27 15 adantr 
 |-  ( ( ph /\ A =/= B ) -> D e. ran L )
28 6 adantr 
 |-  ( ( ph /\ A =/= B ) -> A e. D )
29 1 3 4 21 22 24 26 26 27 28 25 tglinethru 
 |-  ( ( ph /\ A =/= B ) -> D = ( A L B ) )
30 25 29 eleqtrd 
 |-  ( ( ph /\ A =/= B ) -> B e. ( A L B ) )
31 8 adantr 
 |-  ( ( ph /\ A =/= B ) -> C e. P )
32 9 adantr 
 |-  ( ( ph /\ A =/= B ) -> D ( perpG ` G ) ( B L C ) )
33 29 32 eqbrtrrd 
 |-  ( ( ph /\ A =/= B ) -> ( A L B ) ( perpG ` G ) ( B L C ) )
34 1 2 3 4 21 22 24 30 31 33 perprag 
 |-  ( ( ph /\ A =/= B ) -> <" A B C "> e. ( raG ` G ) )
35 20 34 pm2.61dane 
 |-  ( ph -> <" A B C "> e. ( raG ` G ) )