# Metamath Proof Explorer

## Theorem 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 ${⊢}\left({A}\in \mathrm{LinesEE}\wedge \left({P}\in {A}\wedge {Q}\in {A}\right)\wedge {P}\ne {Q}\right)\to {A}={P}\mathrm{Line}{Q}$

### Proof

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