Metamath Proof Explorer


Theorem cgraid

Description: Angle congruence is reflexive. Theorem 11.6 of Schwabhauser p. 96. (Contributed by Thierry Arnoux, 31-Jul-2020)

Ref Expression
Hypotheses cgraid.p 𝑃 = ( Base ‘ 𝐺 )
cgraid.i 𝐼 = ( Itv ‘ 𝐺 )
cgraid.g ( 𝜑𝐺 ∈ TarskiG )
cgraid.k 𝐾 = ( hlG ‘ 𝐺 )
cgraid.a ( 𝜑𝐴𝑃 )
cgraid.b ( 𝜑𝐵𝑃 )
cgraid.c ( 𝜑𝐶𝑃 )
cgraid.1 ( 𝜑𝐴𝐵 )
cgraid.2 ( 𝜑𝐵𝐶 )
Assertion cgraid ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ )

Proof

Step Hyp Ref Expression
1 cgraid.p 𝑃 = ( Base ‘ 𝐺 )
2 cgraid.i 𝐼 = ( Itv ‘ 𝐺 )
3 cgraid.g ( 𝜑𝐺 ∈ TarskiG )
4 cgraid.k 𝐾 = ( hlG ‘ 𝐺 )
5 cgraid.a ( 𝜑𝐴𝑃 )
6 cgraid.b ( 𝜑𝐵𝑃 )
7 cgraid.c ( 𝜑𝐶𝑃 )
8 cgraid.1 ( 𝜑𝐴𝐵 )
9 cgraid.2 ( 𝜑𝐵𝐶 )
10 eqid ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
11 eqid ( cgrG ‘ 𝐺 ) = ( cgrG ‘ 𝐺 )
12 1 10 2 11 3 5 6 7 cgr3id ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ )
13 1 2 4 5 5 6 3 8 hlid ( 𝜑𝐴 ( 𝐾𝐵 ) 𝐴 )
14 9 necomd ( 𝜑𝐶𝐵 )
15 1 2 4 7 5 6 3 14 hlid ( 𝜑𝐶 ( 𝐾𝐵 ) 𝐶 )
16 1 2 4 3 5 6 7 5 6 7 5 7 12 13 15 iscgrad ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ )