Metamath Proof Explorer

Theorem isperp2

Description: Property for 2 lines A, B, intersecting at a point X to be perpendicular. Item (i) of definition 8.13 of Schwabhauser p. 59. (Contributed by Thierry Arnoux, 16-Oct-2019)

Ref Expression
Hypotheses isperp.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
isperp.d ⊢ − = ( dist ‘ 𝐺 )
isperp.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
isperp.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
isperp.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
isperp.a ⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
isperp2.b ⊢ ( 𝜑 → 𝐵 ∈ ran 𝐿 )
isperp2.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 ∩ 𝐵 ) )
Assertion isperp2 ( 𝜑 → ( 𝐴 ( ⟂G ‘ 𝐺 ) 𝐵 ↔ ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐵 ⟨“ 𝑢 𝑋 𝑣 ”⟩ ∈ ( ∟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 isperp2.b ⊢ ( 𝜑 → 𝐵 ∈ ran 𝐿 )
8 isperp2.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 ∩ 𝐵 ) )
9 eqidd ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ( ⟂G ‘ 𝐺 ) 𝐵 ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑣 ∈ 𝐵 ) → 𝑢 = 𝑢 )
10 5 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ( ⟂G ‘ 𝐺 ) 𝐵 ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑣 ∈ 𝐵 ) → 𝐺 ∈ TarskiG )
11 6 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ( ⟂G ‘ 𝐺 ) 𝐵 ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑣 ∈ 𝐵 ) → 𝐴 ∈ ran 𝐿 )
12 7 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ( ⟂G ‘ 𝐺 ) 𝐵 ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑣 ∈ 𝐵 ) → 𝐵 ∈ ran 𝐿 )
13 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ( ⟂G ‘ 𝐺 ) 𝐵 ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑣 ∈ 𝐵 ) → 𝐴 ( ⟂G ‘ 𝐺 ) 𝐵 )
14 1 2 3 4 10 11 12 13 perpneq ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ( ⟂G ‘ 𝐺 ) 𝐵 ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑣 ∈ 𝐵 ) → 𝐴 ≠ 𝐵 )
15 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ( ⟂G ‘ 𝐺 ) 𝐵 ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑣 ∈ 𝐵 ) → 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) )
16 8 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ( ⟂G ‘ 𝐺 ) 𝐵 ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑣 ∈ 𝐵 ) → 𝑋 ∈ ( 𝐴 ∩ 𝐵 ) )
17 1 3 4 10 11 12 14 15 16 tglineineq ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ( ⟂G ‘ 𝐺 ) 𝐵 ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑣 ∈ 𝐵 ) → 𝑥 = 𝑋 )
18 eqidd ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ( ⟂G ‘ 𝐺 ) 𝐵 ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑣 ∈ 𝐵 ) → 𝑣 = 𝑣 )
19 9 17 18 s3eqd ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ( ⟂G ‘ 𝐺 ) 𝐵 ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑣 ∈ 𝐵 ) → ⟨“ 𝑢 𝑥 𝑣 ”⟩ = ⟨“ 𝑢 𝑋 𝑣 ”⟩ )
20 19 eleq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ( ⟂G ‘ 𝐺 ) 𝐵 ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑣 ∈ 𝐵 ) → ( ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ↔ ⟨“ 𝑢 𝑋 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) )
21 20 biimpd ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ( ⟂G ‘ 𝐺 ) 𝐵 ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑣 ∈ 𝐵 ) → ( ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) → ⟨“ 𝑢 𝑋 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) )
22 21 ralimdva ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ( ⟂G ‘ 𝐺 ) 𝐵 ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑢 ∈ 𝐴 ) → ( ∀ 𝑣 ∈ 𝐵 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) → ∀ 𝑣 ∈ 𝐵 ⟨“ 𝑢 𝑋 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) )
23 22 ralimdva ⊢ ( ( ( 𝜑 ∧ 𝐴 ( ⟂G ‘ 𝐺 ) 𝐵 ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) → ( ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐵 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) → ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐵 ⟨“ 𝑢 𝑋 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) )
24 23 imp ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ( ⟂G ‘ 𝐺 ) 𝐵 ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐵 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) → ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐵 ⟨“ 𝑢 𝑋 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
25 1 2 3 4 5 6 7 isperp ⊢ ( 𝜑 → ( 𝐴 ( ⟂G ‘ 𝐺 ) 𝐵 ↔ ∃ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐵 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) )
26 25 biimpa ⊢ ( ( 𝜑 ∧ 𝐴 ( ⟂G ‘ 𝐺 ) 𝐵 ) → ∃ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐵 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
27 24 26 r19.29a ⊢ ( ( 𝜑 ∧ 𝐴 ( ⟂G ‘ 𝐺 ) 𝐵 ) → ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐵 ⟨“ 𝑢 𝑋 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
28 s3eq2 ⊢ ( 𝑥 = 𝑋 → ⟨“ 𝑢 𝑥 𝑣 ”⟩ = ⟨“ 𝑢 𝑋 𝑣 ”⟩ )
29 28 eleq1d ⊢ ( 𝑥 = 𝑋 → ( ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ↔ ⟨“ 𝑢 𝑋 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) )
30 29 2ralbidv ⊢ ( 𝑥 = 𝑋 → ( ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐵 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ↔ ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐵 ⟨“ 𝑢 𝑋 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) )
31 30 rspcev ⊢ ( ( 𝑋 ∈ ( 𝐴 ∩ 𝐵 ) ∧ ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐵 ⟨“ 𝑢 𝑋 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) → ∃ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐵 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
32 8 31 sylan ⊢ ( ( 𝜑 ∧ ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐵 ⟨“ 𝑢 𝑋 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) → ∃ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐵 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
33 25 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐵 ⟨“ 𝑢 𝑋 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) → ( 𝐴 ( ⟂G ‘ 𝐺 ) 𝐵 ↔ ∃ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐵 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) )
34 32 33 mpbird ⊢ ( ( 𝜑 ∧ ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐵 ⟨“ 𝑢 𝑋 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) → 𝐴 ( ⟂G ‘ 𝐺 ) 𝐵 )
35 27 34 impbida ⊢ ( 𝜑 → ( 𝐴 ( ⟂G ‘ 𝐺 ) 𝐵 ↔ ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐵 ⟨“ 𝑢 𝑋 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) )