legtri3

Description: Equality from the less-than relationship. Proposition 5.9 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$
	legtri3.1	$⊢ φ \to (A \underset{˙}{-} B) \underset{˙}{\leq} (C \underset{˙}{-} D)$
	legtri3.2	$⊢ φ \to (C \underset{˙}{-} D) \underset{˙}{\leq} (A \underset{˙}{-} B)$
Assertion	legtri3	$⊢ φ \to A \underset{˙}{-} B = 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		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		legtri3.1	$⊢ φ \to (A \underset{˙}{-} B) \underset{˙}{\leq} (C \underset{˙}{-} D)$
11		legtri3.2	$⊢ φ \to (C \underset{˙}{-} D) \underset{˙}{\leq} (A \underset{˙}{-} B)$
12		simpllr	$⊢ ((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (D \in (C I y) \land C \underset{˙}{-} y = A \underset{˙}{-} B)) \to (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)$
13	12	simprd	$⊢ ((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (D \in (C I y) \land C \underset{˙}{-} y = A \underset{˙}{-} B)) \to A \underset{˙}{-} B = C \underset{˙}{-} x$
14	5	ad4antr	$⊢ ((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (D \in (C I y) \land C \underset{˙}{-} y = A \underset{˙}{-} B)) \to G \in 𝒢_{Tarski}$
15		simp-4r	$⊢ ((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (D \in (C I y) \land C \underset{˙}{-} y = A \underset{˙}{-} B)) \to x \in P$
16	9	ad4antr	$⊢ ((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (D \in (C I y) \land C \underset{˙}{-} y = A \underset{˙}{-} B)) \to D \in P$
17	8	ad4antr	$⊢ ((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (D \in (C I y) \land C \underset{˙}{-} y = A \underset{˙}{-} B)) \to C \in P$
18	12	simpld	$⊢ ((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (D \in (C I y) \land C \underset{˙}{-} y = A \underset{˙}{-} B)) \to x \in (C I D)$
19	1 2 3 14 17 15 16 18	tgbtwncom	$⊢ ((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (D \in (C I y) \land C \underset{˙}{-} y = A \underset{˙}{-} B)) \to x \in (D I C)$
20		simpr	$⊢ ((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (D \in (C I y) \land C \underset{˙}{-} y = A \underset{˙}{-} B)) \to (D \in (C I y) \land C \underset{˙}{-} y = A \underset{˙}{-} B)$
21	20	simpld	$⊢ ((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (D \in (C I y) \land C \underset{˙}{-} y = A \underset{˙}{-} B)) \to D \in (C I y)$
22		simplr	$⊢ ((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (D \in (C I y) \land C \underset{˙}{-} y = A \underset{˙}{-} B)) \to y \in P$
23	7	ad4antr	$⊢ ((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (D \in (C I y) \land C \underset{˙}{-} y = A \underset{˙}{-} B)) \to B \in P$
24	6	ad4antr	$⊢ ((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (D \in (C I y) \land C \underset{˙}{-} y = A \underset{˙}{-} B)) \to A \in P$
25	1 2 3 14 17 16 22 21	tgbtwncom	$⊢ ((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (D \in (C I y) \land C \underset{˙}{-} y = A \underset{˙}{-} B)) \to D \in (y I C)$
26	1 2 3 14 22 16 15 17 25 19	tgbtwnexch2	$⊢ ((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (D \in (C I y) \land C \underset{˙}{-} y = A \underset{˙}{-} B)) \to x \in (y I C)$
27	1 2 3 14 23 24	tgbtwntriv1	$⊢ ((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (D \in (C I y) \land C \underset{˙}{-} y = A \underset{˙}{-} B)) \to B \in (B I A)$
28	20	simprd	$⊢ ((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (D \in (C I y) \land C \underset{˙}{-} y = A \underset{˙}{-} B)) \to C \underset{˙}{-} y = A \underset{˙}{-} B$
29	1 2 3 14 17 22 24 23 28	tgcgrcomlr	$⊢ ((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (D \in (C I y) \land C \underset{˙}{-} y = A \underset{˙}{-} B)) \to y \underset{˙}{-} C = B \underset{˙}{-} A$
30	13	eqcomd	$⊢ ((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (D \in (C I y) \land C \underset{˙}{-} y = A \underset{˙}{-} B)) \to C \underset{˙}{-} x = A \underset{˙}{-} B$
31	1 2 3 14 17 15 24 23 30	tgcgrcomlr	$⊢ ((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (D \in (C I y) \land C \underset{˙}{-} y = A \underset{˙}{-} B)) \to x \underset{˙}{-} C = B \underset{˙}{-} A$
32	1 2 3 14 22 15 17 23 23 24 26 27 29 31	tgcgrsub	$⊢ ((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (D \in (C I y) \land C \underset{˙}{-} y = A \underset{˙}{-} B)) \to y \underset{˙}{-} x = B \underset{˙}{-} B$
33	1 2 3 14 22 15 23 32	axtgcgrid	$⊢ ((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (D \in (C I y) \land C \underset{˙}{-} y = A \underset{˙}{-} B)) \to y = x$
34	33	oveq2d	$⊢ ((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (D \in (C I y) \land C \underset{˙}{-} y = A \underset{˙}{-} B)) \to C I y = C I x$
35	21 34	eleqtrd	$⊢ ((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (D \in (C I y) \land C \underset{˙}{-} y = A \underset{˙}{-} B)) \to D \in (C I x)$
36	1 2 3 14 17 16 15 35	tgbtwncom	$⊢ ((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (D \in (C I y) \land C \underset{˙}{-} y = A \underset{˙}{-} B)) \to D \in (x I C)$
37	1 2 3 14 15 16 17 19 36	tgbtwnswapid	$⊢ ((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (D \in (C I y) \land C \underset{˙}{-} y = A \underset{˙}{-} B)) \to x = D$
38	37	oveq2d	$⊢ ((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (D \in (C I y) \land C \underset{˙}{-} y = A \underset{˙}{-} B)) \to C \underset{˙}{-} x = C \underset{˙}{-} D$
39	13 38	eqtrd	$⊢ ((((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \land y \in P) \land (D \in (C I y) \land C \underset{˙}{-} y = A \underset{˙}{-} B)) \to A \underset{˙}{-} B = C \underset{˙}{-} D$
40	1 2 3 4 5 8 9 6 7	legov2	$⊢ φ \to ((C \underset{˙}{-} D) \underset{˙}{\leq} (A \underset{˙}{-} B) \leftrightarrow \exists y \in P (D \in (C I y) \land C \underset{˙}{-} y = A \underset{˙}{-} B))$
41	11 40	mpbid	$⊢ φ \to \exists y \in P (D \in (C I y) \land C \underset{˙}{-} y = A \underset{˙}{-} B)$
42	41	ad2antrr	$⊢ ((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \to \exists y \in P (D \in (C I y) \land C \underset{˙}{-} y = A \underset{˙}{-} B)$
43	39 42	r19.29a	$⊢ ((φ \land x \in P) \land (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)) \to A \underset{˙}{-} B = C \underset{˙}{-} D$
44	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))$
45	10 44	mpbid	$⊢ φ \to \exists x \in P (x \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} x)$
46	43 45	r19.29a	$⊢ φ \to A \underset{˙}{-} B = C \underset{˙}{-} D$

Metamath Proof Explorer

Theorem legtri3

Proof