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 ⊢ 𝑃 = ( Base ‘ 𝐺 )
isperp.d ⊢ − = ( dist ‘ 𝐺 )
isperp.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
isperp.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
isperp.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
isperp.a ⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
ragperp.b ⊢ ( 𝜑 → 𝐵 ∈ ran 𝐿 )
ragperp.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 ∩ 𝐵 ) )
ragperp.u ⊢ ( 𝜑 → 𝑈 ∈ 𝐴 )
ragperp.v ⊢ ( 𝜑 → 𝑉 ∈ 𝐵 )
ragperp.1 ⊢ ( 𝜑 → 𝑈 ≠ 𝑋 )
ragperp.2 ⊢ ( 𝜑 → 𝑉 ≠ 𝑋 )
ragperp.r ⊢ ( 𝜑 → ⟨“ 𝑈 𝑋 𝑉 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
Assertion ragperp ( 𝜑 → 𝐴 ( ⟂G ‘ 𝐺 ) 𝐵 )

Proof

Step Hyp Ref Expression
1 isperp.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 isperp.d ⊢ − = ( dist ‘ 𝐺 )
3 isperp.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 isperp.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
5 isperp.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
6 isperp.a ⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
7 ragperp.b ⊢ ( 𝜑 → 𝐵 ∈ ran 𝐿 )
8 ragperp.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 ∩ 𝐵 ) )
9 ragperp.u ⊢ ( 𝜑 → 𝑈 ∈ 𝐴 )
10 ragperp.v ⊢ ( 𝜑 → 𝑉 ∈ 𝐵 )
11 ragperp.1 ⊢ ( 𝜑 → 𝑈 ≠ 𝑋 )
12 ragperp.2 ⊢ ( 𝜑 → 𝑉 ≠ 𝑋 )
13 ragperp.r ⊢ ( 𝜑 → ⟨“ 𝑈 𝑋 𝑉 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
14 eqid ⊢ ( pInvG ‘ 𝐺 ) = ( pInvG ‘ 𝐺 )
15 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ) → 𝐺 ∈ TarskiG )
16 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ) → 𝐵 ∈ ran 𝐿 )
17 simprr ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ) → 𝑣 ∈ 𝐵 )
18 1 4 3 15 16 17 tglnpt ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ) → 𝑣 ∈ 𝑃 )
19 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ) → 𝐴 ∈ ran 𝐿 )
20 8 elin1d ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
21 20 adantr ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ) → 𝑋 ∈ 𝐴 )
22 1 4 3 15 19 21 tglnpt ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ) → 𝑋 ∈ 𝑃 )
23 simprl ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ) → 𝑢 ∈ 𝐴 )
24 1 4 3 15 19 23 tglnpt ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ) → 𝑢 ∈ 𝑃 )
25 10 adantr ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ) → 𝑉 ∈ 𝐵 )
26 1 4 3 15 16 25 tglnpt ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ) → 𝑉 ∈ 𝑃 )
27 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ) → 𝑈 ∈ 𝐴 )
28 1 4 3 15 19 27 tglnpt ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ) → 𝑈 ∈ 𝑃 )
29 13 adantr ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ) → ⟨“ 𝑈 𝑋 𝑉 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
30 11 adantr ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ) → 𝑈 ≠ 𝑋 )
31 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ¬ 𝑋 = 𝑢 ) → 𝑈 ∈ 𝐴 )
32 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ¬ 𝑋 = 𝑢 ) → 𝐺 ∈ TarskiG )
33 22 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ¬ 𝑋 = 𝑢 ) → 𝑋 ∈ 𝑃 )
34 24 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ¬ 𝑋 = 𝑢 ) → 𝑢 ∈ 𝑃 )
35 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ¬ 𝑋 = 𝑢 ) → ¬ 𝑋 = 𝑢 )
36 35 neqned ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ¬ 𝑋 = 𝑢 ) → 𝑋 ≠ 𝑢 )
37 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ¬ 𝑋 = 𝑢 ) → 𝐴 ∈ ran 𝐿 )
38 20 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ¬ 𝑋 = 𝑢 ) → 𝑋 ∈ 𝐴 )
39 23 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ¬ 𝑋 = 𝑢 ) → 𝑢 ∈ 𝐴 )
40 1 3 4 32 33 34 36 36 37 38 39 tglinethru ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ¬ 𝑋 = 𝑢 ) → 𝐴 = ( 𝑋 𝐿 𝑢 ) )
41 31 40 eleqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ¬ 𝑋 = 𝑢 ) → 𝑈 ∈ ( 𝑋 𝐿 𝑢 ) )
42 41 ex ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ) → ( ¬ 𝑋 = 𝑢 → 𝑈 ∈ ( 𝑋 𝐿 𝑢 ) ) )
43 42 orrd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ) → ( 𝑋 = 𝑢 ∨ 𝑈 ∈ ( 𝑋 𝐿 𝑢 ) ) )
44 43 orcomd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ) → ( 𝑈 ∈ ( 𝑋 𝐿 𝑢 ) ∨ 𝑋 = 𝑢 ) )
45 1 2 3 4 14 15 28 22 26 24 29 30 44 ragcol ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ) → ⟨“ 𝑢 𝑋 𝑉 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
46 1 2 3 4 14 15 24 22 26 45 ragcom ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ) → ⟨“ 𝑉 𝑋 𝑢 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
47 12 adantr ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ) → 𝑉 ≠ 𝑋 )
48 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ¬ 𝑋 = 𝑣 ) → 𝑉 ∈ 𝐵 )
49 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ¬ 𝑋 = 𝑣 ) → 𝐺 ∈ TarskiG )
50 22 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ¬ 𝑋 = 𝑣 ) → 𝑋 ∈ 𝑃 )
51 18 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ¬ 𝑋 = 𝑣 ) → 𝑣 ∈ 𝑃 )
52 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ¬ 𝑋 = 𝑣 ) → ¬ 𝑋 = 𝑣 )
53 52 neqned ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ¬ 𝑋 = 𝑣 ) → 𝑋 ≠ 𝑣 )
54 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ¬ 𝑋 = 𝑣 ) → 𝐵 ∈ ran 𝐿 )
55 8 elin2d ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
56 55 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ¬ 𝑋 = 𝑣 ) → 𝑋 ∈ 𝐵 )
57 17 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ¬ 𝑋 = 𝑣 ) → 𝑣 ∈ 𝐵 )
58 1 3 4 49 50 51 53 53 54 56 57 tglinethru ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ¬ 𝑋 = 𝑣 ) → 𝐵 = ( 𝑋 𝐿 𝑣 ) )
59 48 58 eleqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ) ∧ ¬ 𝑋 = 𝑣 ) → 𝑉 ∈ ( 𝑋 𝐿 𝑣 ) )
60 59 ex ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ) → ( ¬ 𝑋 = 𝑣 → 𝑉 ∈ ( 𝑋 𝐿 𝑣 ) ) )
61 60 orrd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ) → ( 𝑋 = 𝑣 ∨ 𝑉 ∈ ( 𝑋 𝐿 𝑣 ) ) )
62 61 orcomd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ) → ( 𝑉 ∈ ( 𝑋 𝐿 𝑣 ) ∨ 𝑋 = 𝑣 ) )
63 1 2 3 4 14 15 26 22 24 18 46 47 62 ragcol ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ) → ⟨“ 𝑣 𝑋 𝑢 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
64 1 2 3 4 14 15 18 22 24 63 ragcom ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ) → ⟨“ 𝑢 𝑋 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
65 64 ralrimivva ⊢ ( 𝜑 → ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐵 ⟨“ 𝑢 𝑋 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
66 1 2 3 4 5 6 7 8 isperp2 ⊢ ( 𝜑 → ( 𝐴 ( ⟂G ‘ 𝐺 ) 𝐵 ↔ ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐵 ⟨“ 𝑢 𝑋 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) )
67 65 66 mpbird ⊢ ( 𝜑 → 𝐴 ( ⟂G ‘ 𝐺 ) 𝐵 )