Metamath Proof Explorer

Theorem 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 ⊢ 𝑃 = ( Base ‘ 𝐺 )
ragraghl.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
ragraghl.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
ragraghl.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
ragraghl.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
ragraghl.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
ragraghl.1 ⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
ragraghl.2 ⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
ragraghl.3 ⊢ ( 𝜑 → ⟨“ 𝑌 𝑋 𝑍 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
ragraghl.4 ⊢ ( 𝜑 → ⟨“ 𝑌 𝑋 𝑊 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
ragraghl.5 ⊢ ( 𝜑 → 𝑍 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑋 ) ) 𝑊 )
Assertion ragraghl ( 𝜑 → 𝑍 ( ( hlG ‘ 𝐺 ) ‘ 𝑋 ) 𝑊 )

Proof

Step Hyp Ref Expression
1 ragraghl.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 ragraghl.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
3 ragraghl.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
4 ragraghl.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
5 ragraghl.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
6 ragraghl.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
7 ragraghl.1 ⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
8 ragraghl.2 ⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
9 ragraghl.3 ⊢ ( 𝜑 → ⟨“ 𝑌 𝑋 𝑍 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
10 ragraghl.4 ⊢ ( 𝜑 → ⟨“ 𝑌 𝑋 𝑊 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
11 ragraghl.5 ⊢ ( 𝜑 → 𝑍 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑋 ) ) 𝑊 )
12 eqid ⊢ ( Itv ‘ 𝐺 ) = ( Itv ‘ 𝐺 )
13 eqid ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
14 eqid ⊢ ( pInvG ‘ 𝐺 ) = ( pInvG ‘ 𝐺 )
15 8 necomd ⊢ ( 𝜑 → 𝑌 ≠ 𝑋 )
16 1 12 2 3 5 4 15 tglinerflx2 ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑌 𝐿 𝑋 ) )
17 eleq1w ⊢ ( 𝑎 = 𝑐 → ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑋 ) ) ↔ 𝑐 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑋 ) ) ) )
18 eleq1w ⊢ ( 𝑏 = 𝑑 → ( 𝑏 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑋 ) ) ↔ 𝑑 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑋 ) ) ) )
19 17 18 bi2anan9 ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑋 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑋 ) ) ) ↔ ( 𝑐 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑋 ) ) ∧ 𝑑 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑋 ) ) ) ) )
20 oveq12 ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( 𝑎 ( Itv ‘ 𝐺 ) 𝑏 ) = ( 𝑐 ( Itv ‘ 𝐺 ) 𝑑 ) )
21 20 eleq2d ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( 𝑠 ∈ ( 𝑎 ( Itv ‘ 𝐺 ) 𝑏 ) ↔ 𝑠 ∈ ( 𝑐 ( Itv ‘ 𝐺 ) 𝑑 ) ) )
22 21 rexbidv ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( ∃ 𝑠 ∈ ( 𝑌 𝐿 𝑋 ) 𝑠 ∈ ( 𝑎 ( Itv ‘ 𝐺 ) 𝑏 ) ↔ ∃ 𝑠 ∈ ( 𝑌 𝐿 𝑋 ) 𝑠 ∈ ( 𝑐 ( Itv ‘ 𝐺 ) 𝑑 ) ) )
23 eleq1w ⊢ ( 𝑠 = 𝑡 → ( 𝑠 ∈ ( 𝑐 ( Itv ‘ 𝐺 ) 𝑑 ) ↔ 𝑡 ∈ ( 𝑐 ( Itv ‘ 𝐺 ) 𝑑 ) ) )
24 23 cbvrexvw ⊢ ( ∃ 𝑠 ∈ ( 𝑌 𝐿 𝑋 ) 𝑠 ∈ ( 𝑐 ( Itv ‘ 𝐺 ) 𝑑 ) ↔ ∃ 𝑡 ∈ ( 𝑌 𝐿 𝑋 ) 𝑡 ∈ ( 𝑐 ( Itv ‘ 𝐺 ) 𝑑 ) )
25 22 24 bitrdi ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( ∃ 𝑠 ∈ ( 𝑌 𝐿 𝑋 ) 𝑠 ∈ ( 𝑎 ( Itv ‘ 𝐺 ) 𝑏 ) ↔ ∃ 𝑡 ∈ ( 𝑌 𝐿 𝑋 ) 𝑡 ∈ ( 𝑐 ( Itv ‘ 𝐺 ) 𝑑 ) ) )
26 19 25 anbi12d ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑋 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑋 ) ) ) ∧ ∃ 𝑠 ∈ ( 𝑌 𝐿 𝑋 ) 𝑠 ∈ ( 𝑎 ( Itv ‘ 𝐺 ) 𝑏 ) ) ↔ ( ( 𝑐 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑋 ) ) ∧ 𝑑 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑋 ) ) ) ∧ ∃ 𝑡 ∈ ( 𝑌 𝐿 𝑋 ) 𝑡 ∈ ( 𝑐 ( Itv ‘ 𝐺 ) 𝑑 ) ) ) )
27 26 cbvopabv ⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑋 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑋 ) ) ) ∧ ∃ 𝑠 ∈ ( 𝑌 𝐿 𝑋 ) 𝑠 ∈ ( 𝑎 ( Itv ‘ 𝐺 ) 𝑏 ) ) } = { ⟨ 𝑐 , 𝑑 ⟩ ∣ ( ( 𝑐 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑋 ) ) ∧ 𝑑 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑋 ) ) ) ∧ ∃ 𝑡 ∈ ( 𝑌 𝐿 𝑋 ) 𝑡 ∈ ( 𝑐 ( Itv ‘ 𝐺 ) 𝑑 ) ) }
28 1 12 2 3 5 4 15 tgelrnln ⊢ ( 𝜑 → ( 𝑌 𝐿 𝑋 ) ∈ ran 𝐿 )
29 1 12 2 27 3 28 6 7 11 hpgne1 ⊢ ( 𝜑 → ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑋 ) )
30 nelne2 ⊢ ( ( 𝑋 ∈ ( 𝑌 𝐿 𝑋 ) ∧ ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑋 ) ) → 𝑋 ≠ 𝑍 )
31 16 29 30 syl2anc ⊢ ( 𝜑 → 𝑋 ≠ 𝑍 )
32 31 necomd ⊢ ( 𝜑 → 𝑍 ≠ 𝑋 )
33 1 13 12 2 14 3 5 4 6 9 15 32 ragncol ⊢ ( 𝜑 → ¬ ( 𝑍 ∈ ( 𝑌 𝐿 𝑋 ) ∨ 𝑌 = 𝑋 ) )
34 1 2 12 3 5 4 6 33 ncolrot1 ⊢ ( 𝜑 → ¬ ( 𝑌 ∈ ( 𝑋 𝐿 𝑍 ) ∨ 𝑋 = 𝑍 ) )
35 1 12 2 27 3 28 6 7 11 hpgne2 ⊢ ( 𝜑 → ¬ 𝑊 ∈ ( 𝑌 𝐿 𝑋 ) )
36 nelne2 ⊢ ( ( 𝑋 ∈ ( 𝑌 𝐿 𝑋 ) ∧ ¬ 𝑊 ∈ ( 𝑌 𝐿 𝑋 ) ) → 𝑋 ≠ 𝑊 )
37 16 35 36 syl2anc ⊢ ( 𝜑 → 𝑋 ≠ 𝑊 )
38 37 necomd ⊢ ( 𝜑 → 𝑊 ≠ 𝑋 )
39 1 13 12 2 14 3 5 4 7 10 15 38 ragncol ⊢ ( 𝜑 → ¬ ( 𝑊 ∈ ( 𝑌 𝐿 𝑋 ) ∨ 𝑌 = 𝑋 ) )
40 1 2 12 3 5 4 7 39 ncolrot1 ⊢ ( 𝜑 → ¬ ( 𝑌 ∈ ( 𝑋 𝐿 𝑊 ) ∨ 𝑋 = 𝑊 ) )
41 eqid ⊢ ( hlG ‘ 𝐺 ) = ( hlG ‘ 𝐺 )
42 1 12 3 41 5 4 6 15 31 cgraid ⊢ ( 𝜑 → ⟨“ 𝑌 𝑋 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑌 𝑋 𝑍 ”⟩ )
43 1 3 5 4 6 5 4 7 9 10 15 37 15 31 ragcgra ⊢ ( 𝜑 → ⟨“ 𝑌 𝑋 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑌 𝑋 𝑊 ”⟩ )
44 1 12 2 3 28 7 27 35 hpgid ⊢ ( 𝜑 → 𝑊 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑋 ) ) 𝑊 )
45 1 12 13 3 5 4 6 5 4 7 2 34 40 6 7 41 42 43 11 44 acopyeu ⊢ ( 𝜑 → 𝑍 ( ( hlG ‘ 𝐺 ) ‘ 𝑋 ) 𝑊 )