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

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