Metamath Proof Explorer


Theorem cgrcgra

Description: Triangle congruence implies angle congruence. This is a portion of CPCTC, focusing on a specific angle. (Contributed by Arnoux, 2-Aug-2020)

Ref Expression
Hypotheses cgraid.p 𝑃 = ( Base ‘ 𝐺 )
cgraid.i 𝐼 = ( Itv ‘ 𝐺 )
cgraid.g ( 𝜑𝐺 ∈ TarskiG )
cgraid.k 𝐾 = ( hlG ‘ 𝐺 )
cgraid.a ( 𝜑𝐴𝑃 )
cgraid.b ( 𝜑𝐵𝑃 )
cgraid.c ( 𝜑𝐶𝑃 )
cgracom.d ( 𝜑𝐷𝑃 )
cgracom.e ( 𝜑𝐸𝑃 )
cgracom.f ( 𝜑𝐹𝑃 )
cgrcgra.1 ( 𝜑𝐴𝐵 )
cgrcgra.2 ( 𝜑𝐵𝐶 )
cgrcgra.3 ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
Assertion cgrcgra ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( 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 cgracom.d ( 𝜑𝐷𝑃 )
9 cgracom.e ( 𝜑𝐸𝑃 )
10 cgracom.f ( 𝜑𝐹𝑃 )
11 cgrcgra.1 ( 𝜑𝐴𝐵 )
12 cgrcgra.2 ( 𝜑𝐵𝐶 )
13 cgrcgra.3 ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
14 eqid ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
15 eqid ( cgrG ‘ 𝐺 ) = ( cgrG ‘ 𝐺 )
16 1 14 2 15 3 5 6 7 8 9 10 13 cgr3simp1 ( 𝜑 → ( 𝐴 ( dist ‘ 𝐺 ) 𝐵 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐸 ) )
17 1 14 2 3 5 6 8 9 16 11 tgcgrneq ( 𝜑𝐷𝐸 )
18 1 2 4 8 5 9 3 17 hlid ( 𝜑𝐷 ( 𝐾𝐸 ) 𝐷 )
19 1 14 2 15 3 5 6 7 8 9 10 13 cgr3simp2 ( 𝜑 → ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐹 ) )
20 1 14 2 3 6 7 9 10 19 tgcgrcomlr ( 𝜑 → ( 𝐶 ( dist ‘ 𝐺 ) 𝐵 ) = ( 𝐹 ( dist ‘ 𝐺 ) 𝐸 ) )
21 12 necomd ( 𝜑𝐶𝐵 )
22 1 14 2 3 7 6 10 9 20 21 tgcgrneq ( 𝜑𝐹𝐸 )
23 1 2 4 10 5 9 3 22 hlid ( 𝜑𝐹 ( 𝐾𝐸 ) 𝐹 )
24 1 2 4 3 5 6 7 8 9 10 8 10 13 18 23 iscgrad ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )