linethru

Description: If A is a line containing two distinct points P and Q , then A is the line through P and Q . Theorem 6.18 of Schwabhauser p. 45. (Contributed by Scott Fenton, 28-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

		Ref	Expression
	Assertion	linethru	$⊢ (A \in LinesEE \land (P \in A \land Q \in A) \land P \neq Q) \to A = P Line Q$

Proof

Step	Hyp	Ref	Expression
1		ellines	$⊢ A \in LinesEE \leftrightarrow \exists n \in ℕ \exists a \in 𝔼 (n) \exists b \in 𝔼 (n) (a \neq b \land A = a Line b)$
2		simpll1	$⊢ (((n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \land a \neq b) \land ((P \in (a Line b) \land Q \in (a Line b)) \land P \neq Q)) \to n \in ℕ$
3		simpll2	$⊢ (((n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \land a \neq b) \land ((P \in (a Line b) \land Q \in (a Line b)) \land P \neq Q)) \to a \in 𝔼 (n)$
4		simpll3	$⊢ (((n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \land a \neq b) \land ((P \in (a Line b) \land Q \in (a Line b)) \land P \neq Q)) \to b \in 𝔼 (n)$
5		simplr	$⊢ (((n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \land a \neq b) \land ((P \in (a Line b) \land Q \in (a Line b)) \land P \neq Q)) \to a \neq b$
6		liness	$⊢ (n \in ℕ \land (a \in 𝔼 (n) \land b \in 𝔼 (n) \land a \neq b)) \to a Line b \subseteq 𝔼 (n)$
7	2 3 4 5 6	syl13anc	$⊢ (((n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \land a \neq b) \land ((P \in (a Line b) \land Q \in (a Line b)) \land P \neq Q)) \to a Line b \subseteq 𝔼 (n)$
8		simprll	$⊢ (((n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \land a \neq b) \land ((P \in (a Line b) \land Q \in (a Line b)) \land P \neq Q)) \to P \in (a Line b)$
9	7 8	sseldd	$⊢ (((n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \land a \neq b) \land ((P \in (a Line b) \land Q \in (a Line b)) \land P \neq Q)) \to P \in 𝔼 (n)$
10		simprlr	$⊢ (((n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \land a \neq b) \land ((P \in (a Line b) \land Q \in (a Line b)) \land P \neq Q)) \to Q \in (a Line b)$
11	7 10	sseldd	$⊢ (((n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \land a \neq b) \land ((P \in (a Line b) \land Q \in (a Line b)) \land P \neq Q)) \to Q \in 𝔼 (n)$
12		simplll	$⊢ (((P \in (a Line b) \land Q \in (a Line b)) \land P \neq a) \land (P \in 𝔼 (n) \land Q \in 𝔼 (n))) \to P \in (a Line b)$
13	12	adantl	$⊢ (((n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \land a \neq b) \land (((P \in (a Line b) \land Q \in (a Line b)) \land P \neq a) \land (P \in 𝔼 (n) \land Q \in 𝔼 (n)))) \to P \in (a Line b)$
14		simpll1	$⊢ (((n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \land a \neq b) \land (((P \in (a Line b) \land Q \in (a Line b)) \land P \neq a) \land (P \in 𝔼 (n) \land Q \in 𝔼 (n)))) \to n \in ℕ$
15		simpll2	$⊢ (((n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \land a \neq b) \land (((P \in (a Line b) \land Q \in (a Line b)) \land P \neq a) \land (P \in 𝔼 (n) \land Q \in 𝔼 (n)))) \to a \in 𝔼 (n)$
16		simpll3	$⊢ (((n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \land a \neq b) \land (((P \in (a Line b) \land Q \in (a Line b)) \land P \neq a) \land (P \in 𝔼 (n) \land Q \in 𝔼 (n)))) \to b \in 𝔼 (n)$
17		simplr	$⊢ (((n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \land a \neq b) \land (((P \in (a Line b) \land Q \in (a Line b)) \land P \neq a) \land (P \in 𝔼 (n) \land Q \in 𝔼 (n)))) \to a \neq b$
18		simprrl	$⊢ (((n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \land a \neq b) \land (((P \in (a Line b) \land Q \in (a Line b)) \land P \neq a) \land (P \in 𝔼 (n) \land Q \in 𝔼 (n)))) \to P \in 𝔼 (n)$
19		simprlr	$⊢ (((n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \land a \neq b) \land (((P \in (a Line b) \land Q \in (a Line b)) \land P \neq a) \land (P \in 𝔼 (n) \land Q \in 𝔼 (n)))) \to P \neq a$
20	19	necomd	$⊢ (((n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \land a \neq b) \land (((P \in (a Line b) \land Q \in (a Line b)) \land P \neq a) \land (P \in 𝔼 (n) \land Q \in 𝔼 (n)))) \to a \neq P$
21		lineelsb2	$⊢ (n \in ℕ \land (a \in 𝔼 (n) \land b \in 𝔼 (n) \land a \neq b) \land (P \in 𝔼 (n) \land a \neq P)) \to (P \in (a Line b) \to a Line b = a Line P)$
22	14 15 16 17 18 20 21	syl132anc	$⊢ (((n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \land a \neq b) \land (((P \in (a Line b) \land Q \in (a Line b)) \land P \neq a) \land (P \in 𝔼 (n) \land Q \in 𝔼 (n)))) \to (P \in (a Line b) \to a Line b = a Line P)$
23	13 22	mpd	$⊢ (((n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \land a \neq b) \land (((P \in (a Line b) \land Q \in (a Line b)) \land P \neq a) \land (P \in 𝔼 (n) \land Q \in 𝔼 (n)))) \to a Line b = a Line P$
24		linecom	$⊢ (n \in ℕ \land (a \in 𝔼 (n) \land P \in 𝔼 (n) \land a \neq P)) \to a Line P = P Line a$
25	14 15 18 20 24	syl13anc	$⊢ (((n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \land a \neq b) \land (((P \in (a Line b) \land Q \in (a Line b)) \land P \neq a) \land (P \in 𝔼 (n) \land Q \in 𝔼 (n)))) \to a Line P = P Line a$
26	23 25	eqtrd	$⊢ (((n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \land a \neq b) \land (((P \in (a Line b) \land Q \in (a Line b)) \land P \neq a) \land (P \in 𝔼 (n) \land Q \in 𝔼 (n)))) \to a Line b = P Line a$
27		neeq2	$⊢ Q = a \to (P \neq Q \leftrightarrow P \neq a)$
28	27	anbi2d	$⊢ Q = a \to (((P \in (a Line b) \land Q \in (a Line b)) \land P \neq Q) \leftrightarrow ((P \in (a Line b) \land Q \in (a Line b)) \land P \neq a))$
29	28	anbi1d	$⊢ Q = a \to ((((P \in (a Line b) \land Q \in (a Line b)) \land P \neq Q) \land (P \in 𝔼 (n) \land Q \in 𝔼 (n))) \leftrightarrow (((P \in (a Line b) \land Q \in (a Line b)) \land P \neq a) \land (P \in 𝔼 (n) \land Q \in 𝔼 (n))))$
30	29	anbi2d	$⊢ Q = a \to ((((n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \land a \neq b) \land (((P \in (a Line b) \land Q \in (a Line b)) \land P \neq Q) \land (P \in 𝔼 (n) \land Q \in 𝔼 (n)))) \leftrightarrow (((n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \land a \neq b) \land (((P \in (a Line b) \land Q \in (a Line b)) \land P \neq a) \land (P \in 𝔼 (n) \land Q \in 𝔼 (n)))))$
31		oveq2	$⊢ Q = a \to P Line Q = P Line a$
32	31	eqeq2d	$⊢ Q = a \to (a Line b = P Line Q \leftrightarrow a Line b = P Line a)$
33	30 32	imbi12d	$⊢ Q = a \to (((((n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \land a \neq b) \land (((P \in (a Line b) \land Q \in (a Line b)) \land P \neq Q) \land (P \in 𝔼 (n) \land Q \in 𝔼 (n)))) \to a Line b = P Line Q) \leftrightarrow ((((n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \land a \neq b) \land (((P \in (a Line b) \land Q \in (a Line b)) \land P \neq a) \land (P \in 𝔼 (n) \land Q \in 𝔼 (n)))) \to a Line b = P Line a))$
34	26 33	mpbiri	$⊢ Q = a \to ((((n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \land a \neq b) \land (((P \in (a Line b) \land Q \in (a Line b)) \land P \neq Q) \land (P \in 𝔼 (n) \land Q \in 𝔼 (n)))) \to a Line b = P Line Q)$
35		simp1	$⊢ (((n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \land a \neq b) \land (((P \in (a Line b) \land Q \in (a Line b)) \land P \neq Q) \land (P \in 𝔼 (n) \land Q \in 𝔼 (n))) \land Q \neq a) \to ((n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \land a \neq b)$
36		simp2l	$⊢ (((n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \land a \neq b) \land (((P \in (a Line b) \land Q \in (a Line b)) \land P \neq Q) \land (P \in 𝔼 (n) \land Q \in 𝔼 (n))) \land Q \neq a) \to ((P \in (a Line b) \land Q \in (a Line b)) \land P \neq Q)$
37	35 36 10	syl2anc	$⊢ (((n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \land a \neq b) \land (((P \in (a Line b) \land Q \in (a Line b)) \land P \neq Q) \land (P \in 𝔼 (n) \land Q \in 𝔼 (n))) \land Q \neq a) \to Q \in (a Line b)$
38		simp1l1	$⊢ (((n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \land a \neq b) \land (((P \in (a Line b) \land Q \in (a Line b)) \land P \neq Q) \land (P \in 𝔼 (n) \land Q \in 𝔼 (n))) \land Q \neq a) \to n \in ℕ$
39		simp1l2	$⊢ (((n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \land a \neq b) \land (((P \in (a Line b) \land Q \in (a Line b)) \land P \neq Q) \land (P \in 𝔼 (n) \land Q \in 𝔼 (n))) \land Q \neq a) \to a \in 𝔼 (n)$
40		simp1l3	$⊢ (((n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \land a \neq b) \land (((P \in (a Line b) \land Q \in (a Line b)) \land P \neq Q) \land (P \in 𝔼 (n) \land Q \in 𝔼 (n))) \land Q \neq a) \to b \in 𝔼 (n)$
41		simp1r	$⊢ (((n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \land a \neq b) \land (((P \in (a Line b) \land Q \in (a Line b)) \land P \neq Q) \land (P \in 𝔼 (n) \land Q \in 𝔼 (n))) \land Q \neq a) \to a \neq b$
42		simp2rr	$⊢ (((n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \land a \neq b) \land (((P \in (a Line b) \land Q \in (a Line b)) \land P \neq Q) \land (P \in 𝔼 (n) \land Q \in 𝔼 (n))) \land Q \neq a) \to Q \in 𝔼 (n)$
43		simp3	$⊢ (((n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \land a \neq b) \land (((P \in (a Line b) \land Q \in (a Line b)) \land P \neq Q) \land (P \in 𝔼 (n) \land Q \in 𝔼 (n))) \land Q \neq a) \to Q \neq a$
44	43	necomd	$⊢ (((n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \land a \neq b) \land (((P \in (a Line b) \land Q \in (a Line b)) \land P \neq Q) \land (P \in 𝔼 (n) \land Q \in 𝔼 (n))) \land Q \neq a) \to a \neq Q$
45		lineelsb2	$⊢ (n \in ℕ \land (a \in 𝔼 (n) \land b \in 𝔼 (n) \land a \neq b) \land (Q \in 𝔼 (n) \land a \neq Q)) \to (Q \in (a Line b) \to a Line b = a Line Q)$
46	38 39 40 41 42 44 45	syl132anc	$⊢ (((n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \land a \neq b) \land (((P \in (a Line b) \land Q \in (a Line b)) \land P \neq Q) \land (P \in 𝔼 (n) \land Q \in 𝔼 (n))) \land Q \neq a) \to (Q \in (a Line b) \to a Line b = a Line Q)$
47	37 46	mpd	$⊢ (((n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \land a \neq b) \land (((P \in (a Line b) \land Q \in (a Line b)) \land P \neq Q) \land (P \in 𝔼 (n) \land Q \in 𝔼 (n))) \land Q \neq a) \to a Line b = a Line Q$
48		linecom	$⊢ (n \in ℕ \land (a \in 𝔼 (n) \land Q \in 𝔼 (n) \land a \neq Q)) \to a Line Q = Q Line a$
49	38 39 42 44 48	syl13anc	$⊢ (((n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \land a \neq b) \land (((P \in (a Line b) \land Q \in (a Line b)) \land P \neq Q) \land (P \in 𝔼 (n) \land Q \in 𝔼 (n))) \land Q \neq a) \to a Line Q = Q Line a$
50	47 49	eqtrd	$⊢ (((n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \land a \neq b) \land (((P \in (a Line b) \land Q \in (a Line b)) \land P \neq Q) \land (P \in 𝔼 (n) \land Q \in 𝔼 (n))) \land Q \neq a) \to a Line b = Q Line a$
51	36	simplld	$⊢ (((n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \land a \neq b) \land (((P \in (a Line b) \land Q \in (a Line b)) \land P \neq Q) \land (P \in 𝔼 (n) \land Q \in 𝔼 (n))) \land Q \neq a) \to P \in (a Line b)$
52	51 50	eleqtrd	$⊢ (((n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \land a \neq b) \land (((P \in (a Line b) \land Q \in (a Line b)) \land P \neq Q) \land (P \in 𝔼 (n) \land Q \in 𝔼 (n))) \land Q \neq a) \to P \in (Q Line a)$
53		simp2rl	$⊢ (((n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \land a \neq b) \land (((P \in (a Line b) \land Q \in (a Line b)) \land P \neq Q) \land (P \in 𝔼 (n) \land Q \in 𝔼 (n))) \land Q \neq a) \to P \in 𝔼 (n)$
54		simp2lr	$⊢ (((n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \land a \neq b) \land (((P \in (a Line b) \land Q \in (a Line b)) \land P \neq Q) \land (P \in 𝔼 (n) \land Q \in 𝔼 (n))) \land Q \neq a) \to P \neq Q$
55	54	necomd	$⊢ (((n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \land a \neq b) \land (((P \in (a Line b) \land Q \in (a Line b)) \land P \neq Q) \land (P \in 𝔼 (n) \land Q \in 𝔼 (n))) \land Q \neq a) \to Q \neq P$
56		lineelsb2	$⊢ (n \in ℕ \land (Q \in 𝔼 (n) \land a \in 𝔼 (n) \land Q \neq a) \land (P \in 𝔼 (n) \land Q \neq P)) \to (P \in (Q Line a) \to Q Line a = Q Line P)$
57	38 42 39 43 53 55 56	syl132anc	$⊢ (((n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \land a \neq b) \land (((P \in (a Line b) \land Q \in (a Line b)) \land P \neq Q) \land (P \in 𝔼 (n) \land Q \in 𝔼 (n))) \land Q \neq a) \to (P \in (Q Line a) \to Q Line a = Q Line P)$
58	52 57	mpd	$⊢ (((n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \land a \neq b) \land (((P \in (a Line b) \land Q \in (a Line b)) \land P \neq Q) \land (P \in 𝔼 (n) \land Q \in 𝔼 (n))) \land Q \neq a) \to Q Line a = Q Line P$
59		linecom	$⊢ (n \in ℕ \land (Q \in 𝔼 (n) \land P \in 𝔼 (n) \land Q \neq P)) \to Q Line P = P Line Q$
60	38 42 53 55 59	syl13anc	$⊢ (((n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \land a \neq b) \land (((P \in (a Line b) \land Q \in (a Line b)) \land P \neq Q) \land (P \in 𝔼 (n) \land Q \in 𝔼 (n))) \land Q \neq a) \to Q Line P = P Line Q$
61	50 58 60	3eqtrd	$⊢ (((n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \land a \neq b) \land (((P \in (a Line b) \land Q \in (a Line b)) \land P \neq Q) \land (P \in 𝔼 (n) \land Q \in 𝔼 (n))) \land Q \neq a) \to a Line b = P Line Q$
62	61	3expa	$⊢ ((((n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \land a \neq b) \land (((P \in (a Line b) \land Q \in (a Line b)) \land P \neq Q) \land (P \in 𝔼 (n) \land Q \in 𝔼 (n)))) \land Q \neq a) \to a Line b = P Line Q$
63	62	expcom	$⊢ Q \neq a \to ((((n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \land a \neq b) \land (((P \in (a Line b) \land Q \in (a Line b)) \land P \neq Q) \land (P \in 𝔼 (n) \land Q \in 𝔼 (n)))) \to a Line b = P Line Q)$
64	34 63	pm2.61ine	$⊢ (((n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \land a \neq b) \land (((P \in (a Line b) \land Q \in (a Line b)) \land P \neq Q) \land (P \in 𝔼 (n) \land Q \in 𝔼 (n)))) \to a Line b = P Line Q$
65	64	expr	$⊢ (((n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \land a \neq b) \land ((P \in (a Line b) \land Q \in (a Line b)) \land P \neq Q)) \to ((P \in 𝔼 (n) \land Q \in 𝔼 (n)) \to a Line b = P Line Q)$
66	9 11 65	mp2and	$⊢ (((n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \land a \neq b) \land ((P \in (a Line b) \land Q \in (a Line b)) \land P \neq Q)) \to a Line b = P Line Q$
67	66	ex	$⊢ ((n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \land a \neq b) \to (((P \in (a Line b) \land Q \in (a Line b)) \land P \neq Q) \to a Line b = P Line Q)$
68		eleq2	$⊢ A = a Line b \to (P \in A \leftrightarrow P \in (a Line b))$
69		eleq2	$⊢ A = a Line b \to (Q \in A \leftrightarrow Q \in (a Line b))$
70	68 69	anbi12d	$⊢ A = a Line b \to ((P \in A \land Q \in A) \leftrightarrow (P \in (a Line b) \land Q \in (a Line b)))$
71	70	anbi1d	$⊢ A = a Line b \to (((P \in A \land Q \in A) \land P \neq Q) \leftrightarrow ((P \in (a Line b) \land Q \in (a Line b)) \land P \neq Q))$
72		eqeq1	$⊢ A = a Line b \to (A = P Line Q \leftrightarrow a Line b = P Line Q)$
73	71 72	imbi12d	$⊢ A = a Line b \to ((((P \in A \land Q \in A) \land P \neq Q) \to A = P Line Q) \leftrightarrow (((P \in (a Line b) \land Q \in (a Line b)) \land P \neq Q) \to a Line b = P Line Q))$
74	67 73	syl5ibrcom	$⊢ ((n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \land a \neq b) \to (A = a Line b \to (((P \in A \land Q \in A) \land P \neq Q) \to A = P Line Q))$
75	74	expimpd	$⊢ (n \in ℕ \land a \in 𝔼 (n) \land b \in 𝔼 (n)) \to ((a \neq b \land A = a Line b) \to (((P \in A \land Q \in A) \land P \neq Q) \to A = P Line Q))$
76	75	3expa	$⊢ ((n \in ℕ \land a \in 𝔼 (n)) \land b \in 𝔼 (n)) \to ((a \neq b \land A = a Line b) \to (((P \in A \land Q \in A) \land P \neq Q) \to A = P Line Q))$
77	76	rexlimdva	$⊢ (n \in ℕ \land a \in 𝔼 (n)) \to (\exists b \in 𝔼 (n) (a \neq b \land A = a Line b) \to (((P \in A \land Q \in A) \land P \neq Q) \to A = P Line Q))$
78	77	rexlimivv	$⊢ \exists n \in ℕ \exists a \in 𝔼 (n) \exists b \in 𝔼 (n) (a \neq b \land A = a Line b) \to (((P \in A \land Q \in A) \land P \neq Q) \to A = P Line Q)$
79	1 78	sylbi	$⊢ A \in LinesEE \to (((P \in A \land Q \in A) \land P \neq Q) \to A = P Line Q)$
80	79	3impib	$⊢ (A \in LinesEE \land (P \in A \land Q \in A) \land P \neq Q) \to A = P Line Q$

Metamath Proof Explorer

Theorem linethru

Proof