Theorem tgsss3

Description: Third congruence theorem: SSS. Theorem 11.51 of Schwabhauser p. 109. (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 )
	tgsss.1	|- ( ph -> ( A .- B ) = ( D .- E ) )
	tgsss.2	|- ( ph -> ( B .- C ) = ( E .- F ) )
	tgsss.3	|- ( ph -> ( C .- A ) = ( F .- D ) )
	tgsss.4	|- ( ph -> A =/= B )
	tgsss.5	|- ( ph -> B =/= C )
	tgsss.6	|- ( ph -> C =/= A )
Assertion	tgsss3	|- ( ph -> <" B C A "> ( cgrA ` G ) <" E F D "> )

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		tgsss.1	|- ( ph -> ( A .- B ) = ( D .- E ) )
12		tgsss.2	|- ( ph -> ( B .- C ) = ( E .- F ) )
13		tgsss.3	|- ( ph -> ( C .- A ) = ( F .- D ) )
14		tgsss.4	|- ( ph -> A =/= B )
15		tgsss.5	|- ( ph -> B =/= C )
16		tgsss.6	|- ( ph -> C =/= A )
17	1 2 3 4 6 7 5 9 10 8 12 13 11 15 16 14	tgsss1	|- ( ph -> <" B C A "> ( cgrA ` G ) <" E F D "> )