Metamath Proof Explorer


Theorem perpln1

Description: Derive a line from perpendicularity. (Contributed by Thierry Arnoux, 27-Nov-2019)

Ref Expression
Hypotheses perpln.l L = Line 𝒢 G
perpln.1 φ G 𝒢 Tarski
perpln.2 φ A 𝒢 G B
Assertion perpln1 φ A ran L

Proof

Step Hyp Ref Expression
1 perpln.l L = Line 𝒢 G
2 perpln.1 φ G 𝒢 Tarski
3 perpln.2 φ A 𝒢 G B
4 df-perpg 𝒢 = g V a b | a ran Line 𝒢 g b ran Line 𝒢 g x a b u a v b ⟨“ uxv ”⟩ 𝒢 g
5 simpr φ g = G g = G
6 5 fveq2d φ g = G Line 𝒢 g = Line 𝒢 G
7 6 1 eqtr4di φ g = G Line 𝒢 g = L
8 7 rneqd φ g = G ran Line 𝒢 g = ran L
9 8 eleq2d φ g = G a ran Line 𝒢 g a ran L
10 8 eleq2d φ g = G b ran Line 𝒢 g b ran L
11 9 10 anbi12d φ g = G a ran Line 𝒢 g b ran Line 𝒢 g a ran L b ran L
12 5 fveq2d φ g = G 𝒢 g = 𝒢 G
13 12 eleq2d φ g = G ⟨“ uxv ”⟩ 𝒢 g ⟨“ uxv ”⟩ 𝒢 G
14 13 ralbidv φ g = G v b ⟨“ uxv ”⟩ 𝒢 g v b ⟨“ uxv ”⟩ 𝒢 G
15 14 rexralbidv φ g = G x a b u a v b ⟨“ uxv ”⟩ 𝒢 g x a b u a v b ⟨“ uxv ”⟩ 𝒢 G
16 11 15 anbi12d φ g = G a ran Line 𝒢 g b ran Line 𝒢 g x a b u a v b ⟨“ uxv ”⟩ 𝒢 g a ran L b ran L x a b u a v b ⟨“ uxv ”⟩ 𝒢 G
17 16 opabbidv φ g = G a b | a ran Line 𝒢 g b ran Line 𝒢 g x a b u a v b ⟨“ uxv ”⟩ 𝒢 g = a b | a ran L b ran L x a b u a v b ⟨“ uxv ”⟩ 𝒢 G
18 2 elexd φ G V
19 1 fvexi L V
20 rnexg L V ran L V
21 19 20 mp1i φ ran L V
22 21 21 xpexd φ ran L × ran L V
23 opabssxp a b | a ran L b ran L x a b u a v b ⟨“ uxv ”⟩ 𝒢 G ran L × ran L
24 23 a1i φ a b | a ran L b ran L x a b u a v b ⟨“ uxv ”⟩ 𝒢 G ran L × ran L
25 22 24 ssexd φ a b | a ran L b ran L x a b u a v b ⟨“ uxv ”⟩ 𝒢 G V
26 4 17 18 25 fvmptd2 φ 𝒢 G = a b | a ran L b ran L x a b u a v b ⟨“ uxv ”⟩ 𝒢 G
27 anass a ran L b ran L x a b u a v b ⟨“ uxv ”⟩ 𝒢 G a ran L b ran L x a b u a v b ⟨“ uxv ”⟩ 𝒢 G
28 27 opabbii a b | a ran L b ran L x a b u a v b ⟨“ uxv ”⟩ 𝒢 G = a b | a ran L b ran L x a b u a v b ⟨“ uxv ”⟩ 𝒢 G
29 26 28 eqtrdi φ 𝒢 G = a b | a ran L b ran L x a b u a v b ⟨“ uxv ”⟩ 𝒢 G
30 29 dmeqd φ dom 𝒢 G = dom a b | a ran L b ran L x a b u a v b ⟨“ uxv ”⟩ 𝒢 G
31 dmopabss dom a b | a ran L b ran L x a b u a v b ⟨“ uxv ”⟩ 𝒢 G ran L
32 30 31 eqsstrdi φ dom 𝒢 G ran L
33 relopabv Rel a b | a ran L b ran L x a b u a v b ⟨“ uxv ”⟩ 𝒢 G
34 26 releqd φ Rel 𝒢 G Rel a b | a ran L b ran L x a b u a v b ⟨“ uxv ”⟩ 𝒢 G
35 33 34 mpbiri φ Rel 𝒢 G
36 brrelex12 Rel 𝒢 G A 𝒢 G B A V B V
37 35 3 36 syl2anc φ A V B V
38 37 simpld φ A V
39 37 simprd φ B V
40 breldmg A V B V A 𝒢 G B A dom 𝒢 G
41 38 39 3 40 syl3anc φ A dom 𝒢 G
42 32 41 sseldd φ A ran L