Metamath Proof Explorer


Theorem perpln2

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 perpln2 φ B 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 26 rneqd φ ran 𝒢 G = ran a b | a ran L b ran L x a b u a v b ⟨“ uxv ”⟩ 𝒢 G
28 23 rnssi ran a b | a ran L b ran L x a b u a v b ⟨“ uxv ”⟩ 𝒢 G ran ran L × ran L
29 27 28 eqsstrdi φ ran 𝒢 G ran ran L × ran L
30 rnxpss ran ran L × ran L ran L
31 29 30 sstrdi φ ran 𝒢 G ran L
32 relopabv Rel a b | a ran L b ran L x a b u a v b ⟨“ uxv ”⟩ 𝒢 G
33 26 releqd φ Rel 𝒢 G Rel a b | a ran L b ran L x a b u a v b ⟨“ uxv ”⟩ 𝒢 G
34 32 33 mpbiri φ Rel 𝒢 G
35 brrelex12 Rel 𝒢 G A 𝒢 G B A V B V
36 34 3 35 syl2anc φ A V B V
37 36 simpld φ A V
38 36 simprd φ B V
39 brelrng A V B V A 𝒢 G B B ran 𝒢 G
40 37 38 3 39 syl3anc φ B ran 𝒢 G
41 31 40 sseldd φ B ran L