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 ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )