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 
|- P = ( Base ` G )
tgaascgra.m 
|- .- = ( dist ` G )
tgaascgra.i 
|- I = ( Itv ` G )
tgaascgra.l 
|- L = ( LineG ` G )
tgaascgra.k 
|- K = ( hlG ` G )
tgaascgra.g 
|- ( ph -> G e. TarskiG )
tgaascgra.a 
|- ( ph -> A e. P )
tgaascgra.b 
|- ( ph -> B e. P )
tgaascgra.c 
|- ( ph -> C e. P )
tgaascgra.d 
|- ( ph -> D e. P )
tgaascgra.e 
|- ( ph -> E e. P )
tgaascgra.f 
|- ( ph -> F e. P )
tgaascgra.h 
|- ( ph -> H e. P )
tgaascgra.ncol 
|- ( ph -> -. ( C e. ( A L B ) \/ A = B ) )
tgaascgra.1 
|- ( ph -> ( A .- B ) = ( D .- E ) )
tgaascgra.2 
|- ( ph -> <" A B C "> ( cgrA ` G ) <" D E F "> )
tgaascgra.3 
|- ( ph -> <" B C A "> ( cgrA ` G ) <" E F D "> )
tgaascgra.4 
|- ( ph -> H ( K ` E ) F )
tgaascgra.5 
|- ( ph -> ( E .- H ) = ( B .- C ) )
Assertion tgaascgra 
|- ( ph -> <" D F E "> ( cgrA ` G ) <" D H E "> )

Proof

Step Hyp Ref Expression
1 tgaascgra.p 
 |-  P = ( Base ` G )
2 tgaascgra.m 
 |-  .- = ( dist ` G )
3 tgaascgra.i 
 |-  I = ( Itv ` G )
4 tgaascgra.l 
 |-  L = ( LineG ` G )
5 tgaascgra.k 
 |-  K = ( hlG ` G )
6 tgaascgra.g 
 |-  ( ph -> G e. TarskiG )
7 tgaascgra.a 
 |-  ( ph -> A e. P )
8 tgaascgra.b 
 |-  ( ph -> B e. P )
9 tgaascgra.c 
 |-  ( ph -> C e. P )
10 tgaascgra.d 
 |-  ( ph -> D e. P )
11 tgaascgra.e 
 |-  ( ph -> E e. P )
12 tgaascgra.f 
 |-  ( ph -> F e. P )
13 tgaascgra.h 
 |-  ( ph -> H e. P )
14 tgaascgra.ncol 
 |-  ( ph -> -. ( C e. ( A L B ) \/ A = B ) )
15 tgaascgra.1 
 |-  ( ph -> ( A .- B ) = ( D .- E ) )
16 tgaascgra.2 
 |-  ( ph -> <" A B C "> ( cgrA ` G ) <" D E F "> )
17 tgaascgra.3 
 |-  ( ph -> <" B C A "> ( cgrA ` G ) <" E F D "> )
18 tgaascgra.4 
 |-  ( ph -> H ( K ` E ) F )
19 tgaascgra.5 
 |-  ( ph -> ( E .- H ) = ( B .- C ) )
20 1 3 6 5 8 9 7 11 12 10 17 cgracom 
 |-  ( ph -> <" E F D "> ( cgrA ` G ) <" B C A "> )
21 1 3 4 6 7 8 9 14 tgbcne 
 |-  ( ph -> B =/= C )
22 1 3 4 6 7 8 9 14 tgacne 
 |-  ( ph -> A =/= C )
23 22 necomd 
 |-  ( ph -> C =/= A )
24 eqid 
 |-  ( cgrG ` G ) = ( cgrG ` G )
25 19 eqcomd 
 |-  ( ph -> ( B .- C ) = ( E .- H ) )
26 1 3 5 6 7 8 9 10 11 12 16 13 18 cgrahl2 
 |-  ( ph -> <" A B C "> ( cgrA ` G ) <" D E H "> )
27 1 2 3 6 7 8 9 10 11 13 15 26 25 tgsas 
 |-  ( ph -> <" A B C "> ( cgrG ` G ) <" D E H "> )
28 1 2 3 24 6 7 8 9 10 11 13 27 cgr3simp3 
 |-  ( ph -> ( C .- A ) = ( H .- D ) )
29 1 2 24 6 8 9 7 11 13 10 25 28 15 trgcgr 
 |-  ( ph -> <" B C A "> ( cgrG ` G ) <" E H D "> )
30 1 3 6 5 8 9 7 11 13 10 21 23 29 cgrcgra 
 |-  ( ph -> <" B C A "> ( cgrA ` G ) <" E H D "> )
31 1 3 6 5 11 12 10 8 9 7 20 11 13 10 30 cgratr 
 |-  ( ph -> <" E F D "> ( cgrA ` G ) <" E H D "> )
32 1 3 2 6 11 12 10 11 13 10 31 cgraswaplr 
 |-  ( ph -> <" D F E "> ( cgrA ` G ) <" D H E "> )