# Metamath Proof Explorer

## Definition df-line2

Description: Define the Line function. This function generates the line passing through the distinct points a and b . Adapted from definition 6.14 of Schwabhauser p. 45. (Contributed by Scott Fenton, 25-Oct-2013)

Ref Expression
Assertion df-line2 ${⊢}\mathrm{Line}=\left\{⟨⟨{a},{b}⟩,{l}⟩|\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\left({a}\in 𝔼\left({n}\right)\wedge {b}\in 𝔼\left({n}\right)\wedge {a}\ne {b}\right)\wedge {l}=\left[⟨{a},{b}⟩\right]{\mathrm{Colinear}}^{-1}\right)\right\}$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cline2 ${class}\mathrm{Line}$
1 va ${setvar}{a}$
2 vb ${setvar}{b}$
3 vl ${setvar}{l}$
4 vn ${setvar}{n}$
5 cn ${class}ℕ$
6 1 cv ${setvar}{a}$
7 cee ${class}𝔼$
8 4 cv ${setvar}{n}$
9 8 7 cfv ${class}𝔼\left({n}\right)$
10 6 9 wcel ${wff}{a}\in 𝔼\left({n}\right)$
11 2 cv ${setvar}{b}$
12 11 9 wcel ${wff}{b}\in 𝔼\left({n}\right)$
13 6 11 wne ${wff}{a}\ne {b}$
14 10 12 13 w3a ${wff}\left({a}\in 𝔼\left({n}\right)\wedge {b}\in 𝔼\left({n}\right)\wedge {a}\ne {b}\right)$
15 3 cv ${setvar}{l}$
16 6 11 cop ${class}⟨{a},{b}⟩$
17 ccolin ${class}\mathrm{Colinear}$
18 17 ccnv ${class}{\mathrm{Colinear}}^{-1}$
19 16 18 cec ${class}\left[⟨{a},{b}⟩\right]{\mathrm{Colinear}}^{-1}$
20 15 19 wceq ${wff}{l}=\left[⟨{a},{b}⟩\right]{\mathrm{Colinear}}^{-1}$
21 14 20 wa ${wff}\left(\left({a}\in 𝔼\left({n}\right)\wedge {b}\in 𝔼\left({n}\right)\wedge {a}\ne {b}\right)\wedge {l}=\left[⟨{a},{b}⟩\right]{\mathrm{Colinear}}^{-1}\right)$
22 21 4 5 wrex ${wff}\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\left({a}\in 𝔼\left({n}\right)\wedge {b}\in 𝔼\left({n}\right)\wedge {a}\ne {b}\right)\wedge {l}=\left[⟨{a},{b}⟩\right]{\mathrm{Colinear}}^{-1}\right)$
23 22 1 2 3 coprab ${class}\left\{⟨⟨{a},{b}⟩,{l}⟩|\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\left({a}\in 𝔼\left({n}\right)\wedge {b}\in 𝔼\left({n}\right)\wedge {a}\ne {b}\right)\wedge {l}=\left[⟨{a},{b}⟩\right]{\mathrm{Colinear}}^{-1}\right)\right\}$
24 0 23 wceq ${wff}\mathrm{Line}=\left\{⟨⟨{a},{b}⟩,{l}⟩|\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\left({a}\in 𝔼\left({n}\right)\wedge {b}\in 𝔼\left({n}\right)\wedge {a}\ne {b}\right)\wedge {l}=\left[⟨{a},{b}⟩\right]{\mathrm{Colinear}}^{-1}\right)\right\}$