idinside

Description: Law for finding a point inside a segment. Theorem 4.19 of Schwabhauser p. 38. (Contributed by Scott Fenton, 7-Oct-2013)

		Ref	Expression
	Assertion	idinside	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to ((C Btwn ⟨A, B⟩ \land ⟨A, C⟩ Cgr ⟨A, D⟩ \land ⟨B, C⟩ Cgr ⟨B, D⟩) \to C = D)$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to N \in ℕ$
2		simp3l	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to C \in 𝔼 (N)$
3		simp3r	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to D \in 𝔼 (N)$
4		cgrid2	$⊢ (N \in ℕ \land (C \in 𝔼 (N) \land C \in 𝔼 (N) \land D \in 𝔼 (N))) \to (⟨C, C⟩ Cgr ⟨C, D⟩ \to C = D)$
5	1 2 2 3 4	syl13anc	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to (⟨C, C⟩ Cgr ⟨C, D⟩ \to C = D)$
6		simp2l	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to A \in 𝔼 (N)$
7		axbtwnid	$⊢ (N \in ℕ \land C \in 𝔼 (N) \land A \in 𝔼 (N)) \to (C Btwn ⟨A, A⟩ \to C = A)$
8	1 2 6 7	syl3anc	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to (C Btwn ⟨A, A⟩ \to C = A)$
9		opeq1	$⊢ C = A \to ⟨C, C⟩ = ⟨A, C⟩$
10		opeq1	$⊢ C = A \to ⟨C, D⟩ = ⟨A, D⟩$
11	9 10	breq12d	$⊢ C = A \to (⟨C, C⟩ Cgr ⟨C, D⟩ \leftrightarrow ⟨A, C⟩ Cgr ⟨A, D⟩)$
12	11	imbi1d	$⊢ C = A \to ((⟨C, C⟩ Cgr ⟨C, D⟩ \to C = D) \leftrightarrow (⟨A, C⟩ Cgr ⟨A, D⟩ \to C = D))$
13	12	biimpcd	$⊢ (⟨C, C⟩ Cgr ⟨C, D⟩ \to C = D) \to (C = A \to (⟨A, C⟩ Cgr ⟨A, D⟩ \to C = D))$
14		ax-1	$⊢ C = D \to (⟨B, C⟩ Cgr ⟨B, D⟩ \to C = D)$
15	13 14	syl8	$⊢ (⟨C, C⟩ Cgr ⟨C, D⟩ \to C = D) \to (C = A \to (⟨A, C⟩ Cgr ⟨A, D⟩ \to (⟨B, C⟩ Cgr ⟨B, D⟩ \to C = D)))$
16	5 8 15	sylsyld	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to (C Btwn ⟨A, A⟩ \to (⟨A, C⟩ Cgr ⟨A, D⟩ \to (⟨B, C⟩ Cgr ⟨B, D⟩ \to C = D)))$
17	16	3impd	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to ((C Btwn ⟨A, A⟩ \land ⟨A, C⟩ Cgr ⟨A, D⟩ \land ⟨B, C⟩ Cgr ⟨B, D⟩) \to C = D)$
18		opeq2	$⊢ A = B \to ⟨A, A⟩ = ⟨A, B⟩$
19	18	breq2d	$⊢ A = B \to (C Btwn ⟨A, A⟩ \leftrightarrow C Btwn ⟨A, B⟩)$
20	19	3anbi1d	$⊢ A = B \to ((C Btwn ⟨A, A⟩ \land ⟨A, C⟩ Cgr ⟨A, D⟩ \land ⟨B, C⟩ Cgr ⟨B, D⟩) \leftrightarrow (C Btwn ⟨A, B⟩ \land ⟨A, C⟩ Cgr ⟨A, D⟩ \land ⟨B, C⟩ Cgr ⟨B, D⟩))$
21	20	imbi1d	$⊢ A = B \to (((C Btwn ⟨A, A⟩ \land ⟨A, C⟩ Cgr ⟨A, D⟩ \land ⟨B, C⟩ Cgr ⟨B, D⟩) \to C = D) \leftrightarrow ((C Btwn ⟨A, B⟩ \land ⟨A, C⟩ Cgr ⟨A, D⟩ \land ⟨B, C⟩ Cgr ⟨B, D⟩) \to C = D))$
22	17 21	syl5ib	$⊢ A = B \to ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to ((C Btwn ⟨A, B⟩ \land ⟨A, C⟩ Cgr ⟨A, D⟩ \land ⟨B, C⟩ Cgr ⟨B, D⟩) \to C = D))$
23		simpr1	$⊢ (A \neq B \land (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \to N \in ℕ$
24		simpr2l	$⊢ (A \neq B \land (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \to A \in 𝔼 (N)$
25		simpr2r	$⊢ (A \neq B \land (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \to B \in 𝔼 (N)$
26		simpr3l	$⊢ (A \neq B \land (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \to C \in 𝔼 (N)$
27		btwncolinear1	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N))) \to (C Btwn ⟨A, B⟩ \to A Colinear ⟨B, C⟩)$
28	23 24 25 26 27	syl13anc	$⊢ (A \neq B \land (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \to (C Btwn ⟨A, B⟩ \to A Colinear ⟨B, C⟩)$
29		idd	$⊢ (A \neq B \land (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \to (⟨A, C⟩ Cgr ⟨A, D⟩ \to ⟨A, C⟩ Cgr ⟨A, D⟩)$
30		idd	$⊢ (A \neq B \land (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \to (⟨B, C⟩ Cgr ⟨B, D⟩ \to ⟨B, C⟩ Cgr ⟨B, D⟩)$
31	28 29 30	3anim123d	$⊢ (A \neq B \land (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \to ((C Btwn ⟨A, B⟩ \land ⟨A, C⟩ Cgr ⟨A, D⟩ \land ⟨B, C⟩ Cgr ⟨B, D⟩) \to (A Colinear ⟨B, C⟩ \land ⟨A, C⟩ Cgr ⟨A, D⟩ \land ⟨B, C⟩ Cgr ⟨B, D⟩))$
32		simp1	$⊢ (A Colinear ⟨B, C⟩ \land ⟨A, C⟩ Cgr ⟨A, D⟩ \land ⟨B, C⟩ Cgr ⟨B, D⟩) \to A Colinear ⟨B, C⟩$
33	32	anim2i	$⊢ (A \neq B \land (A Colinear ⟨B, C⟩ \land ⟨A, C⟩ Cgr ⟨A, D⟩ \land ⟨B, C⟩ Cgr ⟨B, D⟩)) \to (A \neq B \land A Colinear ⟨B, C⟩)$
34		3simpc	$⊢ (A Colinear ⟨B, C⟩ \land ⟨A, C⟩ Cgr ⟨A, D⟩ \land ⟨B, C⟩ Cgr ⟨B, D⟩) \to (⟨A, C⟩ Cgr ⟨A, D⟩ \land ⟨B, C⟩ Cgr ⟨B, D⟩)$
35	34	adantl	$⊢ (A \neq B \land (A Colinear ⟨B, C⟩ \land ⟨A, C⟩ Cgr ⟨A, D⟩ \land ⟨B, C⟩ Cgr ⟨B, D⟩)) \to (⟨A, C⟩ Cgr ⟨A, D⟩ \land ⟨B, C⟩ Cgr ⟨B, D⟩)$
36	33 35	jca	$⊢ (A \neq B \land (A Colinear ⟨B, C⟩ \land ⟨A, C⟩ Cgr ⟨A, D⟩ \land ⟨B, C⟩ Cgr ⟨B, D⟩)) \to ((A \neq B \land A Colinear ⟨B, C⟩) \land (⟨A, C⟩ Cgr ⟨A, D⟩ \land ⟨B, C⟩ Cgr ⟨B, D⟩))$
37		lineid	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to (((A \neq B \land A Colinear ⟨B, C⟩) \land (⟨A, C⟩ Cgr ⟨A, D⟩ \land ⟨B, C⟩ Cgr ⟨B, D⟩)) \to C = D)$
38	36 37	syl5	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to ((A \neq B \land (A Colinear ⟨B, C⟩ \land ⟨A, C⟩ Cgr ⟨A, D⟩ \land ⟨B, C⟩ Cgr ⟨B, D⟩)) \to C = D)$
39	38	expd	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to (A \neq B \to ((A Colinear ⟨B, C⟩ \land ⟨A, C⟩ Cgr ⟨A, D⟩ \land ⟨B, C⟩ Cgr ⟨B, D⟩) \to C = D))$
40	39	impcom	$⊢ (A \neq B \land (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \to ((A Colinear ⟨B, C⟩ \land ⟨A, C⟩ Cgr ⟨A, D⟩ \land ⟨B, C⟩ Cgr ⟨B, D⟩) \to C = D)$
41	31 40	syld	$⊢ (A \neq B \land (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \to ((C Btwn ⟨A, B⟩ \land ⟨A, C⟩ Cgr ⟨A, D⟩ \land ⟨B, C⟩ Cgr ⟨B, D⟩) \to C = D)$
42	41	ex	$⊢ A \neq B \to ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to ((C Btwn ⟨A, B⟩ \land ⟨A, C⟩ Cgr ⟨A, D⟩ \land ⟨B, C⟩ Cgr ⟨B, D⟩) \to C = D))$
43	22 42	pm2.61ine	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to ((C Btwn ⟨A, B⟩ \land ⟨A, C⟩ Cgr ⟨A, D⟩ \land ⟨B, C⟩ Cgr ⟨B, D⟩) \to C = D)$

Metamath Proof Explorer

Theorem idinside

Proof