legtrid

Description: Trichotomy law for the less-than relationship. Proposition 5.10 of Schwabhauser p. 42. (Contributed by Thierry Arnoux, 27-Jun-2019)

	Ref	Expression
Hypotheses	legval.p	$⊢ P = {Base}_{G}$
	legval.d	$⊢ \underset{˙}{-} = dist (G)$
	legval.i	$⊢ I = Itv (G)$
	legval.l	$⊢ \underset{˙}{\leq} = \leq_{𝒢} (G)$
	legval.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	legid.a	$⊢ φ \to A \in P$
	legid.b	$⊢ φ \to B \in P$
	legtrd.c	$⊢ φ \to C \in P$
	legtrd.d	$⊢ φ \to D \in P$
Assertion	legtrid	$⊢ φ \to ((A \underset{˙}{-} B) \underset{˙}{\leq} (C \underset{˙}{-} D) \lor (C \underset{˙}{-} D) \underset{˙}{\leq} (A \underset{˙}{-} B))$

Proof

Step	Hyp	Ref	Expression
1		legval.p	$⊢ P = {Base}_{G}$
2		legval.d	$⊢ \underset{˙}{-} = dist (G)$
3		legval.i	$⊢ I = Itv (G)$
4		legval.l	$⊢ \underset{˙}{\leq} = \leq_{𝒢} (G)$
5		legval.g	$⊢ φ \to G \in 𝒢_{Tarski}$
6		legid.a	$⊢ φ \to A \in P$
7		legid.b	$⊢ φ \to B \in P$
8		legtrd.c	$⊢ φ \to C \in P$
9		legtrd.d	$⊢ φ \to D \in P$
10	5	adantr	$⊢ (φ \land \|P\| = 1) \to G \in 𝒢_{Tarski}$
11	6	adantr	$⊢ (φ \land \|P\| = 1) \to A \in P$
12	7	adantr	$⊢ (φ \land \|P\| = 1) \to B \in P$
13	1 2 3 4 10 11 12	legid	$⊢ (φ \land \|P\| = 1) \to (A \underset{˙}{-} B) \underset{˙}{\leq} (A \underset{˙}{-} B)$
14	8	adantr	$⊢ (φ \land \|P\| = 1) \to C \in P$
15		simpr	$⊢ (φ \land \|P\| = 1) \to \|P\| = 1$
16	9	adantr	$⊢ (φ \land \|P\| = 1) \to D \in P$
17	1 2 3 10 11 12 14 15 16	tgldim0cgr	$⊢ (φ \land \|P\| = 1) \to A \underset{˙}{-} B = C \underset{˙}{-} D$
18	13 17	breqtrd	$⊢ (φ \land \|P\| = 1) \to (A \underset{˙}{-} B) \underset{˙}{\leq} (C \underset{˙}{-} D)$
19	18	orcd	$⊢ (φ \land \|P\| = 1) \to ((A \underset{˙}{-} B) \underset{˙}{\leq} (C \underset{˙}{-} D) \lor (C \underset{˙}{-} D) \underset{˙}{\leq} (A \underset{˙}{-} B))$
20	5	ad3antrrr	$⊢ (((φ \land x \in P) \land (A \in (B I x) \land A \neq x)) \land (y \in P \land (A \in (x I y) \land A \underset{˙}{-} y = C \underset{˙}{-} D))) \to G \in 𝒢_{Tarski}$
21		simplr	$⊢ ((φ \land x \in P) \land (A \in (B I x) \land A \neq x)) \to x \in P$
22	21	adantr	$⊢ (((φ \land x \in P) \land (A \in (B I x) \land A \neq x)) \land (y \in P \land (A \in (x I y) \land A \underset{˙}{-} y = C \underset{˙}{-} D))) \to x \in P$
23	6	ad3antrrr	$⊢ (((φ \land x \in P) \land (A \in (B I x) \land A \neq x)) \land (y \in P \land (A \in (x I y) \land A \underset{˙}{-} y = C \underset{˙}{-} D))) \to A \in P$
24	7	ad3antrrr	$⊢ (((φ \land x \in P) \land (A \in (B I x) \land A \neq x)) \land (y \in P \land (A \in (x I y) \land A \underset{˙}{-} y = C \underset{˙}{-} D))) \to B \in P$
25		simprl	$⊢ (((φ \land x \in P) \land (A \in (B I x) \land A \neq x)) \land (y \in P \land (A \in (x I y) \land A \underset{˙}{-} y = C \underset{˙}{-} D))) \to y \in P$
26		simplrr	$⊢ (((φ \land x \in P) \land (A \in (B I x) \land A \neq x)) \land (y \in P \land (A \in (x I y) \land A \underset{˙}{-} y = C \underset{˙}{-} D))) \to A \neq x$
27	26	necomd	$⊢ (((φ \land x \in P) \land (A \in (B I x) \land A \neq x)) \land (y \in P \land (A \in (x I y) \land A \underset{˙}{-} y = C \underset{˙}{-} D))) \to x \neq A$
28		simplrl	$⊢ (((φ \land x \in P) \land (A \in (B I x) \land A \neq x)) \land (y \in P \land (A \in (x I y) \land A \underset{˙}{-} y = C \underset{˙}{-} D))) \to A \in (B I x)$
29	1 2 3 20 24 23 22 28	tgbtwncom	$⊢ (((φ \land x \in P) \land (A \in (B I x) \land A \neq x)) \land (y \in P \land (A \in (x I y) \land A \underset{˙}{-} y = C \underset{˙}{-} D))) \to A \in (x I B)$
30		simprrl	$⊢ (((φ \land x \in P) \land (A \in (B I x) \land A \neq x)) \land (y \in P \land (A \in (x I y) \land A \underset{˙}{-} y = C \underset{˙}{-} D))) \to A \in (x I y)$
31	1 3 20 22 23 24 25 27 29 30	tgbtwnconn2	$⊢ (((φ \land x \in P) \land (A \in (B I x) \land A \neq x)) \land (y \in P \land (A \in (x I y) \land A \underset{˙}{-} y = C \underset{˙}{-} D))) \to (B \in (A I y) \lor y \in (A I B))$
32		simprrr	$⊢ (((φ \land x \in P) \land (A \in (B I x) \land A \neq x)) \land (y \in P \land (A \in (x I y) \land A \underset{˙}{-} y = C \underset{˙}{-} D))) \to A \underset{˙}{-} y = C \underset{˙}{-} D$
33	31 32	jca	$⊢ (((φ \land x \in P) \land (A \in (B I x) \land A \neq x)) \land (y \in P \land (A \in (x I y) \land A \underset{˙}{-} y = C \underset{˙}{-} D))) \to ((B \in (A I y) \lor y \in (A I B)) \land A \underset{˙}{-} y = C \underset{˙}{-} D)$
34	5	ad2antrr	$⊢ ((φ \land x \in P) \land (A \in (B I x) \land A \neq x)) \to G \in 𝒢_{Tarski}$
35	6	ad2antrr	$⊢ ((φ \land x \in P) \land (A \in (B I x) \land A \neq x)) \to A \in P$
36	8	ad2antrr	$⊢ ((φ \land x \in P) \land (A \in (B I x) \land A \neq x)) \to C \in P$
37	9	ad2antrr	$⊢ ((φ \land x \in P) \land (A \in (B I x) \land A \neq x)) \to D \in P$
38	1 2 3 34 21 35 36 37	axtgsegcon	$⊢ ((φ \land x \in P) \land (A \in (B I x) \land A \neq x)) \to \exists y \in P (A \in (x I y) \land A \underset{˙}{-} y = C \underset{˙}{-} D)$
39	33 38	reximddv	$⊢ ((φ \land x \in P) \land (A \in (B I x) \land A \neq x)) \to \exists y \in P ((B \in (A I y) \lor y \in (A I B)) \land A \underset{˙}{-} y = C \underset{˙}{-} D)$
40	39	adantllr	$⊢ (((φ \land 2 \leq \|P\|) \land x \in P) \land (A \in (B I x) \land A \neq x)) \to \exists y \in P ((B \in (A I y) \lor y \in (A I B)) \land A \underset{˙}{-} y = C \underset{˙}{-} D)$
41	5	adantr	$⊢ (φ \land 2 \leq \|P\|) \to G \in 𝒢_{Tarski}$
42	7	adantr	$⊢ (φ \land 2 \leq \|P\|) \to B \in P$
43	6	adantr	$⊢ (φ \land 2 \leq \|P\|) \to A \in P$
44		simpr	$⊢ (φ \land 2 \leq \|P\|) \to 2 \leq \|P\|$
45	1 2 3 41 42 43 44	tgbtwndiff	$⊢ (φ \land 2 \leq \|P\|) \to \exists x \in P (A \in (B I x) \land A \neq x)$
46	40 45	r19.29a	$⊢ (φ \land 2 \leq \|P\|) \to \exists y \in P ((B \in (A I y) \lor y \in (A I B)) \land A \underset{˙}{-} y = C \underset{˙}{-} D)$
47		andir	$⊢ ((B \in (A I y) \lor y \in (A I B)) \land A \underset{˙}{-} y = C \underset{˙}{-} D) \leftrightarrow ((B \in (A I y) \land A \underset{˙}{-} y = C \underset{˙}{-} D) \lor (y \in (A I B) \land A \underset{˙}{-} y = C \underset{˙}{-} D))$
48		eqcom	$⊢ A \underset{˙}{-} y = C \underset{˙}{-} D \leftrightarrow C \underset{˙}{-} D = A \underset{˙}{-} y$
49	48	anbi2i	$⊢ (y \in (A I B) \land A \underset{˙}{-} y = C \underset{˙}{-} D) \leftrightarrow (y \in (A I B) \land C \underset{˙}{-} D = A \underset{˙}{-} y)$
50	49	orbi2i	$⊢ ((B \in (A I y) \land A \underset{˙}{-} y = C \underset{˙}{-} D) \lor (y \in (A I B) \land A \underset{˙}{-} y = C \underset{˙}{-} D)) \leftrightarrow ((B \in (A I y) \land A \underset{˙}{-} y = C \underset{˙}{-} D) \lor (y \in (A I B) \land C \underset{˙}{-} D = A \underset{˙}{-} y))$
51	47 50	bitri	$⊢ ((B \in (A I y) \lor y \in (A I B)) \land A \underset{˙}{-} y = C \underset{˙}{-} D) \leftrightarrow ((B \in (A I y) \land A \underset{˙}{-} y = C \underset{˙}{-} D) \lor (y \in (A I B) \land C \underset{˙}{-} D = A \underset{˙}{-} y))$
52	51	rexbii	$⊢ \exists y \in P ((B \in (A I y) \lor y \in (A I B)) \land A \underset{˙}{-} y = C \underset{˙}{-} D) \leftrightarrow \exists y \in P ((B \in (A I y) \land A \underset{˙}{-} y = C \underset{˙}{-} D) \lor (y \in (A I B) \land C \underset{˙}{-} D = A \underset{˙}{-} y))$
53		r19.43	$⊢ \exists y \in P ((B \in (A I y) \land A \underset{˙}{-} y = C \underset{˙}{-} D) \lor (y \in (A I B) \land C \underset{˙}{-} D = A \underset{˙}{-} y)) \leftrightarrow (\exists y \in P (B \in (A I y) \land A \underset{˙}{-} y = C \underset{˙}{-} D) \lor \exists y \in P (y \in (A I B) \land C \underset{˙}{-} D = A \underset{˙}{-} y))$
54	52 53	bitri	$⊢ \exists y \in P ((B \in (A I y) \lor y \in (A I B)) \land A \underset{˙}{-} y = C \underset{˙}{-} D) \leftrightarrow (\exists y \in P (B \in (A I y) \land A \underset{˙}{-} y = C \underset{˙}{-} D) \lor \exists y \in P (y \in (A I B) \land C \underset{˙}{-} D = A \underset{˙}{-} y))$
55	46 54	sylib	$⊢ (φ \land 2 \leq \|P\|) \to (\exists y \in P (B \in (A I y) \land A \underset{˙}{-} y = C \underset{˙}{-} D) \lor \exists y \in P (y \in (A I B) \land C \underset{˙}{-} D = A \underset{˙}{-} y))$
56	1 2 3 4 5 6 7 8 9	legov2	$⊢ φ \to ((A \underset{˙}{-} B) \underset{˙}{\leq} (C \underset{˙}{-} D) \leftrightarrow \exists y \in P (B \in (A I y) \land A \underset{˙}{-} y = C \underset{˙}{-} D))$
57	1 2 3 4 5 8 9 6 7	legov	$⊢ φ \to ((C \underset{˙}{-} D) \underset{˙}{\leq} (A \underset{˙}{-} B) \leftrightarrow \exists y \in P (y \in (A I B) \land C \underset{˙}{-} D = A \underset{˙}{-} y))$
58	56 57	orbi12d	$⊢ φ \to (((A \underset{˙}{-} B) \underset{˙}{\leq} (C \underset{˙}{-} D) \lor (C \underset{˙}{-} D) \underset{˙}{\leq} (A \underset{˙}{-} B)) \leftrightarrow (\exists y \in P (B \in (A I y) \land A \underset{˙}{-} y = C \underset{˙}{-} D) \lor \exists y \in P (y \in (A I B) \land C \underset{˙}{-} D = A \underset{˙}{-} y)))$
59	58	adantr	$⊢ (φ \land 2 \leq \|P\|) \to (((A \underset{˙}{-} B) \underset{˙}{\leq} (C \underset{˙}{-} D) \lor (C \underset{˙}{-} D) \underset{˙}{\leq} (A \underset{˙}{-} B)) \leftrightarrow (\exists y \in P (B \in (A I y) \land A \underset{˙}{-} y = C \underset{˙}{-} D) \lor \exists y \in P (y \in (A I B) \land C \underset{˙}{-} D = A \underset{˙}{-} y)))$
60	55 59	mpbird	$⊢ (φ \land 2 \leq \|P\|) \to ((A \underset{˙}{-} B) \underset{˙}{\leq} (C \underset{˙}{-} D) \lor (C \underset{˙}{-} D) \underset{˙}{\leq} (A \underset{˙}{-} B))$
61	1 6	tgldimor	$⊢ φ \to (\|P\| = 1 \lor 2 \leq \|P\|)$
62	19 60 61	mpjaodan	$⊢ φ \to ((A \underset{˙}{-} B) \underset{˙}{\leq} (C \underset{˙}{-} D) \lor (C \underset{˙}{-} D) \underset{˙}{\leq} (A \underset{˙}{-} B))$

Metamath Proof Explorer

Theorem legtrid

Proof