Metamath Proof Explorer

Theorem ragsupplcgra

Description: An angle <" X Y Z "> is a right angle exactly when it is congruent to its supplementary angle <" X Y W "> . Theorem 11.18 of Schwabhauser p. 98. (Contributed by Thierry Arnoux, 13-Jul-2026)

Ref Expression
Hypotheses ragsupplcgra.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
ragsupplcgra.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
ragsupplcgra.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
ragsupplcgra.7 ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑃 ∖ { 𝑌 } ) )
ragsupplcgra.x ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
ragsupplcgra.z ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑃 ∖ { 𝑌 } ) )
ragsupplcgra.w ⊢ ( 𝜑 → 𝑊 ∈ ( 𝑃 ∖ { 𝑌 } ) )
ragsupplcgra.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑍 𝐼 𝑊 ) )
Assertion ragsupplcgra ( 𝜑 → ( ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ↔ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑊 ”⟩ ) )

Proof

Step Hyp Ref Expression
1 ragsupplcgra.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 ragsupplcgra.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
3 ragsupplcgra.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
4 ragsupplcgra.7 ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑃 ∖ { 𝑌 } ) )
5 ragsupplcgra.x ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
6 ragsupplcgra.z ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑃 ∖ { 𝑌 } ) )
7 ragsupplcgra.w ⊢ ( 𝜑 → 𝑊 ∈ ( 𝑃 ∖ { 𝑌 } ) )
8 ragsupplcgra.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑍 𝐼 𝑊 ) )
9 3 adantr ⊢ ( ( 𝜑 ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) → 𝐺 ∈ TarskiG )
10 4 eldifad ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
11 10 adantr ⊢ ( ( 𝜑 ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) → 𝑋 ∈ 𝑃 )
12 5 adantr ⊢ ( ( 𝜑 ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) → 𝑌 ∈ 𝑃 )
13 6 eldifad ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
14 13 adantr ⊢ ( ( 𝜑 ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) → 𝑍 ∈ 𝑃 )
15 7 eldifad ⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
16 15 adantr ⊢ ( ( 𝜑 ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) → 𝑊 ∈ 𝑃 )
17 simpr ⊢ ( ( 𝜑 ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
18 eqid ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
19 eqid ⊢ ( LineG ‘ 𝐺 ) = ( LineG ‘ 𝐺 )
20 eqid ⊢ ( pInvG ‘ 𝐺 ) = ( pInvG ‘ 𝐺 )
21 1 18 2 19 20 9 11 12 14 17 ragcom ⊢ ( ( 𝜑 ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) → ⟨“ 𝑍 𝑌 𝑋 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
22 6 eldifsnbd ⊢ ( 𝜑 → 𝑍 ≠ 𝑌 )
23 22 adantr ⊢ ( ( 𝜑 ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) → 𝑍 ≠ 𝑌 )
24 8 adantr ⊢ ( ( 𝜑 ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) → 𝑌 ∈ ( 𝑍 𝐼 𝑊 ) )
25 1 19 2 9 12 16 14 24 btwncolg2 ⊢ ( ( 𝜑 ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) → ( 𝑍 ∈ ( 𝑌 ( LineG ‘ 𝐺 ) 𝑊 ) ∨ 𝑌 = 𝑊 ) )
26 1 18 2 19 20 9 14 12 11 16 21 23 25 ragcol ⊢ ( ( 𝜑 ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) → ⟨“ 𝑊 𝑌 𝑋 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
27 1 18 2 19 20 9 16 12 11 26 ragcom ⊢ ( ( 𝜑 ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) → ⟨“ 𝑋 𝑌 𝑊 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
28 4 eldifsnbd ⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
29 28 adantr ⊢ ( ( 𝜑 ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) → 𝑋 ≠ 𝑌 )
30 7 eldifsnbd ⊢ ( 𝜑 → 𝑊 ≠ 𝑌 )
31 30 necomd ⊢ ( 𝜑 → 𝑌 ≠ 𝑊 )
32 31 adantr ⊢ ( ( 𝜑 ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) → 𝑌 ≠ 𝑊 )
33 22 necomd ⊢ ( 𝜑 → 𝑌 ≠ 𝑍 )
34 33 adantr ⊢ ( ( 𝜑 ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) → 𝑌 ≠ 𝑍 )
35 1 9 11 12 14 11 12 16 17 27 29 32 29 34 ragcgra ⊢ ( ( 𝜑 ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑊 ”⟩ )
36 3 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑊 ”⟩ ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝑌 𝑧 ”⟩ ) ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ 𝑧 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑊 ) → 𝐺 ∈ TarskiG )
37 13 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑊 ”⟩ ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝑌 𝑧 ”⟩ ) ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ 𝑧 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑊 ) → 𝑍 ∈ 𝑃 )
38 10 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑊 ”⟩ ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝑌 𝑧 ”⟩ ) ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ 𝑧 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑊 ) → 𝑋 ∈ 𝑃 )
39 simp-4r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑊 ”⟩ ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝑌 𝑧 ”⟩ ) ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ 𝑧 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑊 ) → 𝑧 ∈ 𝑃 )
40 simp-5r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑊 ”⟩ ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝑌 𝑧 ”⟩ ) ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ 𝑧 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑊 ) → 𝑥 ∈ 𝑃 )
41 eqid ⊢ ( cgrG ‘ 𝐺 ) = ( cgrG ‘ 𝐺 )
42 5 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑊 ”⟩ ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝑌 𝑧 ”⟩ ) ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ 𝑧 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑊 ) → 𝑌 ∈ 𝑃 )
43 simpllr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑊 ”⟩ ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝑌 𝑧 ”⟩ ) ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ 𝑧 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑊 ) → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝑌 𝑧 ”⟩ )
44 1 18 2 41 36 38 42 37 40 42 39 43 cgr3simp3 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑊 ”⟩ ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝑌 𝑧 ”⟩ ) ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ 𝑧 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑊 ) → ( 𝑍 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝑧 ( dist ‘ 𝐺 ) 𝑥 ) )
45 1 18 2 36 37 38 39 40 44 tgcgrcomlr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑊 ”⟩ ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝑌 𝑧 ”⟩ ) ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ 𝑧 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑊 ) → ( 𝑋 ( dist ‘ 𝐺 ) 𝑍 ) = ( 𝑥 ( dist ‘ 𝐺 ) 𝑧 ) )
46 eqid ⊢ ( hlG ‘ 𝐺 ) = ( hlG ‘ 𝐺 )
47 28 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑊 ”⟩ ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝑌 𝑧 ”⟩ ) ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ 𝑧 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑊 ) → 𝑋 ≠ 𝑌 )
48 47 necomd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑊 ”⟩ ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝑌 𝑧 ”⟩ ) ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ 𝑧 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑊 ) → 𝑌 ≠ 𝑋 )
49 1 2 46 38 38 42 36 47 hlid ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑊 ”⟩ ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝑌 𝑧 ”⟩ ) ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ 𝑧 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑊 ) → 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 )
50 simplr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑊 ”⟩ ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝑌 𝑧 ”⟩ ) ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ 𝑧 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑊 ) → 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 )
51 eqidd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑊 ”⟩ ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝑌 𝑧 ”⟩ ) ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ 𝑧 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑊 ) → ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) )
52 1 18 2 41 36 38 42 37 40 42 39 43 cgr3simp1 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑊 ”⟩ ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝑌 𝑧 ”⟩ ) ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ 𝑧 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑊 ) → ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) = ( 𝑥 ( dist ‘ 𝐺 ) 𝑌 ) )
53 52 eqcomd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑊 ”⟩ ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝑌 𝑧 ”⟩ ) ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ 𝑧 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑊 ) → ( 𝑥 ( dist ‘ 𝐺 ) 𝑌 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) )
54 1 18 2 36 40 42 38 42 53 tgcgrcomlr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑊 ”⟩ ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝑌 𝑧 ”⟩ ) ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ 𝑧 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑊 ) → ( 𝑌 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) )
55 1 18 46 42 42 38 36 38 47 48 49 50 51 54 hlcgreq ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑊 ”⟩ ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝑌 𝑧 ”⟩ ) ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ 𝑧 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑊 ) → 𝑋 = 𝑥 )
56 eqid ⊢ ( ( pInvG ‘ 𝐺 ) ‘ 𝑌 ) = ( ( pInvG ‘ 𝐺 ) ‘ 𝑌 )
57 1 18 2 19 20 36 42 56 37 mircl ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑊 ”⟩ ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝑌 𝑧 ”⟩ ) ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ 𝑧 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑊 ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑌 ) ‘ 𝑍 ) ∈ 𝑃 )
58 22 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑊 ”⟩ ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝑌 𝑧 ”⟩ ) ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ 𝑧 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑊 ) → 𝑍 ≠ 𝑌 )
59 1 18 2 19 20 36 42 56 37 mirbtwn ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑊 ”⟩ ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝑌 𝑧 ”⟩ ) ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ 𝑧 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑊 ) → 𝑌 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑌 ) ‘ 𝑍 ) 𝐼 𝑍 ) )
60 1 18 2 36 57 42 37 59 tgbtwncom ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑊 ”⟩ ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝑌 𝑧 ”⟩ ) ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ 𝑧 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑊 ) → 𝑌 ∈ ( 𝑍 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑌 ) ‘ 𝑍 ) ) )
61 15 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑊 ”⟩ ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝑌 𝑧 ”⟩ ) ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ 𝑧 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑊 ) → 𝑊 ∈ 𝑃 )
62 simpr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑊 ”⟩ ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝑌 𝑧 ”⟩ ) ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ 𝑧 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑊 ) → 𝑧 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑊 )
63 1 2 46 39 61 42 36 62 hlcomd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑊 ”⟩ ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝑌 𝑧 ”⟩ ) ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ 𝑧 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑊 ) → 𝑊 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑧 )
64 1 18 2 3 13 5 15 8 tgbtwncom ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑊 𝐼 𝑍 ) )
65 64 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑊 ”⟩ ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝑌 𝑧 ”⟩ ) ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ 𝑧 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑊 ) → 𝑌 ∈ ( 𝑊 𝐼 𝑍 ) )
66 1 2 46 61 39 37 36 42 63 65 btwnhl ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑊 ”⟩ ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝑌 𝑧 ”⟩ ) ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ 𝑧 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑊 ) → 𝑌 ∈ ( 𝑧 𝐼 𝑍 ) )
67 1 18 2 36 39 42 37 66 tgbtwncom ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑊 ”⟩ ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝑌 𝑧 ”⟩ ) ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ 𝑧 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑊 ) → 𝑌 ∈ ( 𝑍 𝐼 𝑧 ) )
68 1 18 2 19 20 36 42 56 37 mircgr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑊 ”⟩ ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝑌 𝑧 ”⟩ ) ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ 𝑧 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑊 ) → ( 𝑌 ( dist ‘ 𝐺 ) ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑌 ) ‘ 𝑍 ) ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) )
69 1 18 2 41 36 38 42 37 40 42 39 43 cgr3simp2 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑊 ”⟩ ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝑌 𝑧 ”⟩ ) ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ 𝑧 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑊 ) → ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑧 ) )
70 69 eqcomd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑊 ”⟩ ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝑌 𝑧 ”⟩ ) ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ 𝑧 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑊 ) → ( 𝑌 ( dist ‘ 𝐺 ) 𝑧 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) )
71 1 18 2 36 42 42 37 37 57 39 58 60 67 68 70 tgsegconeq ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑊 ”⟩ ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝑌 𝑧 ”⟩ ) ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ 𝑧 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑊 ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑌 ) ‘ 𝑍 ) = 𝑧 )
72 55 71 oveq12d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑊 ”⟩ ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝑌 𝑧 ”⟩ ) ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ 𝑧 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑊 ) → ( 𝑋 ( dist ‘ 𝐺 ) ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑌 ) ‘ 𝑍 ) ) = ( 𝑥 ( dist ‘ 𝐺 ) 𝑧 ) )
73 45 72 eqtr4d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑊 ”⟩ ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝑌 𝑧 ”⟩ ) ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ 𝑧 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑊 ) → ( 𝑋 ( dist ‘ 𝐺 ) 𝑍 ) = ( 𝑋 ( dist ‘ 𝐺 ) ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑌 ) ‘ 𝑍 ) ) )
74 1 18 2 19 20 3 10 5 13 israg ⊢ ( 𝜑 → ( ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ↔ ( 𝑋 ( dist ‘ 𝐺 ) 𝑍 ) = ( 𝑋 ( dist ‘ 𝐺 ) ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑌 ) ‘ 𝑍 ) ) ) )
75 74 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑊 ”⟩ ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝑌 𝑧 ”⟩ ) ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ 𝑧 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑊 ) → ( ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ↔ ( 𝑋 ( dist ‘ 𝐺 ) 𝑍 ) = ( 𝑋 ( dist ‘ 𝐺 ) ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑌 ) ‘ 𝑍 ) ) ) )
76 73 75 mpbird ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑊 ”⟩ ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝑌 𝑧 ”⟩ ) ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ 𝑧 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑊 ) → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
77 76 3anasss ⊢ ( ( ( ( ( 𝜑 ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑊 ”⟩ ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝑌 𝑧 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ∧ 𝑧 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑊 ) ) → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
78 1 2 46 3 10 5 13 10 5 15 iscgra ⊢ ( 𝜑 → ( ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑊 ”⟩ ↔ ∃ 𝑥 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝑌 𝑧 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ∧ 𝑧 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑊 ) ) )
79 78 biimpa ⊢ ( ( 𝜑 ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑊 ”⟩ ) → ∃ 𝑥 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝑌 𝑧 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ∧ 𝑧 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑊 ) )
80 77 79 r19.29vva ⊢ ( ( 𝜑 ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑊 ”⟩ ) → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
81 35 80 impbida ⊢ ( 𝜑 → ( ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ↔ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑊 ”⟩ ) )