Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-line2 Structured version   Visualization version   GIF version

Definition df-line2 33672
Description: Define the Line function. This function generates the line passing through the distinct points 𝑎 and 𝑏. Adapted from definition 6.14 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 25-Oct-2013.)
Assertion
Ref Expression
df-line2 Line = {⟨⟨𝑎, 𝑏⟩, 𝑙⟩ ∣ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎𝑏) ∧ 𝑙 = [⟨𝑎, 𝑏⟩] Colinear )}
Distinct variable group:   𝑎,𝑏,𝑙,𝑛

Detailed syntax breakdown of Definition df-line2
StepHypRef Expression
1 cline2 33669 . 2 class Line
2 va . . . . . . . 8 setvar 𝑎
32cv 1537 . . . . . . 7 class 𝑎
4 vn . . . . . . . . 9 setvar 𝑛
54cv 1537 . . . . . . . 8 class 𝑛
6 cee 26680 . . . . . . . 8 class 𝔼
75, 6cfv 6334 . . . . . . 7 class (𝔼‘𝑛)
83, 7wcel 2114 . . . . . 6 wff 𝑎 ∈ (𝔼‘𝑛)
9 vb . . . . . . . 8 setvar 𝑏
109cv 1537 . . . . . . 7 class 𝑏
1110, 7wcel 2114 . . . . . 6 wff 𝑏 ∈ (𝔼‘𝑛)
123, 10wne 3011 . . . . . 6 wff 𝑎𝑏
138, 11, 12w3a 1084 . . . . 5 wff (𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎𝑏)
14 vl . . . . . . 7 setvar 𝑙
1514cv 1537 . . . . . 6 class 𝑙
163, 10cop 4545 . . . . . . 7 class 𝑎, 𝑏
17 ccolin 33572 . . . . . . . 8 class Colinear
1817ccnv 5531 . . . . . . 7 class Colinear
1916, 18cec 8274 . . . . . 6 class [⟨𝑎, 𝑏⟩] Colinear
2015, 19wceq 1538 . . . . 5 wff 𝑙 = [⟨𝑎, 𝑏⟩] Colinear
2113, 20wa 399 . . . 4 wff ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎𝑏) ∧ 𝑙 = [⟨𝑎, 𝑏⟩] Colinear )
22 cn 11625 . . . 4 class
2321, 4, 22wrex 3131 . . 3 wff 𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎𝑏) ∧ 𝑙 = [⟨𝑎, 𝑏⟩] Colinear )
2423, 2, 9, 14coprab 7141 . 2 class {⟨⟨𝑎, 𝑏⟩, 𝑙⟩ ∣ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎𝑏) ∧ 𝑙 = [⟨𝑎, 𝑏⟩] Colinear )}
251, 24wceq 1538 1 wff Line = {⟨⟨𝑎, 𝑏⟩, 𝑙⟩ ∣ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎𝑏) ∧ 𝑙 = [⟨𝑎, 𝑏⟩] Colinear )}
Colors of variables: wff setvar class
This definition is referenced by:  funline  33677  linedegen  33678  fvline  33679  ellines  33687
  Copyright terms: Public domain W3C validator