Theorem legeq

Description: Deduce equality from "less than" null segments. (Contributed by Thierry Arnoux, 12-Aug-2019)

	Ref	Expression
Hypotheses	legval.p	|- P = ( Base ` G )
	legval.d	|- .- = ( dist ` G )
	legval.i	|- I = ( Itv ` G )
	legval.l	|- .<_ = ( leG ` G )
	legval.g	|- ( ph -> G e. TarskiG )
	legid.a	|- ( ph -> A e. P )
	legid.b	|- ( ph -> B e. P )
	legtrd.c	|- ( ph -> C e. P )
	legtrd.d	|- ( ph -> D e. P )
	legeq.1	|- ( ph -> ( A .- B ) .<_ ( C .- C ) )
Assertion	legeq	|- ( ph -> A = B )

Proof

Step	Hyp	Ref	Expression
1		legval.p	|- P = ( Base ` G )
2		legval.d	|- .- = ( dist ` G )
3		legval.i	|- I = ( Itv ` G )
4		legval.l	|- .<_ = ( leG ` G )
5		legval.g	|- ( ph -> G e. TarskiG )
6		legid.a	|- ( ph -> A e. P )
7		legid.b	|- ( ph -> B e. P )
8		legtrd.c	|- ( ph -> C e. P )
9		legtrd.d	|- ( ph -> D e. P )
10		legeq.1	|- ( ph -> ( A .- B ) .<_ ( C .- C ) )
11	1 2 3 4 5 8 6 6 7	leg0	|- ( ph -> ( C .- C ) .<_ ( A .- B ) )
12	1 2 3 4 5 6 7 8 8 10 11	legtri3	|- ( ph -> ( A .- B ) = ( C .- C ) )
13	1 2 3 5 6 7 8 12	axtgcgrid	|- ( ph -> A = B )