segleantisym

Description: Antisymmetry law for segment comparison. Theorem 5.9 of Schwabhauser p. 42. (Contributed by Scott Fenton, 14-Oct-2013)

		Ref	Expression
	Assertion	segleantisym	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to ((⟨A, B⟩ {Seg}_{\leq} ⟨C, D⟩ \land ⟨C, D⟩ {Seg}_{\leq} ⟨A, B⟩) \to ⟨A, B⟩ Cgr ⟨C, D⟩)$

Proof

Step	Hyp	Ref	Expression
1		brsegle	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to (⟨A, B⟩ {Seg}_{\leq} ⟨C, D⟩ \leftrightarrow \exists y \in 𝔼 (N) (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩))$
2		brsegle2	$⊢ (N \in ℕ \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land (A \in 𝔼 (N) \land B \in 𝔼 (N))) \to (⟨C, D⟩ {Seg}_{\leq} ⟨A, B⟩ \leftrightarrow \exists t \in 𝔼 (N) (D Btwn ⟨C, t⟩ \land ⟨C, t⟩ Cgr ⟨A, B⟩))$
3	2	3com23	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to (⟨C, D⟩ {Seg}_{\leq} ⟨A, B⟩ \leftrightarrow \exists t \in 𝔼 (N) (D Btwn ⟨C, t⟩ \land ⟨C, t⟩ Cgr ⟨A, B⟩))$
4	1 3	anbi12d	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to ((⟨A, B⟩ {Seg}_{\leq} ⟨C, D⟩ \land ⟨C, D⟩ {Seg}_{\leq} ⟨A, B⟩) \leftrightarrow (\exists y \in 𝔼 (N) (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land \exists t \in 𝔼 (N) (D Btwn ⟨C, t⟩ \land ⟨C, t⟩ Cgr ⟨A, B⟩)))$
5		reeanv	$⊢ \exists y \in 𝔼 (N) \exists t \in 𝔼 (N) ((y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (D Btwn ⟨C, t⟩ \land ⟨C, t⟩ Cgr ⟨A, B⟩)) \leftrightarrow (\exists y \in 𝔼 (N) (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land \exists t \in 𝔼 (N) (D Btwn ⟨C, t⟩ \land ⟨C, t⟩ Cgr ⟨A, B⟩))$
6	4 5	bitr4di	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to ((⟨A, B⟩ {Seg}_{\leq} ⟨C, D⟩ \land ⟨C, D⟩ {Seg}_{\leq} ⟨A, B⟩) \leftrightarrow \exists y \in 𝔼 (N) \exists t \in 𝔼 (N) ((y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (D Btwn ⟨C, t⟩ \land ⟨C, t⟩ Cgr ⟨A, B⟩)))$
7		simpl1	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land (y \in 𝔼 (N) \land t \in 𝔼 (N))) \to N \in ℕ$
8		simpl3l	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land (y \in 𝔼 (N) \land t \in 𝔼 (N))) \to C \in 𝔼 (N)$
9		simprr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land (y \in 𝔼 (N) \land t \in 𝔼 (N))) \to t \in 𝔼 (N)$
10		simprl	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land (y \in 𝔼 (N) \land t \in 𝔼 (N))) \to y \in 𝔼 (N)$
11		simpl3r	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land (y \in 𝔼 (N) \land t \in 𝔼 (N))) \to D \in 𝔼 (N)$
12		simprll	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land (y \in 𝔼 (N) \land t \in 𝔼 (N))) \land ((y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (D Btwn ⟨C, t⟩ \land ⟨C, t⟩ Cgr ⟨A, B⟩))) \to y Btwn ⟨C, D⟩$
13		simprrl	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land (y \in 𝔼 (N) \land t \in 𝔼 (N))) \land ((y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (D Btwn ⟨C, t⟩ \land ⟨C, t⟩ Cgr ⟨A, B⟩))) \to D Btwn ⟨C, t⟩$
14	7 8 10 11 9 12 13	btwnexchand	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land (y \in 𝔼 (N) \land t \in 𝔼 (N))) \land ((y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (D Btwn ⟨C, t⟩ \land ⟨C, t⟩ Cgr ⟨A, B⟩))) \to y Btwn ⟨C, t⟩$
15		simpl2l	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land (y \in 𝔼 (N) \land t \in 𝔼 (N))) \to A \in 𝔼 (N)$
16		simpl2r	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land (y \in 𝔼 (N) \land t \in 𝔼 (N))) \to B \in 𝔼 (N)$
17		simprrr	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land (y \in 𝔼 (N) \land t \in 𝔼 (N))) \land ((y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (D Btwn ⟨C, t⟩ \land ⟨C, t⟩ Cgr ⟨A, B⟩))) \to ⟨C, t⟩ Cgr ⟨A, B⟩$
18		simprlr	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land (y \in 𝔼 (N) \land t \in 𝔼 (N))) \land ((y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (D Btwn ⟨C, t⟩ \land ⟨C, t⟩ Cgr ⟨A, B⟩))) \to ⟨A, B⟩ Cgr ⟨C, y⟩$
19	7 8 9 15 16 8 10 17 18	cgrtrand	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land (y \in 𝔼 (N) \land t \in 𝔼 (N))) \land ((y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (D Btwn ⟨C, t⟩ \land ⟨C, t⟩ Cgr ⟨A, B⟩))) \to ⟨C, t⟩ Cgr ⟨C, y⟩$
20	7 8 9 10 14 19	endofsegidand	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land (y \in 𝔼 (N) \land t \in 𝔼 (N))) \land ((y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (D Btwn ⟨C, t⟩ \land ⟨C, t⟩ Cgr ⟨A, B⟩))) \to t = y$
21		opeq2	$⊢ t = y \to ⟨C, t⟩ = ⟨C, y⟩$
22	21	breq2d	$⊢ t = y \to (D Btwn ⟨C, t⟩ \leftrightarrow D Btwn ⟨C, y⟩)$
23	21	breq1d	$⊢ t = y \to (⟨C, t⟩ Cgr ⟨A, B⟩ \leftrightarrow ⟨C, y⟩ Cgr ⟨A, B⟩)$
24	22 23	anbi12d	$⊢ t = y \to ((D Btwn ⟨C, t⟩ \land ⟨C, t⟩ Cgr ⟨A, B⟩) \leftrightarrow (D Btwn ⟨C, y⟩ \land ⟨C, y⟩ Cgr ⟨A, B⟩))$
25	24	anbi2d	$⊢ t = y \to (((y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (D Btwn ⟨C, t⟩ \land ⟨C, t⟩ Cgr ⟨A, B⟩)) \leftrightarrow ((y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (D Btwn ⟨C, y⟩ \land ⟨C, y⟩ Cgr ⟨A, B⟩)))$
26	25	anbi2d	$⊢ t = y \to ((((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land (y \in 𝔼 (N) \land t \in 𝔼 (N))) \land ((y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (D Btwn ⟨C, t⟩ \land ⟨C, t⟩ Cgr ⟨A, B⟩))) \leftrightarrow (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land (y \in 𝔼 (N) \land t \in 𝔼 (N))) \land ((y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (D Btwn ⟨C, y⟩ \land ⟨C, y⟩ Cgr ⟨A, B⟩))))$
27		simprrl	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land (y \in 𝔼 (N) \land t \in 𝔼 (N))) \land ((y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (D Btwn ⟨C, y⟩ \land ⟨C, y⟩ Cgr ⟨A, B⟩))) \to D Btwn ⟨C, y⟩$
28	7 11 8 10 27	btwncomand	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land (y \in 𝔼 (N) \land t \in 𝔼 (N))) \land ((y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (D Btwn ⟨C, y⟩ \land ⟨C, y⟩ Cgr ⟨A, B⟩))) \to D Btwn ⟨y, C⟩$
29		simprll	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land (y \in 𝔼 (N) \land t \in 𝔼 (N))) \land ((y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (D Btwn ⟨C, y⟩ \land ⟨C, y⟩ Cgr ⟨A, B⟩))) \to y Btwn ⟨C, D⟩$
30	7 10 8 11 29	btwncomand	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land (y \in 𝔼 (N) \land t \in 𝔼 (N))) \land ((y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (D Btwn ⟨C, y⟩ \land ⟨C, y⟩ Cgr ⟨A, B⟩))) \to y Btwn ⟨D, C⟩$
31		btwnswapid	$⊢ (N \in ℕ \land (D \in 𝔼 (N) \land y \in 𝔼 (N) \land C \in 𝔼 (N))) \to ((D Btwn ⟨y, C⟩ \land y Btwn ⟨D, C⟩) \to D = y)$
32	7 11 10 8 31	syl13anc	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land (y \in 𝔼 (N) \land t \in 𝔼 (N))) \to ((D Btwn ⟨y, C⟩ \land y Btwn ⟨D, C⟩) \to D = y)$
33	32	adantr	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land (y \in 𝔼 (N) \land t \in 𝔼 (N))) \land ((y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (D Btwn ⟨C, y⟩ \land ⟨C, y⟩ Cgr ⟨A, B⟩))) \to ((D Btwn ⟨y, C⟩ \land y Btwn ⟨D, C⟩) \to D = y)$
34	28 30 33	mp2and	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land (y \in 𝔼 (N) \land t \in 𝔼 (N))) \land ((y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (D Btwn ⟨C, y⟩ \land ⟨C, y⟩ Cgr ⟨A, B⟩))) \to D = y$
35		simprlr	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land (y \in 𝔼 (N) \land t \in 𝔼 (N))) \land ((y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (D Btwn ⟨C, y⟩ \land ⟨C, y⟩ Cgr ⟨A, B⟩))) \to ⟨A, B⟩ Cgr ⟨C, y⟩$
36		opeq2	$⊢ D = y \to ⟨C, D⟩ = ⟨C, y⟩$
37	36	breq2d	$⊢ D = y \to (⟨A, B⟩ Cgr ⟨C, D⟩ \leftrightarrow ⟨A, B⟩ Cgr ⟨C, y⟩)$
38	35 37	syl5ibrcom	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land (y \in 𝔼 (N) \land t \in 𝔼 (N))) \land ((y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (D Btwn ⟨C, y⟩ \land ⟨C, y⟩ Cgr ⟨A, B⟩))) \to (D = y \to ⟨A, B⟩ Cgr ⟨C, D⟩)$
39	34 38	mpd	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land (y \in 𝔼 (N) \land t \in 𝔼 (N))) \land ((y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (D Btwn ⟨C, y⟩ \land ⟨C, y⟩ Cgr ⟨A, B⟩))) \to ⟨A, B⟩ Cgr ⟨C, D⟩$
40	26 39	syl6bi	$⊢ t = y \to ((((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land (y \in 𝔼 (N) \land t \in 𝔼 (N))) \land ((y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (D Btwn ⟨C, t⟩ \land ⟨C, t⟩ Cgr ⟨A, B⟩))) \to ⟨A, B⟩ Cgr ⟨C, D⟩)$
41	20 40	mpcom	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land (y \in 𝔼 (N) \land t \in 𝔼 (N))) \land ((y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (D Btwn ⟨C, t⟩ \land ⟨C, t⟩ Cgr ⟨A, B⟩))) \to ⟨A, B⟩ Cgr ⟨C, D⟩$
42	41	exp31	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to ((y \in 𝔼 (N) \land t \in 𝔼 (N)) \to (((y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (D Btwn ⟨C, t⟩ \land ⟨C, t⟩ Cgr ⟨A, B⟩)) \to ⟨A, B⟩ Cgr ⟨C, D⟩))$
43	42	rexlimdvv	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to (\exists y \in 𝔼 (N) \exists t \in 𝔼 (N) ((y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (D Btwn ⟨C, t⟩ \land ⟨C, t⟩ Cgr ⟨A, B⟩)) \to ⟨A, B⟩ Cgr ⟨C, D⟩)$
44	6 43	sylbid	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to ((⟨A, B⟩ {Seg}_{\leq} ⟨C, D⟩ \land ⟨C, D⟩ {Seg}_{\leq} ⟨A, B⟩) \to ⟨A, B⟩ Cgr ⟨C, D⟩)$

Metamath Proof Explorer

Theorem segleantisym

Proof