# Metamath Proof Explorer

## Theorem eulplig

Description: Through two distinct points of a planar incidence geometry, there is a unique line. (Contributed by BJ, 2-Dec-2021)

Ref Expression
Hypothesis eulplig.1 𝑃 = 𝐺
Assertion eulplig ( ( 𝐺 ∈ Plig ∧ ( ( 𝐴𝑃𝐵𝑃 ) ∧ 𝐴𝐵 ) ) → ∃! 𝑙𝐺 ( 𝐴𝑙𝐵𝑙 ) )

### Proof

Step Hyp Ref Expression
1 eulplig.1 𝑃 = 𝐺
2 1 isplig ( 𝐺 ∈ Plig → ( 𝐺 ∈ Plig ↔ ( ∀ 𝑎𝑃𝑏𝑃 ( 𝑎𝑏 → ∃! 𝑙𝐺 ( 𝑎𝑙𝑏𝑙 ) ) ∧ ∀ 𝑙𝐺𝑎𝑃𝑏𝑃 ( 𝑎𝑏𝑎𝑙𝑏𝑙 ) ∧ ∃ 𝑎𝑃𝑏𝑃𝑐𝑃𝑙𝐺 ¬ ( 𝑎𝑙𝑏𝑙𝑐𝑙 ) ) ) )
3 2 ibi ( 𝐺 ∈ Plig → ( ∀ 𝑎𝑃𝑏𝑃 ( 𝑎𝑏 → ∃! 𝑙𝐺 ( 𝑎𝑙𝑏𝑙 ) ) ∧ ∀ 𝑙𝐺𝑎𝑃𝑏𝑃 ( 𝑎𝑏𝑎𝑙𝑏𝑙 ) ∧ ∃ 𝑎𝑃𝑏𝑃𝑐𝑃𝑙𝐺 ¬ ( 𝑎𝑙𝑏𝑙𝑐𝑙 ) ) )
4 simp1 ( ( ∀ 𝑎𝑃𝑏𝑃 ( 𝑎𝑏 → ∃! 𝑙𝐺 ( 𝑎𝑙𝑏𝑙 ) ) ∧ ∀ 𝑙𝐺𝑎𝑃𝑏𝑃 ( 𝑎𝑏𝑎𝑙𝑏𝑙 ) ∧ ∃ 𝑎𝑃𝑏𝑃𝑐𝑃𝑙𝐺 ¬ ( 𝑎𝑙𝑏𝑙𝑐𝑙 ) ) → ∀ 𝑎𝑃𝑏𝑃 ( 𝑎𝑏 → ∃! 𝑙𝐺 ( 𝑎𝑙𝑏𝑙 ) ) )
5 simpl ( ( 𝑎 = 𝐴𝑏 = 𝐵 ) → 𝑎 = 𝐴 )
6 simpr ( ( 𝑎 = 𝐴𝑏 = 𝐵 ) → 𝑏 = 𝐵 )
7 5 6 neeq12d ( ( 𝑎 = 𝐴𝑏 = 𝐵 ) → ( 𝑎𝑏𝐴𝐵 ) )
8 eleq1 ( 𝑎 = 𝐴 → ( 𝑎𝑙𝐴𝑙 ) )
9 eleq1 ( 𝑏 = 𝐵 → ( 𝑏𝑙𝐵𝑙 ) )
10 8 9 bi2anan9 ( ( 𝑎 = 𝐴𝑏 = 𝐵 ) → ( ( 𝑎𝑙𝑏𝑙 ) ↔ ( 𝐴𝑙𝐵𝑙 ) ) )
11 10 reubidv ( ( 𝑎 = 𝐴𝑏 = 𝐵 ) → ( ∃! 𝑙𝐺 ( 𝑎𝑙𝑏𝑙 ) ↔ ∃! 𝑙𝐺 ( 𝐴𝑙𝐵𝑙 ) ) )
12 7 11 imbi12d ( ( 𝑎 = 𝐴𝑏 = 𝐵 ) → ( ( 𝑎𝑏 → ∃! 𝑙𝐺 ( 𝑎𝑙𝑏𝑙 ) ) ↔ ( 𝐴𝐵 → ∃! 𝑙𝐺 ( 𝐴𝑙𝐵𝑙 ) ) ) )
13 12 rspc2gv ( ( 𝐴𝑃𝐵𝑃 ) → ( ∀ 𝑎𝑃𝑏𝑃 ( 𝑎𝑏 → ∃! 𝑙𝐺 ( 𝑎𝑙𝑏𝑙 ) ) → ( 𝐴𝐵 → ∃! 𝑙𝐺 ( 𝐴𝑙𝐵𝑙 ) ) ) )
14 13 com23 ( ( 𝐴𝑃𝐵𝑃 ) → ( 𝐴𝐵 → ( ∀ 𝑎𝑃𝑏𝑃 ( 𝑎𝑏 → ∃! 𝑙𝐺 ( 𝑎𝑙𝑏𝑙 ) ) → ∃! 𝑙𝐺 ( 𝐴𝑙𝐵𝑙 ) ) ) )
15 14 imp ( ( ( 𝐴𝑃𝐵𝑃 ) ∧ 𝐴𝐵 ) → ( ∀ 𝑎𝑃𝑏𝑃 ( 𝑎𝑏 → ∃! 𝑙𝐺 ( 𝑎𝑙𝑏𝑙 ) ) → ∃! 𝑙𝐺 ( 𝐴𝑙𝐵𝑙 ) ) )
16 15 com12 ( ∀ 𝑎𝑃𝑏𝑃 ( 𝑎𝑏 → ∃! 𝑙𝐺 ( 𝑎𝑙𝑏𝑙 ) ) → ( ( ( 𝐴𝑃𝐵𝑃 ) ∧ 𝐴𝐵 ) → ∃! 𝑙𝐺 ( 𝐴𝑙𝐵𝑙 ) ) )
17 3 4 16 3syl ( 𝐺 ∈ Plig → ( ( ( 𝐴𝑃𝐵𝑃 ) ∧ 𝐴𝐵 ) → ∃! 𝑙𝐺 ( 𝐴𝑙𝐵𝑙 ) ) )
18 17 imp ( ( 𝐺 ∈ Plig ∧ ( ( 𝐴𝑃𝐵𝑃 ) ∧ 𝐴𝐵 ) ) → ∃! 𝑙𝐺 ( 𝐴𝑙𝐵𝑙 ) )