Theorem tgsas2

Description: First congruence theorem: SAS. 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 ) )
	tgsas2.4	|- ( ph -> A =/= C )
Assertion	tgsas2	|- ( ph -> <" C A B "> ( cgrA ` G ) <" F D E "> )

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		tgsas2.4	|- ( ph -> A =/= C )
15		eqid	|- ( hlG ` G ) = ( hlG ` G )
16		eqid	|- ( cgrG ` G ) = ( cgrG ` G )
17	1 2 3 4 5 6 7 8 9 10 11 12 13	tgsas	|- ( ph -> <" A B C "> ( cgrG ` G ) <" D E F "> )
18	1 2 3 16 4 5 6 7 8 9 10 17	cgr3rotr	|- ( ph -> <" C A B "> ( cgrG ` G ) <" F D E "> )
19	1 2 3 4 5 6 7 8 9 10 11 12 13	tgsas1	|- ( ph -> ( C .- A ) = ( F .- D ) )
20	14	necomd	|- ( ph -> C =/= A )
21	1 2 3 4 7 5 10 8 19 20	tgcgrneq	|- ( ph -> F =/= D )
22	1 3 15 10 5 8 4 21	hlid	|- ( ph -> F ( ( hlG ` G ) ` D ) F )
23	1 3 15 4 5 6 7 8 9 10 12	cgrane3	|- ( ph -> E =/= D )
24	1 3 15 9 5 8 4 23	hlid	|- ( ph -> E ( ( hlG ` G ) ` D ) E )
25	1 3 15 4 7 5 6 10 8 9 10 9 18 22 24	iscgrad	|- ( ph -> <" C A B "> ( cgrA ` G ) <" F D E "> )