Theorem tgasa

Description: Second congruence theorem: ASA. (Angle-Side-Angle): If two pairs of angles of two triangles are equal in measurement, and the included sides are equal in length, then the triangles are congruent. Theorem 11.50 of Schwabhauser p. 108. (Contributed by Thierry Arnoux, 15-Aug-2020)

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

Proof

Step	Hyp	Ref	Expression
1		tgsas.p	|- P = ( Base ` G )
2		tgsas.m	|- .- = ( dist ` G )
3		tgsas.i	|- I = ( Itv ` G )
4		tgsas.g	|- ( ph -> G e. TarskiG )
5		tgsas.a	|- ( ph -> A e. P )
6		tgsas.b	|- ( ph -> B e. P )
7		tgsas.c	|- ( ph -> C e. P )
8		tgsas.d	|- ( ph -> D e. P )
9		tgsas.e	|- ( ph -> E e. P )
10		tgsas.f	|- ( ph -> F e. P )
11		tgasa.l	|- L = ( LineG ` G )
12		tgasa.1	|- ( ph -> -. ( C e. ( A L B ) \/ A = B ) )
13		tgasa.2	|- ( ph -> ( A .- B ) = ( D .- E ) )
14		tgasa.3	|- ( ph -> <" A B C "> ( cgrA ` G ) <" D E F "> )
15		tgasa.4	|- ( ph -> <" C A B "> ( cgrA ` G ) <" F D E "> )
16	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	tgasa1	|- ( ph -> ( B .- C ) = ( E .- F ) )
17	1 2 3 4 5 6 7 8 9 10 13 14 16	tgsas	|- ( ph -> <" A B C "> ( cgrG ` G ) <" D E F "> )