Theorem iseqlgd

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

	Ref	Expression
Hypotheses	iseqlg.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	iseqlg.m	⊢ − = ( dist ‘ 𝐺 )
	iseqlg.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	iseqlg.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	iseqlg.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	iseqlg.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
	iseqlg.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
	iseqlg.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
	iseqlgd.1	⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = ( 𝐵 − 𝐶 ) )
	iseqlgd.2	⊢ ( 𝜑 → ( 𝐵 − 𝐶 ) = ( 𝐶 − 𝐴 ) )
	iseqlgd.3	⊢ ( 𝜑 → ( 𝐶 − 𝐴 ) = ( 𝐴 − 𝐵 ) )
Assertion	iseqlgd	⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( eqltrG ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		iseqlg.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		iseqlg.m	⊢ − = ( dist ‘ 𝐺 )
3		iseqlg.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
4		iseqlg.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
5		iseqlg.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
6		iseqlg.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
7		iseqlg.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
8		iseqlg.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
9		iseqlgd.1	⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = ( 𝐵 − 𝐶 ) )
10		iseqlgd.2	⊢ ( 𝜑 → ( 𝐵 − 𝐶 ) = ( 𝐶 − 𝐴 ) )
11		iseqlgd.3	⊢ ( 𝜑 → ( 𝐶 − 𝐴 ) = ( 𝐴 − 𝐵 ) )
12		eqid	⊢ ( cgrG ‘ 𝐺 ) = ( cgrG ‘ 𝐺 )
13	1 2 12 5 6 7 8 7 8 6 9 10 11	trgcgr	⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐵 𝐶 𝐴 ”⟩ )
14	1 2 3 4 5 6 7 8	iseqlg	⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( eqltrG ‘ 𝐺 ) ↔ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐵 𝐶 𝐴 ”⟩ ) )
15	13 14	mpbird	⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( eqltrG ‘ 𝐺 ) )