Metamath Proof Explorer

Theorem perprag

Description: Deduce a right angle from perpendicular lines. (Contributed by Thierry Arnoux, 10-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 )
perprag.1 
|- ( ph -> A e. P )
perprag.2 
|- ( ph -> B e. P )
perprag.3 
|- ( ph -> C e. ( A L B ) )
perprag.4 
|- ( ph -> D e. P )
perprag.5 
|- ( ph -> ( A L B ) ( perpG ` G ) ( C L D ) )
Assertion perprag 
|- ( ph -> <" A C D "> 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 perprag.1 
 |-  ( ph -> A e. P )
7 perprag.2 
 |-  ( ph -> B e. P )
8 perprag.3 
 |-  ( ph -> C e. ( A L B ) )
9 perprag.4 
 |-  ( ph -> D e. P )
10 perprag.5 
 |-  ( ph -> ( A L B ) ( perpG ` G ) ( C L D ) )
11 eqidd 
 |-  ( ( ph /\ C = D ) -> A = A )
12 simpr 
 |-  ( ( ph /\ C = D ) -> C = D )
13 eqidd 
 |-  ( ( ph /\ C = D ) -> D = D )
14 11 12 13 s3eqd 
 |-  ( ( ph /\ C = D ) -> <" A C D "> = <" A D D "> )
15 eqid 
 |-  ( pInvG ` G ) = ( pInvG ` G )
16 1 2 3 4 15 5 6 9 9 ragtrivb 
 |-  ( ph -> <" A D D "> e. ( raG ` G ) )
17 16 adantr 
 |-  ( ( ph /\ C = D ) -> <" A D D "> e. ( raG ` G ) )
18 14 17 eqeltrd 
 |-  ( ( ph /\ C = D ) -> <" A C D "> e. ( raG ` G ) )
19 5 adantr 
 |-  ( ( ph /\ C =/= D ) -> G e. TarskiG )
20 1 4 3 5 6 7 8 tglngne 
 |-  ( ph -> A =/= B )
21 1 3 4 5 6 7 20 tgelrnln 
 |-  ( ph -> ( A L B ) e. ran L )
22 21 adantr 
 |-  ( ( ph /\ C =/= D ) -> ( A L B ) e. ran L )
23 1 4 3 5 21 8 tglnpt 
 |-  ( ph -> C e. P )
24 23 adantr 
 |-  ( ( ph /\ C =/= D ) -> C e. P )
25 9 adantr 
 |-  ( ( ph /\ C =/= D ) -> D e. P )
26 simpr 
 |-  ( ( ph /\ C =/= D ) -> C =/= D )
27 1 3 4 19 24 25 26 tgelrnln 
 |-  ( ( ph /\ C =/= D ) -> ( C L D ) e. ran L )
28 8 adantr 
 |-  ( ( ph /\ C =/= D ) -> C e. ( A L B ) )
29 1 3 4 19 24 25 26 tglinerflx1 
 |-  ( ( ph /\ C =/= D ) -> C e. ( C L D ) )
30 28 29 elind 
 |-  ( ( ph /\ C =/= D ) -> C e. ( ( A L B ) i^i ( C L D ) ) )
31 1 3 4 5 6 7 20 tglinerflx1 
 |-  ( ph -> A e. ( A L B ) )
32 31 adantr 
 |-  ( ( ph /\ C =/= D ) -> A e. ( A L B ) )
33 1 3 4 19 24 25 26 tglinerflx2 
 |-  ( ( ph /\ C =/= D ) -> D e. ( C L D ) )
34 10 adantr 
 |-  ( ( ph /\ C =/= D ) -> ( A L B ) ( perpG ` G ) ( C L D ) )
35 1 2 3 4 19 22 27 30 32 33 34 isperp2d 
 |-  ( ( ph /\ C =/= D ) -> <" A C D "> e. ( raG ` G ) )
36 18 35 pm2.61dane 
 |-  ( ph -> <" A C D "> e. ( raG ` G ) )