Metamath Proof Explorer

Theorem tgaascgra

Description: The comparison triangle of the AAS route: with H placed on ray E F at distance B C from E , the triangle D E H is congruent to A B C ( cgrahl2 then tgsas ), so its angle at H can be read off ( cgrcgra ) and matched against the given angle at F . The result is the angle congruence the case split of tgaas1h consumes. (Contributed by JAG, 12-Aug-2026)

Ref Expression
Hypotheses tgaascgra.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
tgaascgra.m ⊢ − = ( dist ‘ 𝐺 )
tgaascgra.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
tgaascgra.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
tgaascgra.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
tgaascgra.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
tgaascgra.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
tgaascgra.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
tgaascgra.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
tgaascgra.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
tgaascgra.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
tgaascgra.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
tgaascgra.h ⊢ ( 𝜑 → 𝐻 ∈ 𝑃 )
tgaascgra.ncol ⊢ ( 𝜑 → ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
tgaascgra.1 ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = ( 𝐷 − 𝐸 ) )
tgaascgra.2 ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
tgaascgra.3 ⊢ ( 𝜑 → ⟨“ 𝐵 𝐶 𝐴 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐸 𝐹 𝐷 ”⟩ )
tgaascgra.4 ⊢ ( 𝜑 → 𝐻 ( 𝐾 ‘ 𝐸 ) 𝐹 )
tgaascgra.5 ⊢ ( 𝜑 → ( 𝐸 − 𝐻 ) = ( 𝐵 − 𝐶 ) )
Assertion tgaascgra ( 𝜑 → ⟨“ 𝐷 𝐹 𝐸 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐻 𝐸 ”⟩ )

Proof

Step Hyp Ref Expression
1 tgaascgra.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 tgaascgra.m ⊢ − = ( dist ‘ 𝐺 )
3 tgaascgra.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 tgaascgra.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
5 tgaascgra.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
6 tgaascgra.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
7 tgaascgra.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
8 tgaascgra.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
9 tgaascgra.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
10 tgaascgra.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
11 tgaascgra.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
12 tgaascgra.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
13 tgaascgra.h ⊢ ( 𝜑 → 𝐻 ∈ 𝑃 )
14 tgaascgra.ncol ⊢ ( 𝜑 → ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
15 tgaascgra.1 ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = ( 𝐷 − 𝐸 ) )
16 tgaascgra.2 ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
17 tgaascgra.3 ⊢ ( 𝜑 → ⟨“ 𝐵 𝐶 𝐴 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐸 𝐹 𝐷 ”⟩ )
18 tgaascgra.4 ⊢ ( 𝜑 → 𝐻 ( 𝐾 ‘ 𝐸 ) 𝐹 )
19 tgaascgra.5 ⊢ ( 𝜑 → ( 𝐸 − 𝐻 ) = ( 𝐵 − 𝐶 ) )
20 1 3 6 5 8 9 7 11 12 10 17 cgracom ⊢ ( 𝜑 → ⟨“ 𝐸 𝐹 𝐷 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐵 𝐶 𝐴 ”⟩ )
21 1 3 4 6 7 8 9 14 tgbcne ⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
22 1 3 4 6 7 8 9 14 tgacne ⊢ ( 𝜑 → 𝐴 ≠ 𝐶 )
23 22 necomd ⊢ ( 𝜑 → 𝐶 ≠ 𝐴 )
24 eqid ⊢ ( cgrG ‘ 𝐺 ) = ( cgrG ‘ 𝐺 )
25 19 eqcomd ⊢ ( 𝜑 → ( 𝐵 − 𝐶 ) = ( 𝐸 − 𝐻 ) )
26 1 3 5 6 7 8 9 10 11 12 16 13 18 cgrahl2 ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐻 ”⟩ )
27 1 2 3 6 7 8 9 10 11 13 15 26 25 tgsas ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐻 ”⟩ )
28 1 2 3 24 6 7 8 9 10 11 13 27 cgr3simp3 ⊢ ( 𝜑 → ( 𝐶 − 𝐴 ) = ( 𝐻 − 𝐷 ) )
29 1 2 24 6 8 9 7 11 13 10 25 28 15 trgcgr ⊢ ( 𝜑 → ⟨“ 𝐵 𝐶 𝐴 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐻 𝐷 ”⟩ )
30 1 3 6 5 8 9 7 11 13 10 21 23 29 cgrcgra ⊢ ( 𝜑 → ⟨“ 𝐵 𝐶 𝐴 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐸 𝐻 𝐷 ”⟩ )
31 1 3 6 5 11 12 10 8 9 7 20 11 13 10 30 cgratr ⊢ ( 𝜑 → ⟨“ 𝐸 𝐹 𝐷 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐸 𝐻 𝐷 ”⟩ )
32 1 3 2 6 11 12 10 11 13 10 31 cgraswaplr ⊢ ( 𝜑 → ⟨“ 𝐷 𝐹 𝐸 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐻 𝐸 ”⟩ )