Metamath Proof Explorer

Theorem cgrarag

Description: Any angle <" A B C "> congruent with a right angle <" X Y Z "> is a right angle. Theorem 11.17 of Schwabhauser p. 98. (Contributed by Thierry Arnoux, 13-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 ‘ 𝐺 ) )
cgrarag.1 ⊢ ( 𝜑 → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ )
Assertion cgrarag ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )

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 cgrarag.1 ⊢ ( 𝜑 → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ )
11 eqid ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
12 eqid ⊢ ( Itv ‘ 𝐺 ) = ( Itv ‘ 𝐺 )
13 eqid ⊢ ( LineG ‘ 𝐺 ) = ( LineG ‘ 𝐺 )
14 eqid ⊢ ( pInvG ‘ 𝐺 ) = ( pInvG ‘ 𝐺 )
15 2 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑎 𝐵 𝑐 ”⟩ ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) → 𝐺 ∈ TarskiG )
16 simp-5r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑎 𝐵 𝑐 ”⟩ ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) → 𝑎 ∈ 𝑃 )
17 7 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑎 𝐵 𝑐 ”⟩ ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) → 𝐵 ∈ 𝑃 )
18 8 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑎 𝐵 𝑐 ”⟩ ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) → 𝐶 ∈ 𝑃 )
19 6 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑎 𝐵 𝑐 ”⟩ ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) → 𝐴 ∈ 𝑃 )
20 simp-4r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑎 𝐵 𝑐 ”⟩ ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) → 𝑐 ∈ 𝑃 )
21 3 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑎 𝐵 𝑐 ”⟩ ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) → 𝑋 ∈ 𝑃 )
22 4 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑎 𝐵 𝑐 ”⟩ ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) → 𝑌 ∈ 𝑃 )
23 5 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑎 𝐵 𝑐 ”⟩ ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) → 𝑍 ∈ 𝑃 )
24 eqid ⊢ ( cgrG ‘ 𝐺 ) = ( cgrG ‘ 𝐺 )
25 9 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑎 𝐵 𝑐 ”⟩ ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
26 simpllr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑎 𝐵 𝑐 ”⟩ ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑎 𝐵 𝑐 ”⟩ )
27 1 11 12 13 14 15 21 22 23 24 16 17 20 25 26 ragcgr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑎 𝐵 𝑐 ”⟩ ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) → ⟨“ 𝑎 𝐵 𝑐 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
28 1 11 12 13 14 15 16 17 20 27 ragcom ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑎 𝐵 𝑐 ”⟩ ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) → ⟨“ 𝑐 𝐵 𝑎 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
29 eqid ⊢ ( hlG ‘ 𝐺 ) = ( hlG ‘ 𝐺 )
30 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑎 𝐵 𝑐 ”⟩ ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) → 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 )
31 1 12 29 20 18 17 15 30 hlne1 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑎 𝐵 𝑐 ”⟩ ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) → 𝑐 ≠ 𝐵 )
32 1 12 29 20 18 17 15 30 hlcomd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑎 𝐵 𝑐 ”⟩ ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) → 𝐶 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝑐 )
33 1 12 29 18 20 17 15 13 32 hlln ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑎 𝐵 𝑐 ”⟩ ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) → 𝐶 ∈ ( 𝑐 ( LineG ‘ 𝐺 ) 𝐵 ) )
34 33 orcd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑎 𝐵 𝑐 ”⟩ ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) → ( 𝐶 ∈ ( 𝑐 ( LineG ‘ 𝐺 ) 𝐵 ) ∨ 𝑐 = 𝐵 ) )
35 1 13 12 15 20 17 18 34 colrot1 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑎 𝐵 𝑐 ”⟩ ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) → ( 𝑐 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐶 ) ∨ 𝐵 = 𝐶 ) )
36 1 11 12 13 14 15 20 17 16 18 28 31 35 ragcol ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑎 𝐵 𝑐 ”⟩ ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) → ⟨“ 𝐶 𝐵 𝑎 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
37 1 11 12 13 14 15 18 17 16 36 ragcom ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑎 𝐵 𝑐 ”⟩ ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) → ⟨“ 𝑎 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
38 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑎 𝐵 𝑐 ”⟩ ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) → 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 )
39 1 12 29 16 19 17 15 38 hlne1 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑎 𝐵 𝑐 ”⟩ ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) → 𝑎 ≠ 𝐵 )
40 1 12 29 16 19 17 15 38 hlcomd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑎 𝐵 𝑐 ”⟩ ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) → 𝐴 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝑎 )
41 1 12 29 19 16 17 15 13 40 hlln ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑎 𝐵 𝑐 ”⟩ ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) → 𝐴 ∈ ( 𝑎 ( LineG ‘ 𝐺 ) 𝐵 ) )
42 41 orcd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑎 𝐵 𝑐 ”⟩ ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) → ( 𝐴 ∈ ( 𝑎 ( LineG ‘ 𝐺 ) 𝐵 ) ∨ 𝑎 = 𝐵 ) )
43 1 13 12 15 16 17 19 42 colrot1 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑎 𝐵 𝑐 ”⟩ ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) → ( 𝑎 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐴 ) ∨ 𝐵 = 𝐴 ) )
44 1 11 12 13 14 15 16 17 18 19 37 39 43 ragcol ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑎 𝐵 𝑐 ”⟩ ) ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
45 44 3anasss ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑎 𝐵 𝑐 ”⟩ ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
46 1 12 29 2 3 4 5 6 7 8 iscgra ⊢ ( 𝜑 → ( ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ ↔ ∃ 𝑎 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ( ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑎 𝐵 𝑐 ”⟩ ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) ) )
47 10 46 mpbid ⊢ ( 𝜑 → ∃ 𝑎 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ( ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑎 𝐵 𝑐 ”⟩ ∧ 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ∧ 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) )
48 45 47 r19.29vva ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )