legov2

Description: An equivalent definition of the less-than relationship. Definition 5.5 of Schwabhauser p. 41. (Contributed by Thierry Arnoux, 21-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}$
	legov.a	$⊢ φ \to A \in P$
	legov.b	$⊢ φ \to B \in P$
	legov.c	$⊢ φ \to C \in P$
	legov.d	$⊢ φ \to D \in P$
Assertion	legov2	$⊢ φ \to ((A \underset{˙}{-} B) \underset{˙}{\leq} (C \underset{˙}{-} D) \leftrightarrow \exists x \in P (B \in (A I x) \land A \underset{˙}{-} x = C \underset{˙}{-} D))$

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		legov.a	$⊢ φ \to A \in P$
7		legov.b	$⊢ φ \to B \in P$
8		legov.c	$⊢ φ \to C \in P$
9		legov.d	$⊢ φ \to D \in P$
10	1 2 3 4 5 6 7 8 9	legov	$⊢ φ \to ((A \underset{˙}{-} B) \underset{˙}{\leq} (C \underset{˙}{-} D) \leftrightarrow \exists y \in P (y \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} y))$
11		eqid	$⊢ {Line}_{𝒢} (G) = {Line}_{𝒢} (G)$
12	5	ad2antrr	$⊢ ((φ \land z \in P) \land (z \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} z)) \to G \in 𝒢_{Tarski}$
13	8	ad2antrr	$⊢ ((φ \land z \in P) \land (z \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} z)) \to C \in P$
14		simplr	$⊢ ((φ \land z \in P) \land (z \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} z)) \to z \in P$
15	9	ad2antrr	$⊢ ((φ \land z \in P) \land (z \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} z)) \to D \in P$
16		eqid	$⊢ \sim_{𝒢} (G) = \sim_{𝒢} (G)$
17	6	ad2antrr	$⊢ ((φ \land z \in P) \land (z \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} z)) \to A \in P$
18	7	ad2antrr	$⊢ ((φ \land z \in P) \land (z \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} z)) \to B \in P$
19		simprl	$⊢ ((φ \land z \in P) \land (z \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} z)) \to z \in (C I D)$
20	1 11 3 12 13 15 14 19	btwncolg1	$⊢ ((φ \land z \in P) \land (z \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} z)) \to (z \in (C {Line}_{𝒢} (G) D) \lor C = D)$
21		simprr	$⊢ ((φ \land z \in P) \land (z \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} z)) \to A \underset{˙}{-} B = C \underset{˙}{-} z$
22	21	eqcomd	$⊢ ((φ \land z \in P) \land (z \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} z)) \to C \underset{˙}{-} z = A \underset{˙}{-} B$
23	1 11 3 12 13 14 15 16 17 18 2 20 22	lnext	$⊢ ((φ \land z \in P) \land (z \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} z)) \to \exists x \in P ⟨“ C z D ”⟩ \sim_{𝒢} (G) ⟨“ A B x ”⟩$
24	12	ad2antrr	$⊢ ((((φ \land z \in P) \land (z \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} z)) \land x \in P) \land ⟨“ C z D ”⟩ \sim_{𝒢} (G) ⟨“ A B x ”⟩) \to G \in 𝒢_{Tarski}$
25	13	ad2antrr	$⊢ ((((φ \land z \in P) \land (z \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} z)) \land x \in P) \land ⟨“ C z D ”⟩ \sim_{𝒢} (G) ⟨“ A B x ”⟩) \to C \in P$
26	14	ad2antrr	$⊢ ((((φ \land z \in P) \land (z \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} z)) \land x \in P) \land ⟨“ C z D ”⟩ \sim_{𝒢} (G) ⟨“ A B x ”⟩) \to z \in P$
27	15	ad2antrr	$⊢ ((((φ \land z \in P) \land (z \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} z)) \land x \in P) \land ⟨“ C z D ”⟩ \sim_{𝒢} (G) ⟨“ A B x ”⟩) \to D \in P$
28	17	ad2antrr	$⊢ ((((φ \land z \in P) \land (z \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} z)) \land x \in P) \land ⟨“ C z D ”⟩ \sim_{𝒢} (G) ⟨“ A B x ”⟩) \to A \in P$
29	18	ad2antrr	$⊢ ((((φ \land z \in P) \land (z \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} z)) \land x \in P) \land ⟨“ C z D ”⟩ \sim_{𝒢} (G) ⟨“ A B x ”⟩) \to B \in P$
30		simplr	$⊢ ((((φ \land z \in P) \land (z \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} z)) \land x \in P) \land ⟨“ C z D ”⟩ \sim_{𝒢} (G) ⟨“ A B x ”⟩) \to x \in P$
31		simpr	$⊢ ((((φ \land z \in P) \land (z \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} z)) \land x \in P) \land ⟨“ C z D ”⟩ \sim_{𝒢} (G) ⟨“ A B x ”⟩) \to ⟨“ C z D ”⟩ \sim_{𝒢} (G) ⟨“ A B x ”⟩$
32		simpllr	$⊢ ((((φ \land z \in P) \land (z \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} z)) \land x \in P) \land ⟨“ C z D ”⟩ \sim_{𝒢} (G) ⟨“ A B x ”⟩) \to (z \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} z)$
33	32	simpld	$⊢ ((((φ \land z \in P) \land (z \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} z)) \land x \in P) \land ⟨“ C z D ”⟩ \sim_{𝒢} (G) ⟨“ A B x ”⟩) \to z \in (C I D)$
34	1 2 3 16 24 25 26 27 28 29 30 31 33	tgbtwnxfr	$⊢ ((((φ \land z \in P) \land (z \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} z)) \land x \in P) \land ⟨“ C z D ”⟩ \sim_{𝒢} (G) ⟨“ A B x ”⟩) \to B \in (A I x)$
35	1 2 3 16 24 25 26 27 28 29 30 31	trgcgrcom	$⊢ ((((φ \land z \in P) \land (z \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} z)) \land x \in P) \land ⟨“ C z D ”⟩ \sim_{𝒢} (G) ⟨“ A B x ”⟩) \to ⟨“ A B x ”⟩ \sim_{𝒢} (G) ⟨“ C z D ”⟩$
36	1 2 3 16 24 28 29 30 25 26 27 35	cgr3simp3	$⊢ ((((φ \land z \in P) \land (z \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} z)) \land x \in P) \land ⟨“ C z D ”⟩ \sim_{𝒢} (G) ⟨“ A B x ”⟩) \to x \underset{˙}{-} A = D \underset{˙}{-} C$
37	1 2 3 24 30 28 27 25 36	tgcgrcomlr	$⊢ ((((φ \land z \in P) \land (z \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} z)) \land x \in P) \land ⟨“ C z D ”⟩ \sim_{𝒢} (G) ⟨“ A B x ”⟩) \to A \underset{˙}{-} x = C \underset{˙}{-} D$
38	34 37	jca	$⊢ ((((φ \land z \in P) \land (z \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} z)) \land x \in P) \land ⟨“ C z D ”⟩ \sim_{𝒢} (G) ⟨“ A B x ”⟩) \to (B \in (A I x) \land A \underset{˙}{-} x = C \underset{˙}{-} D)$
39	38	ex	$⊢ (((φ \land z \in P) \land (z \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} z)) \land x \in P) \to (⟨“ C z D ”⟩ \sim_{𝒢} (G) ⟨“ A B x ”⟩ \to (B \in (A I x) \land A \underset{˙}{-} x = C \underset{˙}{-} D))$
40	39	reximdva	$⊢ ((φ \land z \in P) \land (z \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} z)) \to (\exists x \in P ⟨“ C z D ”⟩ \sim_{𝒢} (G) ⟨“ A B x ”⟩ \to \exists x \in P (B \in (A I x) \land A \underset{˙}{-} x = C \underset{˙}{-} D))$
41	23 40	mpd	$⊢ ((φ \land z \in P) \land (z \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} z)) \to \exists x \in P (B \in (A I x) \land A \underset{˙}{-} x = C \underset{˙}{-} D)$
42	41	adantllr	$⊢ (((φ \land \exists y \in P (y \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} y)) \land z \in P) \land (z \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} z)) \to \exists x \in P (B \in (A I x) \land A \underset{˙}{-} x = C \underset{˙}{-} D)$
43		simpr	$⊢ (φ \land \exists y \in P (y \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} y)) \to \exists y \in P (y \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} y)$
44		eleq1	$⊢ y = z \to (y \in (C I D) \leftrightarrow z \in (C I D))$
45		oveq2	$⊢ y = z \to C \underset{˙}{-} y = C \underset{˙}{-} z$
46	45	eqeq2d	$⊢ y = z \to (A \underset{˙}{-} B = C \underset{˙}{-} y \leftrightarrow A \underset{˙}{-} B = C \underset{˙}{-} z)$
47	44 46	anbi12d	$⊢ y = z \to ((y \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} y) \leftrightarrow (z \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} z))$
48	47	cbvrexvw	$⊢ \exists y \in P (y \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} y) \leftrightarrow \exists z \in P (z \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} z)$
49	43 48	sylib	$⊢ (φ \land \exists y \in P (y \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} y)) \to \exists z \in P (z \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} z)$
50	42 49	r19.29a	$⊢ (φ \land \exists y \in P (y \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} y)) \to \exists x \in P (B \in (A I x) \land A \underset{˙}{-} x = C \underset{˙}{-} D)$
51	5	ad2antrr	$⊢ ((φ \land z \in P) \land (B \in (A I z) \land A \underset{˙}{-} z = C \underset{˙}{-} D)) \to G \in 𝒢_{Tarski}$
52	6	ad2antrr	$⊢ ((φ \land z \in P) \land (B \in (A I z) \land A \underset{˙}{-} z = C \underset{˙}{-} D)) \to A \in P$
53		simplr	$⊢ ((φ \land z \in P) \land (B \in (A I z) \land A \underset{˙}{-} z = C \underset{˙}{-} D)) \to z \in P$
54	7	ad2antrr	$⊢ ((φ \land z \in P) \land (B \in (A I z) \land A \underset{˙}{-} z = C \underset{˙}{-} D)) \to B \in P$
55	8	ad2antrr	$⊢ ((φ \land z \in P) \land (B \in (A I z) \land A \underset{˙}{-} z = C \underset{˙}{-} D)) \to C \in P$
56	9	ad2antrr	$⊢ ((φ \land z \in P) \land (B \in (A I z) \land A \underset{˙}{-} z = C \underset{˙}{-} D)) \to D \in P$
57		simprl	$⊢ ((φ \land z \in P) \land (B \in (A I z) \land A \underset{˙}{-} z = C \underset{˙}{-} D)) \to B \in (A I z)$
58	1 11 3 51 52 54 53 57	btwncolg3	$⊢ ((φ \land z \in P) \land (B \in (A I z) \land A \underset{˙}{-} z = C \underset{˙}{-} D)) \to (z \in (A {Line}_{𝒢} (G) B) \lor A = B)$
59		simprr	$⊢ ((φ \land z \in P) \land (B \in (A I z) \land A \underset{˙}{-} z = C \underset{˙}{-} D)) \to A \underset{˙}{-} z = C \underset{˙}{-} D$
60	1 11 3 51 52 53 54 16 55 56 2 58 59	lnext	$⊢ ((φ \land z \in P) \land (B \in (A I z) \land A \underset{˙}{-} z = C \underset{˙}{-} D)) \to \exists y \in P ⟨“ A z B ”⟩ \sim_{𝒢} (G) ⟨“ C D y ”⟩$
61	51	ad2antrr	$⊢ ((((φ \land z \in P) \land (B \in (A I z) \land A \underset{˙}{-} z = C \underset{˙}{-} D)) \land y \in P) \land ⟨“ A z B ”⟩ \sim_{𝒢} (G) ⟨“ C D y ”⟩) \to G \in 𝒢_{Tarski}$
62	52	ad2antrr	$⊢ ((((φ \land z \in P) \land (B \in (A I z) \land A \underset{˙}{-} z = C \underset{˙}{-} D)) \land y \in P) \land ⟨“ A z B ”⟩ \sim_{𝒢} (G) ⟨“ C D y ”⟩) \to A \in P$
63	54	ad2antrr	$⊢ ((((φ \land z \in P) \land (B \in (A I z) \land A \underset{˙}{-} z = C \underset{˙}{-} D)) \land y \in P) \land ⟨“ A z B ”⟩ \sim_{𝒢} (G) ⟨“ C D y ”⟩) \to B \in P$
64	53	ad2antrr	$⊢ ((((φ \land z \in P) \land (B \in (A I z) \land A \underset{˙}{-} z = C \underset{˙}{-} D)) \land y \in P) \land ⟨“ A z B ”⟩ \sim_{𝒢} (G) ⟨“ C D y ”⟩) \to z \in P$
65	55	ad2antrr	$⊢ ((((φ \land z \in P) \land (B \in (A I z) \land A \underset{˙}{-} z = C \underset{˙}{-} D)) \land y \in P) \land ⟨“ A z B ”⟩ \sim_{𝒢} (G) ⟨“ C D y ”⟩) \to C \in P$
66		simplr	$⊢ ((((φ \land z \in P) \land (B \in (A I z) \land A \underset{˙}{-} z = C \underset{˙}{-} D)) \land y \in P) \land ⟨“ A z B ”⟩ \sim_{𝒢} (G) ⟨“ C D y ”⟩) \to y \in P$
67	56	ad2antrr	$⊢ ((((φ \land z \in P) \land (B \in (A I z) \land A \underset{˙}{-} z = C \underset{˙}{-} D)) \land y \in P) \land ⟨“ A z B ”⟩ \sim_{𝒢} (G) ⟨“ C D y ”⟩) \to D \in P$
68		simpr	$⊢ ((((φ \land z \in P) \land (B \in (A I z) \land A \underset{˙}{-} z = C \underset{˙}{-} D)) \land y \in P) \land ⟨“ A z B ”⟩ \sim_{𝒢} (G) ⟨“ C D y ”⟩) \to ⟨“ A z B ”⟩ \sim_{𝒢} (G) ⟨“ C D y ”⟩$
69	1 2 3 16 61 62 64 63 65 67 66 68	cgr3swap23	$⊢ ((((φ \land z \in P) \land (B \in (A I z) \land A \underset{˙}{-} z = C \underset{˙}{-} D)) \land y \in P) \land ⟨“ A z B ”⟩ \sim_{𝒢} (G) ⟨“ C D y ”⟩) \to ⟨“ A B z ”⟩ \sim_{𝒢} (G) ⟨“ C y D ”⟩$
70		simpllr	$⊢ ((((φ \land z \in P) \land (B \in (A I z) \land A \underset{˙}{-} z = C \underset{˙}{-} D)) \land y \in P) \land ⟨“ A z B ”⟩ \sim_{𝒢} (G) ⟨“ C D y ”⟩) \to (B \in (A I z) \land A \underset{˙}{-} z = C \underset{˙}{-} D)$
71	70	simpld	$⊢ ((((φ \land z \in P) \land (B \in (A I z) \land A \underset{˙}{-} z = C \underset{˙}{-} D)) \land y \in P) \land ⟨“ A z B ”⟩ \sim_{𝒢} (G) ⟨“ C D y ”⟩) \to B \in (A I z)$
72	1 2 3 16 61 62 63 64 65 66 67 69 71	tgbtwnxfr	$⊢ ((((φ \land z \in P) \land (B \in (A I z) \land A \underset{˙}{-} z = C \underset{˙}{-} D)) \land y \in P) \land ⟨“ A z B ”⟩ \sim_{𝒢} (G) ⟨“ C D y ”⟩) \to y \in (C I D)$
73	1 2 3 16 61 62 64 63 65 67 66 68	cgr3simp3	$⊢ ((((φ \land z \in P) \land (B \in (A I z) \land A \underset{˙}{-} z = C \underset{˙}{-} D)) \land y \in P) \land ⟨“ A z B ”⟩ \sim_{𝒢} (G) ⟨“ C D y ”⟩) \to B \underset{˙}{-} A = y \underset{˙}{-} C$
74	1 2 3 61 63 62 66 65 73	tgcgrcomlr	$⊢ ((((φ \land z \in P) \land (B \in (A I z) \land A \underset{˙}{-} z = C \underset{˙}{-} D)) \land y \in P) \land ⟨“ A z B ”⟩ \sim_{𝒢} (G) ⟨“ C D y ”⟩) \to A \underset{˙}{-} B = C \underset{˙}{-} y$
75	72 74	jca	$⊢ ((((φ \land z \in P) \land (B \in (A I z) \land A \underset{˙}{-} z = C \underset{˙}{-} D)) \land y \in P) \land ⟨“ A z B ”⟩ \sim_{𝒢} (G) ⟨“ C D y ”⟩) \to (y \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} y)$
76	75	ex	$⊢ (((φ \land z \in P) \land (B \in (A I z) \land A \underset{˙}{-} z = C \underset{˙}{-} D)) \land y \in P) \to (⟨“ A z B ”⟩ \sim_{𝒢} (G) ⟨“ C D y ”⟩ \to (y \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} y))$
77	76	reximdva	$⊢ ((φ \land z \in P) \land (B \in (A I z) \land A \underset{˙}{-} z = C \underset{˙}{-} D)) \to (\exists y \in P ⟨“ A z B ”⟩ \sim_{𝒢} (G) ⟨“ C D y ”⟩ \to \exists y \in P (y \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} y))$
78	60 77	mpd	$⊢ ((φ \land z \in P) \land (B \in (A I z) \land A \underset{˙}{-} z = C \underset{˙}{-} D)) \to \exists y \in P (y \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} y)$
79	78	adantllr	$⊢ (((φ \land \exists x \in P (B \in (A I x) \land A \underset{˙}{-} x = C \underset{˙}{-} D)) \land z \in P) \land (B \in (A I z) \land A \underset{˙}{-} z = C \underset{˙}{-} D)) \to \exists y \in P (y \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} y)$
80		simpr	$⊢ (φ \land \exists x \in P (B \in (A I x) \land A \underset{˙}{-} x = C \underset{˙}{-} D)) \to \exists x \in P (B \in (A I x) \land A \underset{˙}{-} x = C \underset{˙}{-} D)$
81		oveq2	$⊢ x = z \to A I x = A I z$
82	81	eleq2d	$⊢ x = z \to (B \in (A I x) \leftrightarrow B \in (A I z))$
83		oveq2	$⊢ x = z \to A \underset{˙}{-} x = A \underset{˙}{-} z$
84	83	eqeq1d	$⊢ x = z \to (A \underset{˙}{-} x = C \underset{˙}{-} D \leftrightarrow A \underset{˙}{-} z = C \underset{˙}{-} D)$
85	82 84	anbi12d	$⊢ x = z \to ((B \in (A I x) \land A \underset{˙}{-} x = C \underset{˙}{-} D) \leftrightarrow (B \in (A I z) \land A \underset{˙}{-} z = C \underset{˙}{-} D))$
86	85	cbvrexvw	$⊢ \exists x \in P (B \in (A I x) \land A \underset{˙}{-} x = C \underset{˙}{-} D) \leftrightarrow \exists z \in P (B \in (A I z) \land A \underset{˙}{-} z = C \underset{˙}{-} D)$
87	80 86	sylib	$⊢ (φ \land \exists x \in P (B \in (A I x) \land A \underset{˙}{-} x = C \underset{˙}{-} D)) \to \exists z \in P (B \in (A I z) \land A \underset{˙}{-} z = C \underset{˙}{-} D)$
88	79 87	r19.29a	$⊢ (φ \land \exists x \in P (B \in (A I x) \land A \underset{˙}{-} x = C \underset{˙}{-} D)) \to \exists y \in P (y \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} y)$
89	50 88	impbida	$⊢ φ \to (\exists y \in P (y \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} y) \leftrightarrow \exists x \in P (B \in (A I x) \land A \underset{˙}{-} x = C \underset{˙}{-} D))$
90	10 89	bitrd	$⊢ φ \to ((A \underset{˙}{-} B) \underset{˙}{\leq} (C \underset{˙}{-} D) \leftrightarrow \exists x \in P (B \in (A I x) \land A \underset{˙}{-} x = C \underset{˙}{-} D))$

Metamath Proof Explorer

Theorem legov2

Proof