Metamath Proof Explorer

Theorem ragcgra

Description: Right angles are congruent with each other. Theorem 11.16 of Schwabhauser p. 98. (Contributed by Thierry Arnoux, 5-Jul-2026)

Ref Expression
Hypotheses ragcgra.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
ragcgra.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
ragcgra.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
ragcgra.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
ragcgra.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
ragcgra.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
ragcgra.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
ragcgra.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
ragcgra.1 ⊢ ( 𝜑 → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
ragcgra.2 ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
ragcgra.3 ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
ragcgra.4 ⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
ragcgra.5 ⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
ragcgra.6 ⊢ ( 𝜑 → 𝑌 ≠ 𝑍 )
Assertion ragcgra ( 𝜑 → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ )

Proof

Step Hyp Ref Expression
1 ragcgra.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 ragcgra.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
3 ragcgra.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
4 ragcgra.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
5 ragcgra.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
6 ragcgra.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
7 ragcgra.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
8 ragcgra.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
9 ragcgra.1 ⊢ ( 𝜑 → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
10 ragcgra.2 ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
11 ragcgra.3 ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
12 ragcgra.4 ⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
13 ragcgra.5 ⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
14 ragcgra.6 ⊢ ( 𝜑 → 𝑌 ≠ 𝑍 )
15 eqid ⊢ ( Itv ‘ 𝐺 ) = ( Itv ‘ 𝐺 )
16 eqid ⊢ ( hlG ‘ 𝐺 ) = ( hlG ‘ 𝐺 )
17 2 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑎 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑐 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → 𝐺 ∈ TarskiG )
18 3 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑎 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑐 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → 𝑋 ∈ 𝑃 )
19 4 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑎 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑐 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → 𝑌 ∈ 𝑃 )
20 5 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑎 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑐 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → 𝑍 ∈ 𝑃 )
21 6 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑎 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑐 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → 𝐴 ∈ 𝑃 )
22 7 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑎 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑐 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → 𝐵 ∈ 𝑃 )
23 8 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑎 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑐 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → 𝐶 ∈ 𝑃 )
24 simp-6r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑎 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑐 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → 𝑎 ∈ 𝑃 )
25 simpllr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑎 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑐 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → 𝑐 ∈ 𝑃 )
26 eqid ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
27 eqid ⊢ ( cgrG ‘ 𝐺 ) = ( cgrG ‘ 𝐺 )
28 simp-4r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑎 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑐 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → ( 𝐵 ( dist ‘ 𝐺 ) 𝑎 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) )
29 28 eqcomd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑎 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑐 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝑎 ) )
30 1 26 15 17 19 18 22 24 29 tgcgrcomlr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑎 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑐 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) = ( 𝑎 ( dist ‘ 𝐺 ) 𝐵 ) )
31 simpr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑎 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑐 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → ( 𝐵 ( dist ‘ 𝐺 ) 𝑐 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) )
32 31 eqcomd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑎 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑐 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝑐 ) )
33 eqid ⊢ ( LineG ‘ 𝐺 ) = ( LineG ‘ 𝐺 )
34 eqid ⊢ ( pInvG ‘ 𝐺 ) = ( pInvG ‘ 𝐺 )
35 12 necomd ⊢ ( 𝜑 → 𝐶 ≠ 𝐵 )
36 1 26 15 33 34 2 6 7 8 10 11 35 ragncol ⊢ ( 𝜑 → ¬ ( 𝐶 ∈ ( 𝐴 ( LineG ‘ 𝐺 ) 𝐵 ) ∨ 𝐴 = 𝐵 ) )
37 1 33 15 2 6 7 8 36 ncoltgdim2 ⊢ ( 𝜑 → 𝐺 DimTarskiG≥ 2 )
38 37 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑎 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑐 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → 𝐺 DimTarskiG≥ 2 )
39 9 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑎 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑐 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
40 10 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑎 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑐 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
41 1 26 15 33 34 17 21 22 23 40 ragcom ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑎 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑐 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → ⟨“ 𝐶 𝐵 𝐴 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
42 35 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑎 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑐 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → 𝐶 ≠ 𝐵 )
43 14 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑎 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑐 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → 𝑌 ≠ 𝑍 )
44 1 26 15 17 19 20 22 25 32 43 tgcgrneq ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑎 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑐 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → 𝐵 ≠ 𝑐 )
45 simplr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑎 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑐 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 )
46 1 15 16 25 23 22 17 33 45 hlln ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑎 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑐 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → 𝑐 ∈ ( 𝐶 ( LineG ‘ 𝐺 ) 𝐵 ) )
47 1 15 33 17 22 25 23 44 46 42 lnrot1 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑎 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑐 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → 𝐶 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝑐 ) )
48 47 orcd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑎 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑐 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → ( 𝐶 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝑐 ) ∨ 𝐵 = 𝑐 ) )
49 1 26 15 33 34 17 23 22 21 25 41 42 48 ragcol ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑎 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑐 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → ⟨“ 𝑐 𝐵 𝐴 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
50 1 26 15 33 34 17 25 22 21 49 ragcom ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑎 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑐 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → ⟨“ 𝐴 𝐵 𝑐 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
51 11 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑎 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑐 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → 𝐴 ≠ 𝐵 )
52 13 necomd ⊢ ( 𝜑 → 𝑌 ≠ 𝑋 )
53 52 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑎 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑐 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → 𝑌 ≠ 𝑋 )
54 1 26 15 17 19 18 22 24 29 53 tgcgrneq ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑎 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑐 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → 𝐵 ≠ 𝑎 )
55 simp-5r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑎 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑐 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 )
56 1 15 16 24 21 22 17 33 55 hlln ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑎 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑐 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → 𝑎 ∈ ( 𝐴 ( LineG ‘ 𝐺 ) 𝐵 ) )
57 1 15 33 17 22 24 21 54 56 51 lnrot1 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑎 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑐 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → 𝐴 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝑎 ) )
58 57 orcd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑎 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑐 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → ( 𝐴 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝑎 ) ∨ 𝐵 = 𝑎 ) )
59 1 26 15 33 34 17 21 22 25 24 50 51 58 ragcol ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑎 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑐 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → ⟨“ 𝑎 𝐵 𝑐 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
60 1 26 15 17 38 18 19 20 24 22 25 39 59 30 32 hypcgr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑎 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑐 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → ( 𝑋 ( dist ‘ 𝐺 ) 𝑍 ) = ( 𝑎 ( dist ‘ 𝐺 ) 𝑐 ) )
61 1 26 15 17 18 20 24 25 60 tgcgrcomlr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑎 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑐 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → ( 𝑍 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝑐 ( dist ‘ 𝐺 ) 𝑎 ) )
62 1 26 27 17 18 19 20 24 22 25 30 32 61 trgcgr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑎 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑐 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑎 𝐵 𝑐 ”⟩ )
63 1 15 16 17 18 19 20 21 22 23 24 25 62 55 45 iscgrad ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑎 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑐 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ )
64 63 anasss ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑎 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑐 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) ) → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ )
65 1 15 16 7 4 5 2 8 26 35 14 hlcgrex ⊢ ( 𝜑 → ∃ 𝑐 ∈ 𝑃 ( 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑐 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) )
66 65 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑎 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) → ∃ 𝑐 ∈ 𝑃 ( 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑐 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑍 ) ) )
67 64 66 r19.29a ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑎 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ )
68 67 anasss ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ ( 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑎 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) ) → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ )
69 1 15 16 7 4 3 2 6 26 11 52 hlcgrex ⊢ ( 𝜑 → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑎 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑋 ) ) )
70 68 69 r19.29a ⊢ ( 𝜑 → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ )