ragraghl

Description: Drawing two right angles at a point X on the same side of a line ( X L Y ) leads to points W and Z on the same ray from X . Theorem 11.19 of Schwabhauser p. 99. (Contributed by Thierry Arnoux, 5-Jul-2026)

	Ref	Expression
Hypotheses	ragraghl.p	$⊢ P = {Base}_{G}$
	ragraghl.l	$⊢ L = {Line}_{𝒢} (G)$
	ragraghl.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	ragraghl.x	$⊢ φ \to X \in P$
	ragraghl.y	$⊢ φ \to Y \in P$
	ragraghl.z	$⊢ φ \to Z \in P$
	ragraghl.1	$⊢ φ \to W \in P$
	ragraghl.2	$⊢ φ \to X \neq Y$
	ragraghl.3	$⊢ φ \to ⟨“ Y X Z ”⟩ \in ∟_{𝒢} (G)$
	ragraghl.4	$⊢ φ \to ⟨“ Y X W ”⟩ \in ∟_{𝒢} (G)$
	ragraghl.5	$⊢ φ \to Z {hp}_{𝒢} (G) (Y L X) W$
Assertion	ragraghl	$⊢ φ \to Z {hl}_{𝒢} (G) (X) W$

Proof

Step	Hyp	Ref	Expression
1		ragraghl.p	$⊢ P = {Base}_{G}$
2		ragraghl.l	$⊢ L = {Line}_{𝒢} (G)$
3		ragraghl.g	$⊢ φ \to G \in 𝒢_{Tarski}$
4		ragraghl.x	$⊢ φ \to X \in P$
5		ragraghl.y	$⊢ φ \to Y \in P$
6		ragraghl.z	$⊢ φ \to Z \in P$
7		ragraghl.1	$⊢ φ \to W \in P$
8		ragraghl.2	$⊢ φ \to X \neq Y$
9		ragraghl.3	$⊢ φ \to ⟨“ Y X Z ”⟩ \in ∟_{𝒢} (G)$
10		ragraghl.4	$⊢ φ \to ⟨“ Y X W ”⟩ \in ∟_{𝒢} (G)$
11		ragraghl.5	$⊢ φ \to Z {hp}_{𝒢} (G) (Y L X) W$
12		eqid	$⊢ Itv (G) = Itv (G)$
13		eqid	$⊢ dist (G) = dist (G)$
14		eqid	$⊢ {pInv}_{𝒢} (G) = {pInv}_{𝒢} (G)$
15	8	necomd	$⊢ φ \to Y \neq X$
16	1 12 2 3 5 4 15	tglinerflx2	$⊢ φ \to X \in (Y L X)$
17		eleq1w	$⊢ a = c \to (a \in (P ∖ (Y L X)) \leftrightarrow c \in (P ∖ (Y L X)))$
18		eleq1w	$⊢ b = d \to (b \in (P ∖ (Y L X)) \leftrightarrow d \in (P ∖ (Y L X)))$
19	17 18	bi2anan9	$⊢ (a = c \land b = d) \to ((a \in (P ∖ (Y L X)) \land b \in (P ∖ (Y L X))) \leftrightarrow (c \in (P ∖ (Y L X)) \land d \in (P ∖ (Y L X))))$
20		oveq12	$⊢ (a = c \land b = d) \to a Itv (G) b = c Itv (G) d$
21	20	eleq2d	$⊢ (a = c \land b = d) \to (s \in (a Itv (G) b) \leftrightarrow s \in (c Itv (G) d))$
22	21	rexbidv	$⊢ (a = c \land b = d) \to (\exists s \in (Y L X) s \in (a Itv (G) b) \leftrightarrow \exists s \in (Y L X) s \in (c Itv (G) d))$
23		eleq1w	$⊢ s = t \to (s \in (c Itv (G) d) \leftrightarrow t \in (c Itv (G) d))$
24	23	cbvrexvw	$⊢ \exists s \in (Y L X) s \in (c Itv (G) d) \leftrightarrow \exists t \in (Y L X) t \in (c Itv (G) d)$
25	22 24	bitrdi	$⊢ (a = c \land b = d) \to (\exists s \in (Y L X) s \in (a Itv (G) b) \leftrightarrow \exists t \in (Y L X) t \in (c Itv (G) d))$
26	19 25	anbi12d	$⊢ (a = c \land b = d) \to (((a \in (P ∖ (Y L X)) \land b \in (P ∖ (Y L X))) \land \exists s \in (Y L X) s \in (a Itv (G) b)) \leftrightarrow ((c \in (P ∖ (Y L X)) \land d \in (P ∖ (Y L X))) \land \exists t \in (Y L X) t \in (c Itv (G) d)))$
27	26	cbvopabv	$⊢ \{⟨a, b⟩ \| ((a \in (P ∖ (Y L X)) \land b \in (P ∖ (Y L X))) \land \exists s \in (Y L X) s \in (a Itv (G) b))\} = \{⟨c, d⟩ \| ((c \in (P ∖ (Y L X)) \land d \in (P ∖ (Y L X))) \land \exists t \in (Y L X) t \in (c Itv (G) d))\}$
28	1 12 2 3 5 4 15	tgelrnln	$⊢ φ \to Y L X \in ran L$
29	1 12 2 27 3 28 6 7 11	hpgne1	$⊢ φ \to \neg Z \in (Y L X)$
30		nelne2	$⊢ (X \in (Y L X) \land \neg Z \in (Y L X)) \to X \neq Z$
31	16 29 30	syl2anc	$⊢ φ \to X \neq Z$
32	31	necomd	$⊢ φ \to Z \neq X$
33	1 13 12 2 14 3 5 4 6 9 15 32	ragncol	$⊢ φ \to \neg (Z \in (Y L X) \lor Y = X)$
34	1 2 12 3 5 4 6 33	ncolrot1	$⊢ φ \to \neg (Y \in (X L Z) \lor X = Z)$
35	1 12 2 27 3 28 6 7 11	hpgne2	$⊢ φ \to \neg W \in (Y L X)$
36		nelne2	$⊢ (X \in (Y L X) \land \neg W \in (Y L X)) \to X \neq W$
37	16 35 36	syl2anc	$⊢ φ \to X \neq W$
38	37	necomd	$⊢ φ \to W \neq X$
39	1 13 12 2 14 3 5 4 7 10 15 38	ragncol	$⊢ φ \to \neg (W \in (Y L X) \lor Y = X)$
40	1 2 12 3 5 4 7 39	ncolrot1	$⊢ φ \to \neg (Y \in (X L W) \lor X = W)$
41		eqid	$⊢ {hl}_{𝒢} (G) = {hl}_{𝒢} (G)$
42	1 12 3 41 5 4 6 15 31	cgraid	$⊢ φ \to ⟨“ Y X Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ Y X Z ”⟩$
43	1 3 5 4 6 5 4 7 9 10 15 37 15 31	ragcgra	$⊢ φ \to ⟨“ Y X Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ Y X W ”⟩$
44	1 12 2 3 28 7 27 35	hpgid	$⊢ φ \to W {hp}_{𝒢} (G) (Y L X) W$
45	1 12 13 3 5 4 6 5 4 7 2 34 40 6 7 41 42 43 11 44	acopyeu	$⊢ φ \to Z {hl}_{𝒢} (G) (X) W$

Metamath Proof Explorer

Theorem ragraghl

Proof