Metamath Proof Explorer

Theorem ragperp

Description: Deduce that two lines are perpendicular from a right angle statement. One direction of theorem 8.13 of Schwabhauser p. 59. (Contributed by Thierry Arnoux, 20-Oct-2019)

Ref Expression
Hypotheses isperp.p 
|- P = ( Base ` G )
isperp.d 
|- .- = ( dist ` G )
isperp.i 
|- I = ( Itv ` G )
isperp.l 
|- L = ( LineG ` G )
isperp.g 
|- ( ph -> G e. TarskiG )
isperp.a 
|- ( ph -> A e. ran L )
ragperp.b 
|- ( ph -> B e. ran L )
ragperp.x 
|- ( ph -> X e. ( A i^i B ) )
ragperp.u 
|- ( ph -> U e. A )
ragperp.v 
|- ( ph -> V e. B )
ragperp.1 
|- ( ph -> U =/= X )
ragperp.2 
|- ( ph -> V =/= X )
ragperp.r 
|- ( ph -> <" U X V "> e. ( raG ` G ) )
Assertion ragperp 
|- ( ph -> A ( perpG ` G ) B )

Proof

Step Hyp Ref Expression
1 isperp.p 
 |-  P = ( Base ` G )
2 isperp.d 
 |-  .- = ( dist ` G )
3 isperp.i 
 |-  I = ( Itv ` G )
4 isperp.l 
 |-  L = ( LineG ` G )
5 isperp.g 
 |-  ( ph -> G e. TarskiG )
6 isperp.a 
 |-  ( ph -> A e. ran L )
7 ragperp.b 
 |-  ( ph -> B e. ran L )
8 ragperp.x 
 |-  ( ph -> X e. ( A i^i B ) )
9 ragperp.u 
 |-  ( ph -> U e. A )
10 ragperp.v 
 |-  ( ph -> V e. B )
11 ragperp.1 
 |-  ( ph -> U =/= X )
12 ragperp.2 
 |-  ( ph -> V =/= X )
13 ragperp.r 
 |-  ( ph -> <" U X V "> e. ( raG ` G ) )
14 eqid 
 |-  ( pInvG ` G ) = ( pInvG ` G )
15 5 adantr 
 |-  ( ( ph /\ ( u e. A /\ v e. B ) ) -> G e. TarskiG )
16 7 adantr 
 |-  ( ( ph /\ ( u e. A /\ v e. B ) ) -> B e. ran L )
17 simprr 
 |-  ( ( ph /\ ( u e. A /\ v e. B ) ) -> v e. B )
18 1 4 3 15 16 17 tglnpt 
 |-  ( ( ph /\ ( u e. A /\ v e. B ) ) -> v e. P )
19 6 adantr 
 |-  ( ( ph /\ ( u e. A /\ v e. B ) ) -> A e. ran L )
20 8 elin1d 
 |-  ( ph -> X e. A )
21 20 adantr 
 |-  ( ( ph /\ ( u e. A /\ v e. B ) ) -> X e. A )
22 1 4 3 15 19 21 tglnpt 
 |-  ( ( ph /\ ( u e. A /\ v e. B ) ) -> X e. P )
23 simprl 
 |-  ( ( ph /\ ( u e. A /\ v e. B ) ) -> u e. A )
24 1 4 3 15 19 23 tglnpt 
 |-  ( ( ph /\ ( u e. A /\ v e. B ) ) -> u e. P )
25 10 adantr 
 |-  ( ( ph /\ ( u e. A /\ v e. B ) ) -> V e. B )
26 1 4 3 15 16 25 tglnpt 
 |-  ( ( ph /\ ( u e. A /\ v e. B ) ) -> V e. P )
27 9 adantr 
 |-  ( ( ph /\ ( u e. A /\ v e. B ) ) -> U e. A )
28 1 4 3 15 19 27 tglnpt 
 |-  ( ( ph /\ ( u e. A /\ v e. B ) ) -> U e. P )
29 13 adantr 
 |-  ( ( ph /\ ( u e. A /\ v e. B ) ) -> <" U X V "> e. ( raG ` G ) )
30 11 adantr 
 |-  ( ( ph /\ ( u e. A /\ v e. B ) ) -> U =/= X )
31 9 ad2antrr 
 |-  ( ( ( ph /\ ( u e. A /\ v e. B ) ) /\ -. X = u ) -> U e. A )
32 5 ad2antrr 
 |-  ( ( ( ph /\ ( u e. A /\ v e. B ) ) /\ -. X = u ) -> G e. TarskiG )
33 22 adantr 
 |-  ( ( ( ph /\ ( u e. A /\ v e. B ) ) /\ -. X = u ) -> X e. P )
34 24 adantr 
 |-  ( ( ( ph /\ ( u e. A /\ v e. B ) ) /\ -. X = u ) -> u e. P )
35 simpr 
 |-  ( ( ( ph /\ ( u e. A /\ v e. B ) ) /\ -. X = u ) -> -. X = u )
36 35 neqned 
 |-  ( ( ( ph /\ ( u e. A /\ v e. B ) ) /\ -. X = u ) -> X =/= u )
37 6 ad2antrr 
 |-  ( ( ( ph /\ ( u e. A /\ v e. B ) ) /\ -. X = u ) -> A e. ran L )
38 20 ad2antrr 
 |-  ( ( ( ph /\ ( u e. A /\ v e. B ) ) /\ -. X = u ) -> X e. A )
39 23 adantr 
 |-  ( ( ( ph /\ ( u e. A /\ v e. B ) ) /\ -. X = u ) -> u e. A )
40 1 3 4 32 33 34 36 36 37 38 39 tglinethru 
 |-  ( ( ( ph /\ ( u e. A /\ v e. B ) ) /\ -. X = u ) -> A = ( X L u ) )
41 31 40 eleqtrd 
 |-  ( ( ( ph /\ ( u e. A /\ v e. B ) ) /\ -. X = u ) -> U e. ( X L u ) )
42 41 ex 
 |-  ( ( ph /\ ( u e. A /\ v e. B ) ) -> ( -. X = u -> U e. ( X L u ) ) )
43 42 orrd 
 |-  ( ( ph /\ ( u e. A /\ v e. B ) ) -> ( X = u \/ U e. ( X L u ) ) )
44 43 orcomd 
 |-  ( ( ph /\ ( u e. A /\ v e. B ) ) -> ( U e. ( X L u ) \/ X = u ) )
45 1 2 3 4 14 15 28 22 26 24 29 30 44 ragcol 
 |-  ( ( ph /\ ( u e. A /\ v e. B ) ) -> <" u X V "> e. ( raG ` G ) )
46 1 2 3 4 14 15 24 22 26 45 ragcom 
 |-  ( ( ph /\ ( u e. A /\ v e. B ) ) -> <" V X u "> e. ( raG ` G ) )
47 12 adantr 
 |-  ( ( ph /\ ( u e. A /\ v e. B ) ) -> V =/= X )
48 10 ad2antrr 
 |-  ( ( ( ph /\ ( u e. A /\ v e. B ) ) /\ -. X = v ) -> V e. B )
49 5 ad2antrr 
 |-  ( ( ( ph /\ ( u e. A /\ v e. B ) ) /\ -. X = v ) -> G e. TarskiG )
50 22 adantr 
 |-  ( ( ( ph /\ ( u e. A /\ v e. B ) ) /\ -. X = v ) -> X e. P )
51 18 adantr 
 |-  ( ( ( ph /\ ( u e. A /\ v e. B ) ) /\ -. X = v ) -> v e. P )
52 simpr 
 |-  ( ( ( ph /\ ( u e. A /\ v e. B ) ) /\ -. X = v ) -> -. X = v )
53 52 neqned 
 |-  ( ( ( ph /\ ( u e. A /\ v e. B ) ) /\ -. X = v ) -> X =/= v )
54 7 ad2antrr 
 |-  ( ( ( ph /\ ( u e. A /\ v e. B ) ) /\ -. X = v ) -> B e. ran L )
55 8 elin2d 
 |-  ( ph -> X e. B )
56 55 ad2antrr 
 |-  ( ( ( ph /\ ( u e. A /\ v e. B ) ) /\ -. X = v ) -> X e. B )
57 17 adantr 
 |-  ( ( ( ph /\ ( u e. A /\ v e. B ) ) /\ -. X = v ) -> v e. B )
58 1 3 4 49 50 51 53 53 54 56 57 tglinethru 
 |-  ( ( ( ph /\ ( u e. A /\ v e. B ) ) /\ -. X = v ) -> B = ( X L v ) )
59 48 58 eleqtrd 
 |-  ( ( ( ph /\ ( u e. A /\ v e. B ) ) /\ -. X = v ) -> V e. ( X L v ) )
60 59 ex 
 |-  ( ( ph /\ ( u e. A /\ v e. B ) ) -> ( -. X = v -> V e. ( X L v ) ) )
61 60 orrd 
 |-  ( ( ph /\ ( u e. A /\ v e. B ) ) -> ( X = v \/ V e. ( X L v ) ) )
62 61 orcomd 
 |-  ( ( ph /\ ( u e. A /\ v e. B ) ) -> ( V e. ( X L v ) \/ X = v ) )
63 1 2 3 4 14 15 26 22 24 18 46 47 62 ragcol 
 |-  ( ( ph /\ ( u e. A /\ v e. B ) ) -> <" v X u "> e. ( raG ` G ) )
64 1 2 3 4 14 15 18 22 24 63 ragcom 
 |-  ( ( ph /\ ( u e. A /\ v e. B ) ) -> <" u X v "> e. ( raG ` G ) )
65 64 ralrimivva 
 |-  ( ph -> A. u e. A A. v e. B <" u X v "> e. ( raG ` G ) )
66 1 2 3 4 5 6 7 8 isperp2 
 |-  ( ph -> ( A ( perpG ` G ) B <-> A. u e. A A. v e. B <" u X v "> e. ( raG ` G ) ) )
67 65 66 mpbird 
 |-  ( ph -> A ( perpG ` G ) B )