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		eleq1	$⊢ y = z \to (y \in (C I D) \leftrightarrow z \in (C I D))$
44		oveq2	$⊢ y = z \to C \underset{˙}{-} y = C \underset{˙}{-} z$
45	44	eqeq2d	$⊢ y = z \to (A \underset{˙}{-} B = C \underset{˙}{-} y \leftrightarrow A \underset{˙}{-} B = C \underset{˙}{-} z)$
46	43 45	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))$
47	46	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)$
48	47	bilani	$⊢ (φ \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)$
49	42 48	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)$
50	5	ad2antrr	$⊢ ((φ \land z \in P) \land (B \in (A I z) \land A \underset{˙}{-} z = C \underset{˙}{-} D)) \to G \in 𝒢_{Tarski}$
51	6	ad2antrr	$⊢ ((φ \land z \in P) \land (B \in (A I z) \land A \underset{˙}{-} z = C \underset{˙}{-} D)) \to A \in P$
52		simplr	$⊢ ((φ \land z \in P) \land (B \in (A I z) \land A \underset{˙}{-} z = C \underset{˙}{-} D)) \to z \in P$
53	7	ad2antrr	$⊢ ((φ \land z \in P) \land (B \in (A I z) \land A \underset{˙}{-} z = C \underset{˙}{-} D)) \to B \in P$
54	8	ad2antrr	$⊢ ((φ \land z \in P) \land (B \in (A I z) \land A \underset{˙}{-} z = C \underset{˙}{-} D)) \to C \in P$
55	9	ad2antrr	$⊢ ((φ \land z \in P) \land (B \in (A I z) \land A \underset{˙}{-} z = C \underset{˙}{-} D)) \to D \in P$
56		simprl	$⊢ ((φ \land z \in P) \land (B \in (A I z) \land A \underset{˙}{-} z = C \underset{˙}{-} D)) \to B \in (A I z)$
57	1 11 3 50 51 53 52 56	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)$
58		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$
59	1 11 3 50 51 52 53 16 54 55 2 57 58	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 ”⟩$
60	50	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}$
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 A \in P$
62	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 B \in P$
63	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 z \in P$
64	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 C \in P$
65		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$
66	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 D \in P$
67		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 ”⟩$
68	1 2 3 16 60 61 63 62 64 66 65 67	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 ”⟩$
69		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)$
70	69	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)$
71	1 2 3 16 60 61 62 63 64 65 66 68 70	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)$
72	1 2 3 16 60 61 63 62 64 66 65 67	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$
73	1 2 3 60 62 61 65 64 72	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$
74	71 73	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)$
75	74	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))$
76	75	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))$
77	59 76	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)$
78	77	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)$
79		oveq2	$⊢ x = z \to A I x = A I z$
80	79	eleq2d	$⊢ x = z \to (B \in (A I x) \leftrightarrow B \in (A I z))$
81		oveq2	$⊢ x = z \to A \underset{˙}{-} x = A \underset{˙}{-} z$
82	81	eqeq1d	$⊢ x = z \to (A \underset{˙}{-} x = C \underset{˙}{-} D \leftrightarrow A \underset{˙}{-} z = C \underset{˙}{-} D)$
83	80 82	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))$
84	83	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)$
85	84	bilani	$⊢ (φ \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)$
86	78 85	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)$
87	49 86	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))$
88	10 87	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