legtrd

Description: Transitivity of the less-than relationship. Proposition 5.8 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$
	legtrd.e	$⊢ φ \to E \in P$
	legtrd.f	$⊢ φ \to F \in P$
	legtrd.1	$⊢ φ \to (A \underset{˙}{-} B) \underset{˙}{\leq} (C \underset{˙}{-} D)$
	legtrd.2	$⊢ φ \to (C \underset{˙}{-} D) \underset{˙}{\leq} (E \underset{˙}{-} F)$
Assertion	legtrd	$⊢ φ \to (A \underset{˙}{-} B) \underset{˙}{\leq} (E \underset{˙}{-} F)$

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		legtrd.e	$⊢ φ \to E \in P$
11		legtrd.f	$⊢ φ \to F \in P$
12		legtrd.1	$⊢ φ \to (A \underset{˙}{-} B) \underset{˙}{\leq} (C \underset{˙}{-} D)$
13		legtrd.2	$⊢ φ \to (C \underset{˙}{-} D) \underset{˙}{\leq} (E \underset{˙}{-} F)$
14		eqid	$⊢ {Line}_{𝒢} (G) = {Line}_{𝒢} (G)$
15	5	ad4antr	$⊢ ((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (y \in (E I F) \land C \underset{˙}{-} D = E \underset{˙}{-} y)) \to G \in 𝒢_{Tarski}$
16	8	ad4antr	$⊢ ((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (y \in (E I F) \land C \underset{˙}{-} D = E \underset{˙}{-} y)) \to C \in P$
17	9	ad4antr	$⊢ ((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (y \in (E I F) \land C \underset{˙}{-} D = E \underset{˙}{-} y)) \to D \in P$
18		simp-4r	$⊢ ((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (y \in (E I F) \land C \underset{˙}{-} D = E \underset{˙}{-} y)) \to x \in P$
19		eqid	$⊢ \sim_{𝒢} (G) = \sim_{𝒢} (G)$
20	10	ad4antr	$⊢ ((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (y \in (E I F) \land C \underset{˙}{-} D = E \underset{˙}{-} y)) \to E \in P$
21		simplr	$⊢ ((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (y \in (E I F) \land C \underset{˙}{-} D = E \underset{˙}{-} y)) \to y \in P$
22		simpllr	$⊢ ((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (y \in (E I F) \land C \underset{˙}{-} D = E \underset{˙}{-} y)) \to (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)$
23	22	simpld	$⊢ ((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (y \in (E I F) \land C \underset{˙}{-} D = E \underset{˙}{-} y)) \to x \in (C I D)$
24	1 14 3 15 16 18 17 23	btwncolg3	$⊢ ((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (y \in (E I F) \land C \underset{˙}{-} D = E \underset{˙}{-} y)) \to (D \in (C {Line}_{𝒢} (G) x) \lor C = x)$
25		simprr	$⊢ ((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (y \in (E I F) \land C \underset{˙}{-} D = E \underset{˙}{-} y)) \to C \underset{˙}{-} D = E \underset{˙}{-} y$
26	1 14 3 15 16 17 18 19 20 21 2 24 25	lnext	$⊢ ((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (y \in (E I F) \land C \underset{˙}{-} D = E \underset{˙}{-} y)) \to \exists z \in P ⟨“ C D x ”⟩ \sim_{𝒢} (G) ⟨“ E y z ”⟩$
27	15	ad2antrr	$⊢ ((((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (y \in (E I F) \land C \underset{˙}{-} D = E \underset{˙}{-} y)) \land z \in P) \land ⟨“ C D x ”⟩ \sim_{𝒢} (G) ⟨“ E y z ”⟩) \to G \in 𝒢_{Tarski}$
28	20	ad2antrr	$⊢ ((((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (y \in (E I F) \land C \underset{˙}{-} D = E \underset{˙}{-} y)) \land z \in P) \land ⟨“ C D x ”⟩ \sim_{𝒢} (G) ⟨“ E y z ”⟩) \to E \in P$
29		simplr	$⊢ ((((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (y \in (E I F) \land C \underset{˙}{-} D = E \underset{˙}{-} y)) \land z \in P) \land ⟨“ C D x ”⟩ \sim_{𝒢} (G) ⟨“ E y z ”⟩) \to z \in P$
30		simp-4r	$⊢ ((((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (y \in (E I F) \land C \underset{˙}{-} D = E \underset{˙}{-} y)) \land z \in P) \land ⟨“ C D x ”⟩ \sim_{𝒢} (G) ⟨“ E y z ”⟩) \to y \in P$
31	11	ad6antr	$⊢ ((((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (y \in (E I F) \land C \underset{˙}{-} D = E \underset{˙}{-} y)) \land z \in P) \land ⟨“ C D x ”⟩ \sim_{𝒢} (G) ⟨“ E y z ”⟩) \to F \in P$
32	16	ad2antrr	$⊢ ((((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (y \in (E I F) \land C \underset{˙}{-} D = E \underset{˙}{-} y)) \land z \in P) \land ⟨“ C D x ”⟩ \sim_{𝒢} (G) ⟨“ E y z ”⟩) \to C \in P$
33	18	ad2antrr	$⊢ ((((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (y \in (E I F) \land C \underset{˙}{-} D = E \underset{˙}{-} y)) \land z \in P) \land ⟨“ C D x ”⟩ \sim_{𝒢} (G) ⟨“ E y z ”⟩) \to x \in P$
34	17	ad2antrr	$⊢ ((((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (y \in (E I F) \land C \underset{˙}{-} D = E \underset{˙}{-} y)) \land z \in P) \land ⟨“ C D x ”⟩ \sim_{𝒢} (G) ⟨“ E y z ”⟩) \to D \in P$
35		simpr	$⊢ ((((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (y \in (E I F) \land C \underset{˙}{-} D = E \underset{˙}{-} y)) \land z \in P) \land ⟨“ C D x ”⟩ \sim_{𝒢} (G) ⟨“ E y z ”⟩) \to ⟨“ C D x ”⟩ \sim_{𝒢} (G) ⟨“ E y z ”⟩$
36	1 2 3 19 27 32 34 33 28 30 29 35	cgr3swap23	$⊢ ((((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (y \in (E I F) \land C \underset{˙}{-} D = E \underset{˙}{-} y)) \land z \in P) \land ⟨“ C D x ”⟩ \sim_{𝒢} (G) ⟨“ E y z ”⟩) \to ⟨“ C x D ”⟩ \sim_{𝒢} (G) ⟨“ E z y ”⟩$
37	23	ad2antrr	$⊢ ((((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (y \in (E I F) \land C \underset{˙}{-} D = E \underset{˙}{-} y)) \land z \in P) \land ⟨“ C D x ”⟩ \sim_{𝒢} (G) ⟨“ E y z ”⟩) \to x \in (C I D)$
38	1 2 3 19 27 32 33 34 28 29 30 36 37	tgbtwnxfr	$⊢ ((((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (y \in (E I F) \land C \underset{˙}{-} D = E \underset{˙}{-} y)) \land z \in P) \land ⟨“ C D x ”⟩ \sim_{𝒢} (G) ⟨“ E y z ”⟩) \to z \in (E I y)$
39		simpllr	$⊢ ((((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (y \in (E I F) \land C \underset{˙}{-} D = E \underset{˙}{-} y)) \land z \in P) \land ⟨“ C D x ”⟩ \sim_{𝒢} (G) ⟨“ E y z ”⟩) \to (y \in (E I F) \land C \underset{˙}{-} D = E \underset{˙}{-} y)$
40	39	simpld	$⊢ ((((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (y \in (E I F) \land C \underset{˙}{-} D = E \underset{˙}{-} y)) \land z \in P) \land ⟨“ C D x ”⟩ \sim_{𝒢} (G) ⟨“ E y z ”⟩) \to y \in (E I F)$
41	1 2 3 27 28 29 30 31 38 40	tgbtwnexch	$⊢ ((((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (y \in (E I F) \land C \underset{˙}{-} D = E \underset{˙}{-} y)) \land z \in P) \land ⟨“ C D x ”⟩ \sim_{𝒢} (G) ⟨“ E y z ”⟩) \to z \in (E I F)$
42		simp-5r	$⊢ ((((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (y \in (E I F) \land C \underset{˙}{-} D = E \underset{˙}{-} y)) \land z \in P) \land ⟨“ C D x ”⟩ \sim_{𝒢} (G) ⟨“ E y z ”⟩) \to (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)$
43	42	simprd	$⊢ ((((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (y \in (E I F) \land C \underset{˙}{-} D = E \underset{˙}{-} y)) \land z \in P) \land ⟨“ C D x ”⟩ \sim_{𝒢} (G) ⟨“ E y z ”⟩) \to A \underset{˙}{-} B = C \underset{˙}{-} x$
44	1 2 3 19 27 32 33 34 28 29 30 36	cgr3simp1	$⊢ ((((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (y \in (E I F) \land C \underset{˙}{-} D = E \underset{˙}{-} y)) \land z \in P) \land ⟨“ C D x ”⟩ \sim_{𝒢} (G) ⟨“ E y z ”⟩) \to C \underset{˙}{-} x = E \underset{˙}{-} z$
45	43 44	eqtrd	$⊢ ((((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (y \in (E I F) \land C \underset{˙}{-} D = E \underset{˙}{-} y)) \land z \in P) \land ⟨“ C D x ”⟩ \sim_{𝒢} (G) ⟨“ E y z ”⟩) \to A \underset{˙}{-} B = E \underset{˙}{-} z$
46	41 45	jca	$⊢ ((((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (y \in (E I F) \land C \underset{˙}{-} D = E \underset{˙}{-} y)) \land z \in P) \land ⟨“ C D x ”⟩ \sim_{𝒢} (G) ⟨“ E y z ”⟩) \to (z \in (E I F) \land A \underset{˙}{-} B = E \underset{˙}{-} z)$
47	46	ex	$⊢ (((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (y \in (E I F) \land C \underset{˙}{-} D = E \underset{˙}{-} y)) \land z \in P) \to (⟨“ C D x ”⟩ \sim_{𝒢} (G) ⟨“ E y z ”⟩ \to (z \in (E I F) \land A \underset{˙}{-} B = E \underset{˙}{-} z))$
48	47	reximdva	$⊢ ((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (y \in (E I F) \land C \underset{˙}{-} D = E \underset{˙}{-} y)) \to (\exists z \in P ⟨“ C D x ”⟩ \sim_{𝒢} (G) ⟨“ E y z ”⟩ \to \exists z \in P (z \in (E I F) \land A \underset{˙}{-} B = E \underset{˙}{-} z))$
49	26 48	mpd	$⊢ ((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (y \in (E I F) \land C \underset{˙}{-} D = E \underset{˙}{-} y)) \to \exists z \in P (z \in (E I F) \land A \underset{˙}{-} B = E \underset{˙}{-} z)$
50	1 2 3 4 5 8 9 10 11	legov	$⊢ φ \to ((C \underset{˙}{-} D) \underset{˙}{\leq} (E \underset{˙}{-} F) \leftrightarrow \exists y \in P (y \in (E I F) \land C \underset{˙}{-} D = E \underset{˙}{-} y))$
51	13 50	mpbid	$⊢ φ \to \exists y \in P (y \in (E I F) \land C \underset{˙}{-} D = E \underset{˙}{-} y)$
52	51	ad2antrr	$⊢ ((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \to \exists y \in P (y \in (E I F) \land C \underset{˙}{-} D = E \underset{˙}{-} y)$
53	49 52	r19.29a	$⊢ ((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \to \exists z \in P (z \in (E I F) \land A \underset{˙}{-} B = E \underset{˙}{-} z)$
54	1 2 3 4 5 6 7 8 9	legov	$⊢ φ \to ((A \underset{˙}{-} B) \underset{˙}{\leq} (C \underset{˙}{-} D) \leftrightarrow \exists x \in P (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x))$
55	12 54	mpbid	$⊢ φ \to \exists x \in P (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)$
56	53 55	r19.29a	$⊢ φ \to \exists z \in P (z \in (E I F) \land A \underset{˙}{-} B = E \underset{˙}{-} z)$
57	1 2 3 4 5 6 7 10 11	legov	$⊢ φ \to ((A \underset{˙}{-} B) \underset{˙}{\leq} (E \underset{˙}{-} F) \leftrightarrow \exists z \in P (z \in (E I F) \land A \underset{˙}{-} B = E \underset{˙}{-} z))$
58	56 57	mpbird	$⊢ φ \to (A \underset{˙}{-} B) \underset{˙}{\leq} (E \underset{˙}{-} F)$

Metamath Proof Explorer

Theorem legtrd

Proof