Theorem ltgov

Description: Strict "shorter than" geometric relation between segments. (Contributed by Thierry Arnoux, 15-Dec-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}}$$
	legso.a	$$⊢E=\underset{\dot{}}{-}\left[P\times P\right]$$
	legso.f	$$⊢\phi \to \mathrm{Fun}\underset{\dot{}}{-}$$
	legso.l	$$⊢\underset{\dot{}}{<}=\left({\underset{\dot{}}{\le }\upharpoonright }_E\right)\setminus \mathrm{I}$$
	legso.d	$$⊢\phi \to P\times P\subseteq \mathrm{dom}\underset{\dot{}}{-}$$
	ltgov.a	$$⊢\phi \to A\in P$$
	ltgov.b	$$⊢\phi \to B\in P$$
Assertion	ltgov	$$⊢\phi \to \left(\left(A\underset{\dot{}}{-}B\right)\underset{\dot{}}{<}\left(C\underset{\dot{}}{-}D\right)\leftrightarrow \left(\left(A\underset{\dot{}}{-}B\right)\underset{\dot{}}{\le }\left(C\underset{\dot{}}{-}D\right)\wedge A\underset{\dot{}}{-}B\ne C\underset{\dot{}}{-}D\right)\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		legso.a	$$⊢E=\underset{\dot{}}{-}\left[P\times P\right]$$
7		legso.f	$$⊢\phi \to \mathrm{Fun}\underset{\dot{}}{-}$$
8		legso.l	$$⊢\underset{\dot{}}{<}=\left({\underset{\dot{}}{\le }\upharpoonright }_E\right)\setminus \mathrm{I}$$
9		legso.d	$$⊢\phi \to P\times P\subseteq \mathrm{dom}\underset{\dot{}}{-}$$
10		ltgov.a	$$⊢\phi \to A\in P$$
11		ltgov.b	$$⊢\phi \to B\in P$$
12	8	breqi	$$⊢\left(A\underset{\dot{}}{-}B\right)\underset{\dot{}}{<}\left(C\underset{\dot{}}{-}D\right)\leftrightarrow \left(A\underset{\dot{}}{-}B\right)\left(\left({\underset{\dot{}}{\le }\upharpoonright }_E\right)\setminus \mathrm{I}\right)\left(C\underset{\dot{}}{-}D\right)$$
13		brdif	$$⊢\left(A\underset{\dot{}}{-}B\right)\left(\left({\underset{\dot{}}{\le }\upharpoonright }_E\right)\setminus \mathrm{I}\right)\left(C\underset{\dot{}}{-}D\right)\leftrightarrow \left(\left(A\underset{\dot{}}{-}B\right)\left({\underset{\dot{}}{\le }\upharpoonright }_E\right)\left(C\underset{\dot{}}{-}D\right)\wedge \neg \left(A\underset{\dot{}}{-}B\right)\mathrm{I}\left(C\underset{\dot{}}{-}D\right)\right)$$
14	12 13	bitri	$$⊢\left(A\underset{\dot{}}{-}B\right)\underset{\dot{}}{<}\left(C\underset{\dot{}}{-}D\right)\leftrightarrow \left(\left(A\underset{\dot{}}{-}B\right)\left({\underset{\dot{}}{\le }\upharpoonright }_E\right)\left(C\underset{\dot{}}{-}D\right)\wedge \neg \left(A\underset{\dot{}}{-}B\right)\mathrm{I}\left(C\underset{\dot{}}{-}D\right)\right)$$
15		ovex	$$⊢C\underset{\dot{}}{-}D\in \mathrm{V}$$
16	15	brresi	$$⊢\left(A\underset{\dot{}}{-}B\right)\left({\underset{\dot{}}{\le }\upharpoonright }_E\right)\left(C\underset{\dot{}}{-}D\right)\leftrightarrow \left(A\underset{\dot{}}{-}B\in E\wedge \left(A\underset{\dot{}}{-}B\right)\underset{\dot{}}{\le }\left(C\underset{\dot{}}{-}D\right)\right)$$
17	16	anbi1i	$$⊢\left(\left(A\underset{\dot{}}{-}B\right)\left({\underset{\dot{}}{\le }\upharpoonright }_E\right)\left(C\underset{\dot{}}{-}D\right)\wedge \neg \left(A\underset{\dot{}}{-}B\right)\mathrm{I}\left(C\underset{\dot{}}{-}D\right)\right)\leftrightarrow \left(\left(A\underset{\dot{}}{-}B\in E\wedge \left(A\underset{\dot{}}{-}B\right)\underset{\dot{}}{\le }\left(C\underset{\dot{}}{-}D\right)\right)\wedge \neg \left(A\underset{\dot{}}{-}B\right)\mathrm{I}\left(C\underset{\dot{}}{-}D\right)\right)$$
18		an21	$$⊢\left(\left(A\underset{\dot{}}{-}B\in E\wedge \left(A\underset{\dot{}}{-}B\right)\underset{\dot{}}{\le }\left(C\underset{\dot{}}{-}D\right)\right)\wedge \neg \left(A\underset{\dot{}}{-}B\right)\mathrm{I}\left(C\underset{\dot{}}{-}D\right)\right)\leftrightarrow \left(\left(A\underset{\dot{}}{-}B\right)\underset{\dot{}}{\le }\left(C\underset{\dot{}}{-}D\right)\wedge \left(A\underset{\dot{}}{-}B\in E\wedge \neg \left(A\underset{\dot{}}{-}B\right)\mathrm{I}\left(C\underset{\dot{}}{-}D\right)\right)\right)$$
19	14 17 18	3bitri	$$⊢\left(A\underset{\dot{}}{-}B\right)\underset{\dot{}}{<}\left(C\underset{\dot{}}{-}D\right)\leftrightarrow \left(\left(A\underset{\dot{}}{-}B\right)\underset{\dot{}}{\le }\left(C\underset{\dot{}}{-}D\right)\wedge \left(A\underset{\dot{}}{-}B\in E\wedge \neg \left(A\underset{\dot{}}{-}B\right)\mathrm{I}\left(C\underset{\dot{}}{-}D\right)\right)\right)$$
20	10 11 7 9	elovimad	$$⊢\phi \to A\underset{\dot{}}{-}B\in \underset{\dot{}}{-}\left[P\times P\right]$$
21	20 6	eleqtrrdi	$$⊢\phi \to A\underset{\dot{}}{-}B\in E$$
22	21	biantrurd	$$⊢\phi \to \left(\neg \left(A\underset{\dot{}}{-}B\right)\mathrm{I}\left(C\underset{\dot{}}{-}D\right)\leftrightarrow \left(A\underset{\dot{}}{-}B\in E\wedge \neg \left(A\underset{\dot{}}{-}B\right)\mathrm{I}\left(C\underset{\dot{}}{-}D\right)\right)\right)$$
23	15	ideq	$$⊢\left(A\underset{\dot{}}{-}B\right)\mathrm{I}\left(C\underset{\dot{}}{-}D\right)\leftrightarrow A\underset{\dot{}}{-}B=C\underset{\dot{}}{-}D$$
24	23	necon3bbii	$$⊢\neg \left(A\underset{\dot{}}{-}B\right)\mathrm{I}\left(C\underset{\dot{}}{-}D\right)\leftrightarrow A\underset{\dot{}}{-}B\ne C\underset{\dot{}}{-}D$$
25	22 24	bitr3di	$$⊢\phi \to \left(\left(A\underset{\dot{}}{-}B\in E\wedge \neg \left(A\underset{\dot{}}{-}B\right)\mathrm{I}\left(C\underset{\dot{}}{-}D\right)\right)\leftrightarrow A\underset{\dot{}}{-}B\ne C\underset{\dot{}}{-}D\right)$$
26	25	anbi2d	$$⊢\phi \to \left(\left(\left(A\underset{\dot{}}{-}B\right)\underset{\dot{}}{\le }\left(C\underset{\dot{}}{-}D\right)\wedge \left(A\underset{\dot{}}{-}B\in E\wedge \neg \left(A\underset{\dot{}}{-}B\right)\mathrm{I}\left(C\underset{\dot{}}{-}D\right)\right)\right)\leftrightarrow \left(\left(A\underset{\dot{}}{-}B\right)\underset{\dot{}}{\le }\left(C\underset{\dot{}}{-}D\right)\wedge A\underset{\dot{}}{-}B\ne C\underset{\dot{}}{-}D\right)\right)$$
27	19 26	bitrid	$$⊢\phi \to \left(\left(A\underset{\dot{}}{-}B\right)\underset{\dot{}}{<}\left(C\underset{\dot{}}{-}D\right)\leftrightarrow \left(\left(A\underset{\dot{}}{-}B\right)\underset{\dot{}}{\le }\left(C\underset{\dot{}}{-}D\right)\wedge A\underset{\dot{}}{-}B\ne C\underset{\dot{}}{-}D\right)\right)$$