Metamath Proof Explorer

Theorem tgaas1

Description: Under the AAS hypotheses, the side included between the two given angles is congruent. This is the whole content of AAS: tgaas simply packages it with SAS ( tgsas ). The point copied onto ray E F by tgaascgra is eliminated here. (Contributed by JAG, 12-Aug-2026)

Ref Expression
Hypotheses tgaas1.p 
|- P = ( Base ` G )
tgaas1.m 
|- .- = ( dist ` G )
tgaas1.i 
|- I = ( Itv ` G )
tgaas1.l 
|- L = ( LineG ` G )
tgaas1.g 
|- ( ph -> G e. TarskiG )
tgaas1.a 
|- ( ph -> A e. P )
tgaas1.b 
|- ( ph -> B e. P )
tgaas1.c 
|- ( ph -> C e. P )
tgaas1.d 
|- ( ph -> D e. P )
tgaas1.e 
|- ( ph -> E e. P )
tgaas1.f 
|- ( ph -> F e. P )
tgaas1.ncol 
|- ( ph -> -. ( C e. ( A L B ) \/ A = B ) )
tgaas1.1 
|- ( ph -> ( A .- B ) = ( D .- E ) )
tgaas1.2 
|- ( ph -> <" A B C "> ( cgrA ` G ) <" D E F "> )
tgaas1.3 
|- ( ph -> <" B C A "> ( cgrA ` G ) <" E F D "> )
Assertion tgaas1 
|- ( ph -> ( B .- C ) = ( E .- F ) )

Proof

Step Hyp Ref Expression
1 tgaas1.p 
 |-  P = ( Base ` G )
2 tgaas1.m 
 |-  .- = ( dist ` G )
3 tgaas1.i 
 |-  I = ( Itv ` G )
4 tgaas1.l 
 |-  L = ( LineG ` G )
5 tgaas1.g 
 |-  ( ph -> G e. TarskiG )
6 tgaas1.a 
 |-  ( ph -> A e. P )
7 tgaas1.b 
 |-  ( ph -> B e. P )
8 tgaas1.c 
 |-  ( ph -> C e. P )
9 tgaas1.d 
 |-  ( ph -> D e. P )
10 tgaas1.e 
 |-  ( ph -> E e. P )
11 tgaas1.f 
 |-  ( ph -> F e. P )
12 tgaas1.ncol 
 |-  ( ph -> -. ( C e. ( A L B ) \/ A = B ) )
13 tgaas1.1 
 |-  ( ph -> ( A .- B ) = ( D .- E ) )
14 tgaas1.2 
 |-  ( ph -> <" A B C "> ( cgrA ` G ) <" D E F "> )
15 tgaas1.3 
 |-  ( ph -> <" B C A "> ( cgrA ` G ) <" E F D "> )
16 eqid 
 |-  ( hlG ` G ) = ( hlG ` G )
17 5 adantr 
 |-  ( ( ph /\ x e. P ) -> G e. TarskiG )
18 17 adantr 
 |-  ( ( ( ph /\ x e. P ) /\ ( x ( ( hlG ` G ) ` E ) F /\ ( E .- x ) = ( B .- C ) ) ) -> G e. TarskiG )
19 6 adantr 
 |-  ( ( ph /\ x e. P ) -> A e. P )
20 19 adantr 
 |-  ( ( ( ph /\ x e. P ) /\ ( x ( ( hlG ` G ) ` E ) F /\ ( E .- x ) = ( B .- C ) ) ) -> A e. P )
21 7 adantr 
 |-  ( ( ph /\ x e. P ) -> B e. P )
22 21 adantr 
 |-  ( ( ( ph /\ x e. P ) /\ ( x ( ( hlG ` G ) ` E ) F /\ ( E .- x ) = ( B .- C ) ) ) -> B e. P )
23 8 adantr 
 |-  ( ( ph /\ x e. P ) -> C e. P )
24 23 adantr 
 |-  ( ( ( ph /\ x e. P ) /\ ( x ( ( hlG ` G ) ` E ) F /\ ( E .- x ) = ( B .- C ) ) ) -> C e. P )
25 9 adantr 
 |-  ( ( ph /\ x e. P ) -> D e. P )
26 25 adantr 
 |-  ( ( ( ph /\ x e. P ) /\ ( x ( ( hlG ` G ) ` E ) F /\ ( E .- x ) = ( B .- C ) ) ) -> D e. P )
27 10 adantr 
 |-  ( ( ph /\ x e. P ) -> E e. P )
28 27 adantr 
 |-  ( ( ( ph /\ x e. P ) /\ ( x ( ( hlG ` G ) ` E ) F /\ ( E .- x ) = ( B .- C ) ) ) -> E e. P )
29 11 adantr 
 |-  ( ( ph /\ x e. P ) -> F e. P )
30 29 adantr 
 |-  ( ( ( ph /\ x e. P ) /\ ( x ( ( hlG ` G ) ` E ) F /\ ( E .- x ) = ( B .- C ) ) ) -> F e. P )
31 simpl 
 |-  ( ( ( ph /\ x e. P ) /\ ( x ( ( hlG ` G ) ` E ) F /\ ( E .- x ) = ( B .- C ) ) ) -> ( ph /\ x e. P ) )
32 31 simprd 
 |-  ( ( ( ph /\ x e. P ) /\ ( x ( ( hlG ` G ) ` E ) F /\ ( E .- x ) = ( B .- C ) ) ) -> x e. P )
33 12 adantr 
 |-  ( ( ph /\ x e. P ) -> -. ( C e. ( A L B ) \/ A = B ) )
34 33 adantr 
 |-  ( ( ( ph /\ x e. P ) /\ ( x ( ( hlG ` G ) ` E ) F /\ ( E .- x ) = ( B .- C ) ) ) -> -. ( C e. ( A L B ) \/ A = B ) )
35 13 adantr 
 |-  ( ( ph /\ x e. P ) -> ( A .- B ) = ( D .- E ) )
36 35 adantr 
 |-  ( ( ( ph /\ x e. P ) /\ ( x ( ( hlG ` G ) ` E ) F /\ ( E .- x ) = ( B .- C ) ) ) -> ( A .- B ) = ( D .- E ) )
37 14 adantr 
 |-  ( ( ph /\ x e. P ) -> <" A B C "> ( cgrA ` G ) <" D E F "> )
38 37 adantr 
 |-  ( ( ( ph /\ x e. P ) /\ ( x ( ( hlG ` G ) ` E ) F /\ ( E .- x ) = ( B .- C ) ) ) -> <" A B C "> ( cgrA ` G ) <" D E F "> )
39 15 adantr 
 |-  ( ( ph /\ x e. P ) -> <" B C A "> ( cgrA ` G ) <" E F D "> )
40 39 adantr 
 |-  ( ( ( ph /\ x e. P ) /\ ( x ( ( hlG ` G ) ` E ) F /\ ( E .- x ) = ( B .- C ) ) ) -> <" B C A "> ( cgrA ` G ) <" E F D "> )
41 simpr 
 |-  ( ( ( ph /\ x e. P ) /\ ( x ( ( hlG ` G ) ` E ) F /\ ( E .- x ) = ( B .- C ) ) ) -> ( x ( ( hlG ` G ) ` E ) F /\ ( E .- x ) = ( B .- C ) ) )
42 41 simpld 
 |-  ( ( ( ph /\ x e. P ) /\ ( x ( ( hlG ` G ) ` E ) F /\ ( E .- x ) = ( B .- C ) ) ) -> x ( ( hlG ` G ) ` E ) F )
43 41 simprd 
 |-  ( ( ( ph /\ x e. P ) /\ ( x ( ( hlG ` G ) ` E ) F /\ ( E .- x ) = ( B .- C ) ) ) -> ( E .- x ) = ( B .- C ) )
44 1 2 3 4 16 18 20 22 24 26 28 30 32 34 36 38 40 42 43 tgaas1h 
 |-  ( ( ( ph /\ x e. P ) /\ ( x ( ( hlG ` G ) ` E ) F /\ ( E .- x ) = ( B .- C ) ) ) -> ( B .- C ) = ( E .- F ) )
45 1 3 2 5 6 7 8 9 10 11 14 4 12 cgrancol 
 |-  ( ph -> -. ( F e. ( D L E ) \/ D = E ) )
46 1 3 4 5 9 10 11 45 tgbcne 
 |-  ( ph -> E =/= F )
47 46 necomd 
 |-  ( ph -> F =/= E )
48 1 3 4 5 6 7 8 12 tgbcne 
 |-  ( ph -> B =/= C )
49 1 3 16 10 7 8 5 11 2 47 48 hlcgrex 
 |-  ( ph -> E. x e. P ( x ( ( hlG ` G ) ` E ) F /\ ( E .- x ) = ( B .- C ) ) )
50 44 49 r19.29a 
 |-  ( ph -> ( B .- C ) = ( E .- F ) )