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 ( ( 𝐴 ∈ LinesEE ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑄 ) → 𝐴 = ( 𝑃 Line 𝑄 ) )

Proof

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