# 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 𝑄 ) )