outsidele

Description: Relate OutsideOf to Seg<_ . Theorem 6.13 of Schwabhauser p. 45. (Contributed by Scott Fenton, 24-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

		Ref	Expression
	Assertion	outsidele	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \to (P OutsideOf ⟨A, B⟩ \to (⟨P, A⟩ {Seg}_{\leq} ⟨P, B⟩ \leftrightarrow A Btwn ⟨P, B⟩))$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \to N \in ℕ$
2		simpr1	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \to P \in 𝔼 (N)$
3		simpr2	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \to A \in 𝔼 (N)$
4		simpr3	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \to B \in 𝔼 (N)$
5		brsegle2	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N)) \land (P \in 𝔼 (N) \land B \in 𝔼 (N))) \to (⟨P, A⟩ {Seg}_{\leq} ⟨P, B⟩ \leftrightarrow \exists y \in 𝔼 (N) (A Btwn ⟨P, y⟩ \land ⟨P, y⟩ Cgr ⟨P, B⟩))$
6	1 2 3 2 4 5	syl122anc	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \to (⟨P, A⟩ {Seg}_{\leq} ⟨P, B⟩ \leftrightarrow \exists y \in 𝔼 (N) (A Btwn ⟨P, y⟩ \land ⟨P, y⟩ Cgr ⟨P, B⟩))$
7	6	adantr	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land P OutsideOf ⟨A, B⟩) \to (⟨P, A⟩ {Seg}_{\leq} ⟨P, B⟩ \leftrightarrow \exists y \in 𝔼 (N) (A Btwn ⟨P, y⟩ \land ⟨P, y⟩ Cgr ⟨P, B⟩))$
8		simprl	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land y \in 𝔼 (N)) \land (P OutsideOf ⟨A, B⟩ \land (A Btwn ⟨P, y⟩ \land ⟨P, y⟩ Cgr ⟨P, B⟩))) \to P OutsideOf ⟨A, B⟩$
9		outsideofcom	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \to (P OutsideOf ⟨A, B⟩ \leftrightarrow P OutsideOf ⟨B, A⟩)$
10	9	ad2antrr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land y \in 𝔼 (N)) \land (P OutsideOf ⟨A, B⟩ \land (A Btwn ⟨P, y⟩ \land ⟨P, y⟩ Cgr ⟨P, B⟩))) \to (P OutsideOf ⟨A, B⟩ \leftrightarrow P OutsideOf ⟨B, A⟩)$
11	8 10	mpbid	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land y \in 𝔼 (N)) \land (P OutsideOf ⟨A, B⟩ \land (A Btwn ⟨P, y⟩ \land ⟨P, y⟩ Cgr ⟨P, B⟩))) \to P OutsideOf ⟨B, A⟩$
12		simpll	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land y \in 𝔼 (N)) \to N \in ℕ$
13		simplr1	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land y \in 𝔼 (N)) \to P \in 𝔼 (N)$
14		simplr3	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land y \in 𝔼 (N)) \to B \in 𝔼 (N)$
15	12 13 14	cgrrflxd	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land y \in 𝔼 (N)) \to ⟨P, B⟩ Cgr ⟨P, B⟩$
16	15	adantr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land y \in 𝔼 (N)) \land (P OutsideOf ⟨A, B⟩ \land (A Btwn ⟨P, y⟩ \land ⟨P, y⟩ Cgr ⟨P, B⟩))) \to ⟨P, B⟩ Cgr ⟨P, B⟩$
17	11 16	jca	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land y \in 𝔼 (N)) \land (P OutsideOf ⟨A, B⟩ \land (A Btwn ⟨P, y⟩ \land ⟨P, y⟩ Cgr ⟨P, B⟩))) \to (P OutsideOf ⟨B, A⟩ \land ⟨P, B⟩ Cgr ⟨P, B⟩)$
18		simprrl	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land y \in 𝔼 (N)) \land (P OutsideOf ⟨A, B⟩ \land (A Btwn ⟨P, y⟩ \land ⟨P, y⟩ Cgr ⟨P, B⟩))) \to A Btwn ⟨P, y⟩$
19		simpr	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land y \in 𝔼 (N)) \to y \in 𝔼 (N)$
20		simplr2	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land y \in 𝔼 (N)) \to A \in 𝔼 (N)$
21		btwncolinear1	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land y \in 𝔼 (N) \land A \in 𝔼 (N))) \to (A Btwn ⟨P, y⟩ \to P Colinear ⟨y, A⟩)$
22	12 13 19 20 21	syl13anc	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land y \in 𝔼 (N)) \to (A Btwn ⟨P, y⟩ \to P Colinear ⟨y, A⟩)$
23	22	adantr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land y \in 𝔼 (N)) \land (P OutsideOf ⟨A, B⟩ \land (A Btwn ⟨P, y⟩ \land ⟨P, y⟩ Cgr ⟨P, B⟩))) \to (A Btwn ⟨P, y⟩ \to P Colinear ⟨y, A⟩)$
24	18 23	mpd	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land y \in 𝔼 (N)) \land (P OutsideOf ⟨A, B⟩ \land (A Btwn ⟨P, y⟩ \land ⟨P, y⟩ Cgr ⟨P, B⟩))) \to P Colinear ⟨y, A⟩$
25		outsidene1	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \to (P OutsideOf ⟨A, B⟩ \to A \neq P)$
26	25	ad2antrr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land y \in 𝔼 (N)) \land (P OutsideOf ⟨A, B⟩ \land (A Btwn ⟨P, y⟩ \land ⟨P, y⟩ Cgr ⟨P, B⟩))) \to (P OutsideOf ⟨A, B⟩ \to A \neq P)$
27	8 26	mpd	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land y \in 𝔼 (N)) \land (P OutsideOf ⟨A, B⟩ \land (A Btwn ⟨P, y⟩ \land ⟨P, y⟩ Cgr ⟨P, B⟩))) \to A \neq P$
28	27	neneqd	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land y \in 𝔼 (N)) \land (P OutsideOf ⟨A, B⟩ \land (A Btwn ⟨P, y⟩ \land ⟨P, y⟩ Cgr ⟨P, B⟩))) \to \neg A = P$
29		df-3an	$⊢ (P OutsideOf ⟨A, B⟩ \land (A Btwn ⟨P, y⟩ \land ⟨P, y⟩ Cgr ⟨P, B⟩) \land P Btwn ⟨y, A⟩) \leftrightarrow ((P OutsideOf ⟨A, B⟩ \land (A Btwn ⟨P, y⟩ \land ⟨P, y⟩ Cgr ⟨P, B⟩)) \land P Btwn ⟨y, A⟩)$
30		simpr2l	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land y \in 𝔼 (N)) \land (P OutsideOf ⟨A, B⟩ \land (A Btwn ⟨P, y⟩ \land ⟨P, y⟩ Cgr ⟨P, B⟩) \land P Btwn ⟨y, A⟩)) \to A Btwn ⟨P, y⟩$
31	12 20 13 19 30	btwncomand	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land y \in 𝔼 (N)) \land (P OutsideOf ⟨A, B⟩ \land (A Btwn ⟨P, y⟩ \land ⟨P, y⟩ Cgr ⟨P, B⟩) \land P Btwn ⟨y, A⟩)) \to A Btwn ⟨y, P⟩$
32		simpr3	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land y \in 𝔼 (N)) \land (P OutsideOf ⟨A, B⟩ \land (A Btwn ⟨P, y⟩ \land ⟨P, y⟩ Cgr ⟨P, B⟩) \land P Btwn ⟨y, A⟩)) \to P Btwn ⟨y, A⟩$
33		btwnswapid2	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land y \in 𝔼 (N) \land P \in 𝔼 (N))) \to ((A Btwn ⟨y, P⟩ \land P Btwn ⟨y, A⟩) \to A = P)$
34	12 20 19 13 33	syl13anc	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land y \in 𝔼 (N)) \to ((A Btwn ⟨y, P⟩ \land P Btwn ⟨y, A⟩) \to A = P)$
35	34	adantr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land y \in 𝔼 (N)) \land (P OutsideOf ⟨A, B⟩ \land (A Btwn ⟨P, y⟩ \land ⟨P, y⟩ Cgr ⟨P, B⟩) \land P Btwn ⟨y, A⟩)) \to ((A Btwn ⟨y, P⟩ \land P Btwn ⟨y, A⟩) \to A = P)$
36	31 32 35	mp2and	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land y \in 𝔼 (N)) \land (P OutsideOf ⟨A, B⟩ \land (A Btwn ⟨P, y⟩ \land ⟨P, y⟩ Cgr ⟨P, B⟩) \land P Btwn ⟨y, A⟩)) \to A = P$
37	29 36	sylan2br	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land y \in 𝔼 (N)) \land ((P OutsideOf ⟨A, B⟩ \land (A Btwn ⟨P, y⟩ \land ⟨P, y⟩ Cgr ⟨P, B⟩)) \land P Btwn ⟨y, A⟩)) \to A = P$
38	37	expr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land y \in 𝔼 (N)) \land (P OutsideOf ⟨A, B⟩ \land (A Btwn ⟨P, y⟩ \land ⟨P, y⟩ Cgr ⟨P, B⟩))) \to (P Btwn ⟨y, A⟩ \to A = P)$
39	28 38	mtod	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land y \in 𝔼 (N)) \land (P OutsideOf ⟨A, B⟩ \land (A Btwn ⟨P, y⟩ \land ⟨P, y⟩ Cgr ⟨P, B⟩))) \to \neg P Btwn ⟨y, A⟩$
40		broutsideof	$⊢ P OutsideOf ⟨y, A⟩ \leftrightarrow (P Colinear ⟨y, A⟩ \land \neg P Btwn ⟨y, A⟩)$
41	24 39 40	sylanbrc	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land y \in 𝔼 (N)) \land (P OutsideOf ⟨A, B⟩ \land (A Btwn ⟨P, y⟩ \land ⟨P, y⟩ Cgr ⟨P, B⟩))) \to P OutsideOf ⟨y, A⟩$
42		simprrr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land y \in 𝔼 (N)) \land (P OutsideOf ⟨A, B⟩ \land (A Btwn ⟨P, y⟩ \land ⟨P, y⟩ Cgr ⟨P, B⟩))) \to ⟨P, y⟩ Cgr ⟨P, B⟩$
43	41 42	jca	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land y \in 𝔼 (N)) \land (P OutsideOf ⟨A, B⟩ \land (A Btwn ⟨P, y⟩ \land ⟨P, y⟩ Cgr ⟨P, B⟩))) \to (P OutsideOf ⟨y, A⟩ \land ⟨P, y⟩ Cgr ⟨P, B⟩)$
44		outsideofeq	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land P \in 𝔼 (N)) \land (B \in 𝔼 (N) \land B \in 𝔼 (N) \land y \in 𝔼 (N))) \to (((P OutsideOf ⟨B, A⟩ \land ⟨P, B⟩ Cgr ⟨P, B⟩) \land (P OutsideOf ⟨y, A⟩ \land ⟨P, y⟩ Cgr ⟨P, B⟩)) \to B = y)$
45	12 13 20 13 14 14 19 44	syl133anc	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land y \in 𝔼 (N)) \to (((P OutsideOf ⟨B, A⟩ \land ⟨P, B⟩ Cgr ⟨P, B⟩) \land (P OutsideOf ⟨y, A⟩ \land ⟨P, y⟩ Cgr ⟨P, B⟩)) \to B = y)$
46	45	adantr	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land y \in 𝔼 (N)) \land (P OutsideOf ⟨A, B⟩ \land (A Btwn ⟨P, y⟩ \land ⟨P, y⟩ Cgr ⟨P, B⟩))) \to (((P OutsideOf ⟨B, A⟩ \land ⟨P, B⟩ Cgr ⟨P, B⟩) \land (P OutsideOf ⟨y, A⟩ \land ⟨P, y⟩ Cgr ⟨P, B⟩)) \to B = y)$
47	17 43 46	mp2and	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land y \in 𝔼 (N)) \land (P OutsideOf ⟨A, B⟩ \land (A Btwn ⟨P, y⟩ \land ⟨P, y⟩ Cgr ⟨P, B⟩))) \to B = y$
48		opeq2	$⊢ B = y \to ⟨P, B⟩ = ⟨P, y⟩$
49	48	breq2d	$⊢ B = y \to (A Btwn ⟨P, B⟩ \leftrightarrow A Btwn ⟨P, y⟩)$
50	18 49	syl5ibrcom	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land y \in 𝔼 (N)) \land (P OutsideOf ⟨A, B⟩ \land (A Btwn ⟨P, y⟩ \land ⟨P, y⟩ Cgr ⟨P, B⟩))) \to (B = y \to A Btwn ⟨P, B⟩)$
51	47 50	mpd	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land y \in 𝔼 (N)) \land (P OutsideOf ⟨A, B⟩ \land (A Btwn ⟨P, y⟩ \land ⟨P, y⟩ Cgr ⟨P, B⟩))) \to A Btwn ⟨P, B⟩$
52	51	an4s	$⊢ (((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land P OutsideOf ⟨A, B⟩) \land (y \in 𝔼 (N) \land (A Btwn ⟨P, y⟩ \land ⟨P, y⟩ Cgr ⟨P, B⟩))) \to A Btwn ⟨P, B⟩$
53	52	rexlimdvaa	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land P OutsideOf ⟨A, B⟩) \to (\exists y \in 𝔼 (N) (A Btwn ⟨P, y⟩ \land ⟨P, y⟩ Cgr ⟨P, B⟩) \to A Btwn ⟨P, B⟩)$
54	7 53	sylbid	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land P OutsideOf ⟨A, B⟩) \to (⟨P, A⟩ {Seg}_{\leq} ⟨P, B⟩ \to A Btwn ⟨P, B⟩)$
55		btwnsegle	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \to (A Btwn ⟨P, B⟩ \to ⟨P, A⟩ {Seg}_{\leq} ⟨P, B⟩)$
56	55	adantr	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land P OutsideOf ⟨A, B⟩) \to (A Btwn ⟨P, B⟩ \to ⟨P, A⟩ {Seg}_{\leq} ⟨P, B⟩)$
57	54 56	impbid	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \land P OutsideOf ⟨A, B⟩) \to (⟨P, A⟩ {Seg}_{\leq} ⟨P, B⟩ \leftrightarrow A Btwn ⟨P, B⟩)$
58	57	ex	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \to (P OutsideOf ⟨A, B⟩ \to (⟨P, A⟩ {Seg}_{\leq} ⟨P, B⟩ \leftrightarrow A Btwn ⟨P, B⟩))$

Metamath Proof Explorer

Theorem outsidele

Proof