Theorem tgsas

Description: First congruence theorem: SAS (Side-Angle-Side): If two pairs of sides of two triangles are equal in length, and the included angles are equal in measurement, then the triangles are congruent. Theorem 11.49 of Schwabhauser p. 107. (Contributed by Thierry Arnoux, 1-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 )
	tgsas.1	|- ( ph -> ( A .- B ) = ( D .- E ) )
	tgsas.2	|- ( ph -> <" A B C "> ( cgrA ` G ) <" D E F "> )
	tgsas.3	|- ( ph -> ( B .- C ) = ( E .- F ) )
Assertion	tgsas	|- ( 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		tgsas.1	|- ( ph -> ( A .- B ) = ( D .- E ) )
12		tgsas.2	|- ( ph -> <" A B C "> ( cgrA ` G ) <" D E F "> )
13		tgsas.3	|- ( ph -> ( B .- C ) = ( E .- F ) )
14		eqid	|- ( cgrG ` G ) = ( cgrG ` G )
15	1 2 3 4 5 6 7 8 9 10 11 12 13	tgsas1	|- ( ph -> ( C .- A ) = ( F .- D ) )
16	1 2 14 4 5 6 7 8 9 10 11 13 15	trgcgr	|- ( ph -> <" A B C "> ( cgrG ` G ) <" D E F "> )