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={\mathrm{Base}}_G$$
	legval.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
	legval.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
	legval.l	$$⊢\underset{\dot{}}{\le }={\le }_{𝒢}\left(G\right)$$
	legval.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	legid.a	$$⊢\phi \to A\in P$$
	legid.b	$$⊢\phi \to B\in P$$
	legtrd.c	$$⊢\phi \to C\in P$$
	legtrd.d	$$⊢\phi \to D\in P$$
Assertion	leg0	$$⊢\phi \to \left(A\underset{\dot{}}{-}A\right)\underset{\dot{}}{\le }\left(C\underset{\dot{}}{-}D\right)$$

Proof

Step	Hyp	Ref	Expression
1		legval.p	$$⊢P={\mathrm{Base}}_G$$
2		legval.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
3		legval.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
4		legval.l	$$⊢\underset{\dot{}}{\le }={\le }_{𝒢}\left(G\right)$$
5		legval.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
6		legid.a	$$⊢\phi \to A\in P$$
7		legid.b	$$⊢\phi \to B\in P$$
8		legtrd.c	$$⊢\phi \to C\in P$$
9		legtrd.d	$$⊢\phi \to D\in P$$
10	1 2 3 5 8 9	tgbtwntriv1	$$⊢\phi \to C\in \left(CID\right)$$
11	1 2 3 5 6 8	tgcgrtriv	$$⊢\phi \to A\underset{\dot{}}{-}A=C\underset{\dot{}}{-}C$$
12		eleq1	$$⊢x=C\to \left(x\in \left(CID\right)\leftrightarrow C\in \left(CID\right)\right)$$
13		oveq2	$$⊢x=C\to C\underset{\dot{}}{-}x=C\underset{\dot{}}{-}C$$
14	13	eqeq2d	$$⊢x=C\to \left(A\underset{\dot{}}{-}A=C\underset{\dot{}}{-}x\leftrightarrow A\underset{\dot{}}{-}A=C\underset{\dot{}}{-}C\right)$$
15	12 14	anbi12d	$$⊢x=C\to \left(\left(x\in \left(CID\right)\wedge A\underset{\dot{}}{-}A=C\underset{\dot{}}{-}x\right)\leftrightarrow \left(C\in \left(CID\right)\wedge A\underset{\dot{}}{-}A=C\underset{\dot{}}{-}C\right)\right)$$
16	15	rspcev	$$⊢\left(C\in P\wedge \left(C\in \left(CID\right)\wedge A\underset{\dot{}}{-}A=C\underset{\dot{}}{-}C\right)\right)\to \exists x\in P\left(x\in \left(CID\right)\wedge A\underset{\dot{}}{-}A=C\underset{\dot{}}{-}x\right)$$
17	8 10 11 16	syl12anc	$$⊢\phi \to \exists x\in P\left(x\in \left(CID\right)\wedge A\underset{\dot{}}{-}A=C\underset{\dot{}}{-}x\right)$$
18	1 2 3 4 5 6 6 8 9	legov	$$⊢\phi \to \left(\left(A\underset{\dot{}}{-}A\right)\underset{\dot{}}{\le }\left(C\underset{\dot{}}{-}D\right)\leftrightarrow \exists x\in P\left(x\in \left(CID\right)\wedge A\underset{\dot{}}{-}A=C\underset{\dot{}}{-}x\right)\right)$$
19	17 18	mpbird	$$⊢\phi \to \left(A\underset{\dot{}}{-}A\right)\underset{\dot{}}{\le }\left(C\underset{\dot{}}{-}D\right)$$