Theorem leg0

Description: Degenerated (zero-length) segments are minimal. Proposition 5.11 of Schwabhauser p. 42. (Contributed by Thierry Arnoux, 27-Jun-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 )
Assertion	leg0	|- ( ph -> ( A .- A ) .<_ ( C .- D ) )

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	1 2 3 5 8 9	tgbtwntriv1	|- ( ph -> C e. ( C I D ) )
11	1 2 3 5 6 8	tgcgrtriv	|- ( ph -> ( A .- A ) = ( C .- C ) )
12		eleq1	|- ( x = C -> ( x e. ( C I D ) <-> C e. ( C I D ) ) )
13		oveq2	|- ( x = C -> ( C .- x ) = ( C .- C ) )
14	13	eqeq2d	|- ( x = C -> ( ( A .- A ) = ( C .- x ) <-> ( A .- A ) = ( C .- C ) ) )
15	12 14	anbi12d	|- ( x = C -> ( ( x e. ( C I D ) /\ ( A .- A ) = ( C .- x ) ) <-> ( C e. ( C I D ) /\ ( A .- A ) = ( C .- C ) ) ) )
16	15	rspcev	|- ( ( C e. P /\ ( C e. ( C I D ) /\ ( A .- A ) = ( C .- C ) ) ) -> E. x e. P ( x e. ( C I D ) /\ ( A .- A ) = ( C .- x ) ) )
17	8 10 11 16	syl12anc	|- ( ph -> E. x e. P ( x e. ( C I D ) /\ ( A .- A ) = ( C .- x ) ) )
18	1 2 3 4 5 6 6 8 9	legov	|- ( ph -> ( ( A .- A ) .<_ ( C .- D ) <-> E. x e. P ( x e. ( C I D ) /\ ( A .- A ) = ( C .- x ) ) ) )
19	17 18	mpbird	|- ( ph -> ( A .- A ) .<_ ( C .- D ) )