Theorem iseqlgd

Description: Condition for a triangle to be equilateral. (Contributed by Thierry Arnoux, 5-Oct-2020)

	Ref	Expression
Hypotheses	iseqlg.p	|- P = ( Base ` G )
	iseqlg.m	|- .- = ( dist ` G )
	iseqlg.i	|- I = ( Itv ` G )
	iseqlg.l	|- L = ( LineG ` G )
	iseqlg.g	|- ( ph -> G e. TarskiG )
	iseqlg.a	|- ( ph -> A e. P )
	iseqlg.b	|- ( ph -> B e. P )
	iseqlg.c	|- ( ph -> C e. P )
	iseqlgd.1	|- ( ph -> ( A .- B ) = ( B .- C ) )
	iseqlgd.2	|- ( ph -> ( B .- C ) = ( C .- A ) )
	iseqlgd.3	|- ( ph -> ( C .- A ) = ( A .- B ) )
Assertion	iseqlgd	|- ( ph -> <" A B C "> e. ( eqltrG ` G ) )

Proof

Step	Hyp	Ref	Expression
1		iseqlg.p	|- P = ( Base ` G )
2		iseqlg.m	|- .- = ( dist ` G )
3		iseqlg.i	|- I = ( Itv ` G )
4		iseqlg.l	|- L = ( LineG ` G )
5		iseqlg.g	|- ( ph -> G e. TarskiG )
6		iseqlg.a	|- ( ph -> A e. P )
7		iseqlg.b	|- ( ph -> B e. P )
8		iseqlg.c	|- ( ph -> C e. P )
9		iseqlgd.1	|- ( ph -> ( A .- B ) = ( B .- C ) )
10		iseqlgd.2	|- ( ph -> ( B .- C ) = ( C .- A ) )
11		iseqlgd.3	|- ( ph -> ( C .- A ) = ( A .- B ) )
12		eqid	|- ( cgrG ` G ) = ( cgrG ` G )
13	1 2 12 5 6 7 8 7 8 6 9 10 11	trgcgr	|- ( ph -> <" A B C "> ( cgrG ` G ) <" B C A "> )
14	1 2 3 4 5 6 7 8	iseqlg	|- ( ph -> ( <" A B C "> e. ( eqltrG ` G ) <-> <" A B C "> ( cgrG ` G ) <" B C A "> ) )
15	13 14	mpbird	|- ( ph -> <" A B C "> e. ( eqltrG ` G ) )