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 P = Base G
isperp.d - ˙ = dist G
isperp.i I = Itv G
isperp.l L = Line 𝒢 G
isperp.g φ G 𝒢 Tarski
isperp.a φ A ran L
isperp2.b φ B ran L
isperp2.x φ X A B
Assertion isperp2 φ A 𝒢 G B u A v B ⟨“ uXv ”⟩ 𝒢 G

Proof

Step Hyp Ref Expression
1 isperp.p P = Base G
2 isperp.d - ˙ = dist G
3 isperp.i I = Itv G
4 isperp.l L = Line 𝒢 G
5 isperp.g φ G 𝒢 Tarski
6 isperp.a φ A ran L
7 isperp2.b φ B ran L
8 isperp2.x φ X A B
9 eqidd φ A 𝒢 G B x A B u A v B u = u
10 5 ad4antr φ A 𝒢 G B x A B u A v B G 𝒢 Tarski
11 6 ad4antr φ A 𝒢 G B x A B u A v B A ran L
12 7 ad4antr φ A 𝒢 G B x A B u A v B B ran L
13 simp-4r φ A 𝒢 G B x A B u A v B A 𝒢 G B
14 1 2 3 4 10 11 12 13 perpneq φ A 𝒢 G B x A B u A v B A B
15 simpllr φ A 𝒢 G B x A B u A v B x A B
16 8 ad4antr φ A 𝒢 G B x A B u A v B X A B
17 1 3 4 10 11 12 14 15 16 tglineineq φ A 𝒢 G B x A B u A v B x = X
18 eqidd φ A 𝒢 G B x A B u A v B v = v
19 9 17 18 s3eqd φ A 𝒢 G B x A B u A v B ⟨“ uxv ”⟩ = ⟨“ uXv ”⟩
20 19 eleq1d φ A 𝒢 G B x A B u A v B ⟨“ uxv ”⟩ 𝒢 G ⟨“ uXv ”⟩ 𝒢 G
21 20 biimpd φ A 𝒢 G B x A B u A v B ⟨“ uxv ”⟩ 𝒢 G ⟨“ uXv ”⟩ 𝒢 G
22 21 ralimdva φ A 𝒢 G B x A B u A v B ⟨“ uxv ”⟩ 𝒢 G v B ⟨“ uXv ”⟩ 𝒢 G
23 22 ralimdva φ A 𝒢 G B x A B u A v B ⟨“ uxv ”⟩ 𝒢 G u A v B ⟨“ uXv ”⟩ 𝒢 G
24 23 imp φ A 𝒢 G B x A B u A v B ⟨“ uxv ”⟩ 𝒢 G u A v B ⟨“ uXv ”⟩ 𝒢 G
25 1 2 3 4 5 6 7 isperp φ A 𝒢 G B x A B u A v B ⟨“ uxv ”⟩ 𝒢 G
26 25 biimpa φ A 𝒢 G B x A B u A v B ⟨“ uxv ”⟩ 𝒢 G
27 24 26 r19.29a φ A 𝒢 G B u A v B ⟨“ uXv ”⟩ 𝒢 G
28 s3eq2 x = X ⟨“ uxv ”⟩ = ⟨“ uXv ”⟩
29 28 eleq1d x = X ⟨“ uxv ”⟩ 𝒢 G ⟨“ uXv ”⟩ 𝒢 G
30 29 2ralbidv x = X u A v B ⟨“ uxv ”⟩ 𝒢 G u A v B ⟨“ uXv ”⟩ 𝒢 G
31 30 rspcev X A B u A v B ⟨“ uXv ”⟩ 𝒢 G x A B u A v B ⟨“ uxv ”⟩ 𝒢 G
32 8 31 sylan φ u A v B ⟨“ uXv ”⟩ 𝒢 G x A B u A v B ⟨“ uxv ”⟩ 𝒢 G
33 25 adantr φ u A v B ⟨“ uXv ”⟩ 𝒢 G A 𝒢 G B x A B u A v B ⟨“ uxv ”⟩ 𝒢 G
34 32 33 mpbird φ u A v B ⟨“ uXv ”⟩ 𝒢 G A 𝒢 G B
35 27 34 impbida φ A 𝒢 G B u A v B ⟨“ uXv ”⟩ 𝒢 G