Metamath Proof Explorer

Theorem isperp

Description: Property for 2 lines A, B to be perpendicular. Item (ii) of definition 8.11 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 𝐿 )
isperp.b ⊢ ( 𝜑 → 𝐵 ∈ ran 𝐿 )
Assertion isperp ( 𝜑 → ( 𝐴 ( ⟂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 isperp.b ⊢ ( 𝜑 → 𝐵 ∈ ran 𝐿 )
8 df-br ⊢ ( 𝐴 ( ⟂G ‘ 𝐺 ) 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ⟂G ‘ 𝐺 ) )
9 df-perpg ⊢ ⟂G = ( 𝑔 ∈ V ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ran ( LineG ‘ 𝑔 ) ∧ 𝑏 ∈ ran ( LineG ‘ 𝑔 ) ) ∧ ∃ 𝑥 ∈ ( 𝑎 ∩ 𝑏 ) ∀ 𝑢 ∈ 𝑎 ∀ 𝑣 ∈ 𝑏 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝑔 ) ) } )
10 simpr ⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → 𝑔 = 𝐺 )
11 10 fveq2d ⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → ( LineG ‘ 𝑔 ) = ( LineG ‘ 𝐺 ) )
12 11 4 eqtr4di ⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → ( LineG ‘ 𝑔 ) = 𝐿 )
13 12 rneqd ⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → ran ( LineG ‘ 𝑔 ) = ran 𝐿 )
14 13 eleq2d ⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → ( 𝑎 ∈ ran ( LineG ‘ 𝑔 ) ↔ 𝑎 ∈ ran 𝐿 ) )
15 13 eleq2d ⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → ( 𝑏 ∈ ran ( LineG ‘ 𝑔 ) ↔ 𝑏 ∈ ran 𝐿 ) )
16 14 15 anbi12d ⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → ( ( 𝑎 ∈ ran ( LineG ‘ 𝑔 ) ∧ 𝑏 ∈ ran ( LineG ‘ 𝑔 ) ) ↔ ( 𝑎 ∈ ran 𝐿 ∧ 𝑏 ∈ ran 𝐿 ) ) )
17 10 fveq2d ⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → ( ∟G ‘ 𝑔 ) = ( ∟G ‘ 𝐺 ) )
18 17 eleq2d ⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → ( ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝑔 ) ↔ ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) )
19 18 ralbidv ⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → ( ∀ 𝑣 ∈ 𝑏 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝑔 ) ↔ ∀ 𝑣 ∈ 𝑏 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) )
20 19 rexralbidv ⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → ( ∃ 𝑥 ∈ ( 𝑎 ∩ 𝑏 ) ∀ 𝑢 ∈ 𝑎 ∀ 𝑣 ∈ 𝑏 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝑔 ) ↔ ∃ 𝑥 ∈ ( 𝑎 ∩ 𝑏 ) ∀ 𝑢 ∈ 𝑎 ∀ 𝑣 ∈ 𝑏 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) )
21 16 20 anbi12d ⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → ( ( ( 𝑎 ∈ ran ( LineG ‘ 𝑔 ) ∧ 𝑏 ∈ ran ( LineG ‘ 𝑔 ) ) ∧ ∃ 𝑥 ∈ ( 𝑎 ∩ 𝑏 ) ∀ 𝑢 ∈ 𝑎 ∀ 𝑣 ∈ 𝑏 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝑔 ) ) ↔ ( ( 𝑎 ∈ ran 𝐿 ∧ 𝑏 ∈ ran 𝐿 ) ∧ ∃ 𝑥 ∈ ( 𝑎 ∩ 𝑏 ) ∀ 𝑢 ∈ 𝑎 ∀ 𝑣 ∈ 𝑏 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) ) )
22 21 opabbidv ⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ran ( LineG ‘ 𝑔 ) ∧ 𝑏 ∈ ran ( LineG ‘ 𝑔 ) ) ∧ ∃ 𝑥 ∈ ( 𝑎 ∩ 𝑏 ) ∀ 𝑢 ∈ 𝑎 ∀ 𝑣 ∈ 𝑏 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝑔 ) ) } = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ran 𝐿 ∧ 𝑏 ∈ ran 𝐿 ) ∧ ∃ 𝑥 ∈ ( 𝑎 ∩ 𝑏 ) ∀ 𝑢 ∈ 𝑎 ∀ 𝑣 ∈ 𝑏 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) } )
23 5 elexd ⊢ ( 𝜑 → 𝐺 ∈ V )
24 4 fvexi ⊢ 𝐿 ∈ V
25 rnexg ⊢ ( 𝐿 ∈ V → ran 𝐿 ∈ V )
26 24 25 mp1i ⊢ ( 𝜑 → ran 𝐿 ∈ V )
27 26 26 xpexd ⊢ ( 𝜑 → ( ran 𝐿 × ran 𝐿 ) ∈ V )
28 opabssxp ⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ran 𝐿 ∧ 𝑏 ∈ ran 𝐿 ) ∧ ∃ 𝑥 ∈ ( 𝑎 ∩ 𝑏 ) ∀ 𝑢 ∈ 𝑎 ∀ 𝑣 ∈ 𝑏 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) } ⊆ ( ran 𝐿 × ran 𝐿 )
29 28 a1i ⊢ ( 𝜑 → { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ran 𝐿 ∧ 𝑏 ∈ ran 𝐿 ) ∧ ∃ 𝑥 ∈ ( 𝑎 ∩ 𝑏 ) ∀ 𝑢 ∈ 𝑎 ∀ 𝑣 ∈ 𝑏 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) } ⊆ ( ran 𝐿 × ran 𝐿 ) )
30 27 29 ssexd ⊢ ( 𝜑 → { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ran 𝐿 ∧ 𝑏 ∈ ran 𝐿 ) ∧ ∃ 𝑥 ∈ ( 𝑎 ∩ 𝑏 ) ∀ 𝑢 ∈ 𝑎 ∀ 𝑣 ∈ 𝑏 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) } ∈ V )
31 9 22 23 30 fvmptd2 ⊢ ( 𝜑 → ( ⟂G ‘ 𝐺 ) = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ran 𝐿 ∧ 𝑏 ∈ ran 𝐿 ) ∧ ∃ 𝑥 ∈ ( 𝑎 ∩ 𝑏 ) ∀ 𝑢 ∈ 𝑎 ∀ 𝑣 ∈ 𝑏 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) } )
32 31 eleq2d ⊢ ( 𝜑 → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ⟂G ‘ 𝐺 ) ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ran 𝐿 ∧ 𝑏 ∈ ran 𝐿 ) ∧ ∃ 𝑥 ∈ ( 𝑎 ∩ 𝑏 ) ∀ 𝑢 ∈ 𝑎 ∀ 𝑣 ∈ 𝑏 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) } ) )
33 8 32 syl5bb ⊢ ( 𝜑 → ( 𝐴 ( ⟂G ‘ 𝐺 ) 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ran 𝐿 ∧ 𝑏 ∈ ran 𝐿 ) ∧ ∃ 𝑥 ∈ ( 𝑎 ∩ 𝑏 ) ∀ 𝑢 ∈ 𝑎 ∀ 𝑣 ∈ 𝑏 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) } ) )
34 ineq12 ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( 𝑎 ∩ 𝑏 ) = ( 𝐴 ∩ 𝐵 ) )
35 simpll ⊢ ( ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) ∧ 𝑥 ∈ ( 𝑎 ∩ 𝑏 ) ) → 𝑎 = 𝐴 )
36 simpllr ⊢ ( ( ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) ∧ 𝑥 ∈ ( 𝑎 ∩ 𝑏 ) ) ∧ 𝑢 ∈ 𝑎 ) → 𝑏 = 𝐵 )
37 36 raleqdv ⊢ ( ( ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) ∧ 𝑥 ∈ ( 𝑎 ∩ 𝑏 ) ) ∧ 𝑢 ∈ 𝑎 ) → ( ∀ 𝑣 ∈ 𝑏 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ↔ ∀ 𝑣 ∈ 𝐵 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) )
38 35 37 raleqbidva ⊢ ( ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) ∧ 𝑥 ∈ ( 𝑎 ∩ 𝑏 ) ) → ( ∀ 𝑢 ∈ 𝑎 ∀ 𝑣 ∈ 𝑏 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ↔ ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐵 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) )
39 34 38 rexeqbidva ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( ∃ 𝑥 ∈ ( 𝑎 ∩ 𝑏 ) ∀ 𝑢 ∈ 𝑎 ∀ 𝑣 ∈ 𝑏 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ↔ ∃ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐵 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) )
40 39 opelopab2a ⊢ ( ( 𝐴 ∈ ran 𝐿 ∧ 𝐵 ∈ ran 𝐿 ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ran 𝐿 ∧ 𝑏 ∈ ran 𝐿 ) ∧ ∃ 𝑥 ∈ ( 𝑎 ∩ 𝑏 ) ∀ 𝑢 ∈ 𝑎 ∀ 𝑣 ∈ 𝑏 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) } ↔ ∃ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐵 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) )
41 6 7 40 syl2anc ⊢ ( 𝜑 → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ran 𝐿 ∧ 𝑏 ∈ ran 𝐿 ) ∧ ∃ 𝑥 ∈ ( 𝑎 ∩ 𝑏 ) ∀ 𝑢 ∈ 𝑎 ∀ 𝑣 ∈ 𝑏 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) } ↔ ∃ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐵 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) )
42 33 41 bitrd ⊢ ( 𝜑 → ( 𝐴 ( ⟂G ‘ 𝐺 ) 𝐵 ↔ ∃ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐵 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) )